TauCetiProject/TauCeti

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. TauCeti/Analysis/Complex/Conformal/Reflection.lean carries the full pointwise Schwarz-reflection API (schwarzReflection, differentiableOn_conj_conj, eqOn_schwarzReflection_conj_of_real_on_axis, the upper/lower branch lemmas from five separate PRs) but never proves the theorem the file is named after: the ConformalMapping roadmap's L4 milestone, holomorphy of the reflected function across the real axis (DifferentiableOn ℂ F Ω on a symmetric domain, given holomorphy above, continuity up to the axis, and real boundary values). The hcont-style continuity hypothesis that the crossing argument needs is never used, and no Morera-type lemma exists anywhere in the directory. Task (new mathematics; cite TauCetiRoadmap/ConformalMapping/README.md L4 and match Suggested.lean's milestone signature; carry an authoring claim + tauceti-target ma

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. The ContourIntegration roadmap's distinctive layer, non-integer winding numbers for singularities on the contour (Hungerbühler-Wasem), exists only as definitions that nothing exercises: Analysis/Contour/RegularityConditions.lean's ConditionAprime, ConditionB, SectorCompatible, crossingAngle, basepointAngle, FlatOfOrder each appear in exactly one file (their own): zero consumers, zero instantiation lemmas, so their faithfulness to the paper is currently unfalsifiable. The only computed value is crossingAngle = π at a smooth crossing. ModelSectorWinding.lean's ½ and 1/6 "winding number" theorems evaluate (2πi)⁻¹ ∫ arc at the arc's centre, an off-curve point where the principal value is the ordinary integral; nothing yet computes a winding number to a non-integer value at an on-curve point. (These match the pinned Suggested.

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. Bernstein's theorem (a function on (0,∞) is completely monotone iff it is the Laplace transform of a unique finite measure) is close to assembled in TauCeti/Analysis/CompletelyMonotone/, but is never stated: BernsteinMeasures.lean (~1500 lines) carries the hard analytic content: the Chafaï approximation (chafaiRescaled, chafai_repeated_ibp, pointwiseBoundedOnUnitInterval) producing the approximating measures. Prokhorov/tightness machinery is available (the audit noted a Prokhorov.lean in the repo's dependency reach). BernsteinMeasures.lean's own docstring (around lines 22-24) defers "the final assembly ... recovering f itself" to "the Bernstein-theorem file", which does not exist. Task (new mathematics; cite TauCetiRoadmap/OneParameterSemigroups/README.md, the completely-monotone/Bernstein part, and carry an authoring claim +

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. ∂² = 0 for the fully blocked grid complex, the CombinatorialHeegaardFloer roadmap's designated first nontrivial theorem, is not yet proved. What exists: KnotTheory/Grid/DifferentialSquareCoefficient.lean reduces the goal: fullyBlockedDifferential_comp_self_eq_zero_iff (d² = 0 iff every length-two rectangle-count sum vanishes). DifferentialSquareSupport.lean bounds the support to two-step column-swap neighbours; card_fullyBlockedRectangles_le_two exists. The juxtaposition case analysis that discharges the sums (each composite domain decomposes as two empty rectangles in exactly two ways: disjoint, shared-corner, and the excluded annular cases, per Ozsváth-Stipsicz-Szabó's Grid Homology for Knots and Links) is absent. The files' own docstrings say "the statements here do not assert square-zero". Beware: SmallGridDifferential.l