feat: the symmetric power of a surface is a topological manifold

[sqrt-of-2]

This PR gives the n-th symmetric power of a Hausdorff space charted by a proper algebraically closed normed field K a charted structure over Fin n → K: for a Riemann surface Σ and K = ℂ this is the statement that Sym^g(Σ) is a topological 2g-manifold. The exact target is TauCetiRoadmap/HeegaardFloer/README.md, Lane F4.1, whose first clause reads "Sym^g(Σ) geometry: smooth complex structure (elementary symmetric functions), the totally real tori T_α, T_β, …", after Ozsváth–Szabó (arXiv:math/0101206, §2.1); HeegaardFloer/STATUS.md names it as a concrete, independent frontier target ("Sym^g(Σ) needs its complex structure: promoting Sym.monicEquiv from a bijection to a homeomorphism, and then to a chart"). The milestone served is Lane F4.1 itself, which Lane F4.4's HF̂ differential is eventually counted on. After this PR that milestone still needs the holomorphic transition maps that upgrade this charted structure to a complex manifold, the totally real tori T_α, T_β, π₂ ≅ ℤ for g > 2, and the basepoint divisor with positivity n_z(φ) ≥ 0.

This was the most effective current step because the two inputs it consumes had just landed and nothing consumed them: TauCeti#2228 made the elementary symmetric chart a homeomorphism Sym K n ≃ₜ (Fin n → K), and TauCeti#3710 made the symmetric power locally a product over a pair of disjoint open sets, its own description saying that what remained was "the k-fold decomposition with multiplicities …, the separation argument that those decompositions cover Sym^g(Σ) for a Hausdorff Σ, and then the charted structure itself". This PR is exactly those three steps. The other open HeegaardFloer pull requests, TauCeti#4283 (Sard–Smale), TauCeti#4254 (negative gradient trajectories) and TauCeti#4189 (the Morse index), are Lanes F0 and M and touch none of this.

The k-fold concatenation is TauCeti.Sym.sumSubtype: given a finite family U : ι → Set α, degrees m : ι → ℕ and a proof ∑ i, m i = n, it sends a family of unordered m i-tuples of points of U i to an unordered n-tuple of points of α, as the sum of the underlying multisets. Carrying the degree condition as a hypothesis rather than making the target Sym α (∑ i, m i) is what lets the map be composed with other maps of symmetric powers without a cast, which the two-member TauCeti.Sym.appendSubtype does not need because n + m is already the sum. For a pairwise disjoint family each part is recovered by filtering on membership in U i, so the map is injective with the expected range. Openness reduces to ordered tuples: TauCeti.Sym.ofFn is an open quotient map on each member, hence so is the product of those maps by Mathlib's IsOpenQuotientMap.piMap, and read on ordered tuples the concatenation is the regrouping of the n entries along a bijection (Σ i, Fin (m i)) ≃ Fin n — a homeomorphism followed by the open inclusions U i ↪ α. That bijection exists because the degrees add up to n, and it is used only through its existence, so no canonicity is claimed for it.

The separation step is TauCeti.exists_mem_range_sumSubtype_of_t2: in a Hausdorff space the distinct points of an unordered tuple have pairwise disjoint open neighbourhoods, which may moreover be taken inside arbitrary prescribed ones, and the tuple is then a concatenation along that family with its multiplicities as the degrees. Taking the prescribed neighbourhoods to be the sources of the charts of α and reading each factor through TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map gives a partial homeomorphism from Sym α n to Fin n → K around every tuple, and hence the ChartedSpace instance. Because the separating neighbourhoods and the regrouping bijection are choices, the atlas is a choice of one chart per point, which is exactly what a charted structure asks for; the module documentation says so and records that exhibiting an atlas with holomorphic transitions is the next step and is not done here. A noncomputable example checks the instance is not vacuous by applying it to the model space itself.

New: TauCeti/Data/Sym/Family.lean (213 lines), the concatenation and its algebra, with nothing topological in it; TauCeti/Topology/Sym/Family.lean (172 lines), the open embedding and the Hausdorff separation; TauCeti/Topology/PiCurry.lean (68 lines), Equiv.piCurry as a homeomorphism and the regrouping of an n-tuple into a family of m i-tuples, which Mathlib has only for a product index (Homeomorph.piCurry) and not for a sigma one; and TauCeti/Geometry/Manifold/SymmetricPower.lean (111 lines), the charts. Also amended: two sentences of module documentation in TauCeti/Topology/Sym/Disjoint.lean and TauCeti/Analysis/Polynomial/SymmetricPower.lean, pointing at the new files where each says what remains. Every proof runs through Mathlib: Set.Finite.t2_separation for the disjoint neighbourhoods, IsOpenQuotientMap.piMap, IsOpenMap.piMap and IsOpenEmbedding.piMap for the products, Homeomorph.piCongrLeft and Fintype.equivFinOfCardEq for the regrouping, Multiset.count/Multiset.filter for the splitting, and IsOpenEmbedding.toOpenPartialHomeomorph for the charts. No Mathlib infrastructure and no external formalization is vendored. The three declarations that take an unordered tuple as an explicit argument sit in the TauCeti namespace rather than TauCeti.Sym, following TauCeti.symFinTwoEquiv, because dot notation on Mathlib's Sym cannot resolve inside namespace TauCeti.

Roadmap: HeegaardFloer

🤖 Prepared with Claude Code

[brettkoonce]

🟡 correctness — request_changes claude/claude-opus-5

The concatenation, its range description, the Hausdorff separation and the chart assembly are all faithful, and the ChartedSpace instance is exactly what is proven. But the new module's title and two docstrings assert a topological manifold, which is strictly stronger than the ChartedSpace structure established, and the advertised non-vacuity check does not establish what its docstring says.

• TauCeti/Geometry/Manifold/SymmetricPower.lean:13 — The module title ("is a topological manifold"), line 17 ("This is the statement that Sym^g(Σ) is a topological 2g-manifold") and the instance docstring at line 102 claim more than is proven: only ChartedSpace (Fin n → K) (Sym α n) is established. No second countability is assumed (the hypotheses admit e.g. an uncountable disjoint union of copies of ℂ, which is T2 and charted by ℂ), and Hausdorffness of Sym α n is never proven either. Fix: Retitle to the charted-space claim and add the caveat the repo already uses verbatim elsewhere: that this is a ChartedSpace structure only, and that the topological-manifold reading needs global hypotheses (second countability) plus T2 of Sym α n, none of which are assumed here.
• TauCeti/Geometry/Manifold/SymmetricPower.lean:109 — noncomputable example : ChartedSpace (Fin n → K) (Sym K n) := inferInstance is stated under the very typeclass hypotheses it claims to witness, so its docstring "The hypotheses are satisfiable" is false: it would typecheck even if no type satisfied NormedField + IsAlgClosed + ProperSpace. Fix: Instantiate at a concrete field — noncomputable example (n : ℕ) : ChartedSpace (Fin n → ℂ) (Sym ℂ n) := inferInstance (importing Mathlib.Analysis.Complex.Polynomial.Basic for Complex.isAlgClosed) — or reword the docstring to say only that the instance applies with α := K.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 212s · 15 in / 15.7k out tokens · reviewing this diff · rubric}

[brettkoonce]

🟡 reuse — request_changes claude/claude-opus-5

The new family-indexed sumSubtype API clones the existing two-set appendSubtype API declaration for declaration (12 pairs, same proofs) and leaves that API with zero consumers. Two proofs also re-derive located lemmas: IsOpenQuotientMap.isOpenMap_iff (already used twice in this repo) and Mathlib's OpenPartialHomeomorph.isOpenEmbedding_restrict.

• TauCeti/Data/Sym/Family.lean:73 — sumSubtype and its lemmas are a strict generalisation (ι := Fin 2) of the existing appendSubtype API, cloned declaration for declaration with the same proofs: appendSubtype/sumSubtype (Data/Sym/Disjoint.lean:52), coe_appendSubtype/coe_sumSubtype (:56), appendSubtype_ofFn/sumSubtype_ofFn (:72), mem_union_of_mem_appendSubtype/exists_mem_of_mem_sumSubtype (:78), filter_mem_map_val_add/filter_mem_coe_sumSubtype (:89), card_filter_mem_appendSubtype/card_filter_mem_sumSubtype (:104), appendSubtype_injective/sumSubtype_injective (:112), exists_appendSubtype_eq/exists_sumSubtype_eq (:130), mem_range_appendSubtype/mem_range_sumSubtype (:165), plus continuous_appendSubtype/isOpenMap_appendSubtype/isOpenEmbedding_appendSubtype (Topology/Sym/Disjoint.lean:65,71,81). After this PR the two-set version has no consumer anywhere. Fix: Delete the two-set concatenation sections (Data/Sym/Disjoint.lean:48-171 and Topology/Sym/Disjoint.lean:61-84 — keep the ofFn_map sections, which isOpenEmbedding_coeffEquiv_comp_ofFn_map still uses) and repoint the docs that name them: Analysis/Polynomial/SymmetricPower.lean:190 ("a general tuple is split into such groups by TauCeti.Sym.isOpenEmbedding_appendSubtype" — the splitting actually used is now isOpenEmbedding_sumSubtype), Topology/Sym/Disjoint.lean:18,21,45 and Data/Sym/Disjoint.lean:19,28-33. If the Prod form is wanted, keep appendSubtype as a definition and derive its lemmas from the sumSubtype ones rather than re-proving them.
• TauCeti/Topology/Sym/Family.lean:108 — isOpenMap_sumSubtype re-derives IsOpenQuotientMap.isOpenMap_iff by hand: the 8-line calc computing sumSubtype '' W = ofFn '' (regroup '' (q ⁻¹' W)) via Set.image_preimage_eq _ hq.surjective and Set.image_comp is exactly that lemma's proof. Fix: Replace the body with rw [isOpenQuotientMap_piMap_ofFn.isOpenMap_iff, sumSubtype_comp_piMap_ofFn hn e]; exact isOpenMap_ofFn.comp (isOpenMap_regroup hU e), mirroring isOpenMap_map and isOpenMap_append.
• TauCeti/Geometry/Manifold/SymmetricPower.lean:61 — isOpenEmbedding_chartRestrict reproves continuity, injectivity and openness of a chart restricted to an open subset of its source; Mathlib already has the restriction to the source, and the inclusion of an open subset is an open embedding. Fix: e.isOpenEmbedding_restrict.comp ⟨.inclusion hVs, by rw [Set.range_inclusion]; exact isOpen_induced hVo⟩ (the composite is defeq to fun x : ↥V => e ↑x), deleting the hand proof.
• TauCeti/Topology/Sym/Family.lean:73 — The private homeomorphism R is the same construction as the new piFinSumHomeomorph: both are (piCurryHomeomorph fun (i : ι) (_ : Fin (m i)) => _).symm.trans (Homeomorph.piCongrLeft ...), one with fibre ↥(U k.1) and a given e, the other with a constant fibre and a chosen e. Fix: State the sigma-regrouping once in TauCeti/Topology/PiCurry.lean with a dependent fibre Z : (Σ i, κ i) → Type* and an explicit e : (Σ i, κ i) ≃ ι', giving (∀ i j, Z ⟨i, j⟩) ≃ₜ (∀ j, Z (e.symm j)); obtain piFinSumHomeomorph (constant Z) and R (Z := fun k => ↥(U k.1)) from it.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 264s · 29 in / 21.1k out tokens · reviewing this diff · rubric}

[brettkoonce]

🟡 api-design — request_changes claude/claude-opus-5

The canonical post-PR ChartedSpace (Fin n → K) (Sym α n) instance is built from Classical.choose of a bare existence statement, so no chartAt/atlas lemma is possible and the next roadmap step (holomorphic transitions) cannot use it; piFinSumHomeomorph likewise ships with no characterizing lemma, and the superseded appendSubtype API is left with no consumer.

• TauCeti/Geometry/Manifold/SymmetricPower.lean:103 — instChartedSpaceSym fixes the canonical charted structure on Sym α n to (exists_openPartialHomeomorph_sym s).choose, and nothing characterizes it: there is no lemma for chartAt K s, its source, its value, or atlas. exists_openPartialHomeomorph_sym (line 74) discards everything its proof establishes (the disjoint family V, the degrees m, the composite formula), keeping only s ∈ e.source, so the atlas is unusable — including for the HasGroupoid/holomorphic-transition step the module doc names as next. Fix: Strengthen exists_openPartialHomeomorph_sym to also record the chart's source (e.source = Set.range (Sym.sumSubtype V m hm)) and its value on that source (the Sym.coeffEquiv/piFinSumHomeomorph composite), then add instChartedSpaceSym_chartAt and instChartedSpaceSym_atlas lemmas so consumers never unfold the instance.
• TauCeti/Geometry/Manifold/SymmetricPower.lean:111 — As a global instance it also fires on the model space: chartAt (Fin n → K) (s : Sym K n) (via chartedSpaceSelf) is an arbitrary chosen chart, not the canonical Sym.coeffHomeomorph K n, and it forecloses adding the natural single-chart structure on Sym K n later — that would be a second competing instance for the same pair of types. Fix: Either follow the collarChartedSpace precedent and make the general construction a def while registering the single-chart structure from Sym.coeffHomeomorph as the instance on Sym K n, or characterize the general charts (finding 1) so the model case can be proved to agree with coeffHomeomorph.
• TauCeti/Topology/PiCurry.lean:58 — piFinSumHomeomorph is a public main declaration whose action is unstatable: the bijection is chosen internally by Fintype.equivFinOfCardEq and there is no apply/symm_apply lemma, unlike its sibling piCurryHomeomorph. Since the chart of finding 1 is composed with it, no chart formula can be written even after strengthening exists_openPartialHomeomorph_sym. Fix: Take the bijection as an explicit argument, piFinSumHomeomorph (Y) (e : (Σ i, Fin (m i)) ≃ Fin n), matching Sym.sumSubtype_ofFn, and add @[simp] piFinSumHomeomorph_apply/_symm_apply; keep the Nonempty ((Σ i, Fin (m i)) ≃ Fin n) existence lemma separately if only existence is needed at the call site.
• TauCeti/Data/Sym/Disjoint.lean:52 — Sym.sumSubtype and its lemma set supersede Sym.appendSubtype, and after this PR the pair version has no consumer anywhere in the repo: appendSubtype, coe_appendSubtype, appendSubtype_eq_append_map, appendSubtype_ofFn, mem_union_of_mem_appendSubtype, card_filter_mem_appendSubtype, appendSubtype_injective, exists_appendSubtype_eq, mem_range_appendSubtype, continuous_appendSubtype, isOpenMap_appendSubtype, isOpenEmbedding_appendSubtype are referenced only by each other and by module docs. The post-PR surface carries two parallel APIs for one operation. Fix: Delete the appendSubtype sections (TauCeti/Data/Sym/Disjoint.lean:48-171 and TauCeti/Topology/Sym/Disjoint.lean:61-84) and update the module docs that point at them; the ofFn_map material in those files stays since isOpenEmbedding_ofFn_map is still used.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 251s · 19 in / 18.2k out tokens · reviewing this diff · rubric}

[brettkoonce]

🟡 generality — request_changes claude/claude-opus-5

The family concatenation is the right general statement, but the PR leaves the strictly special-case appendSubtype development standing as a full parallel copy rather than deriving or removing it, states the concatenation only for subtype families instead of factoring through a hypothesis-free family concatenation as the pair case does, and carries a globally quantified neighbourhood hypothesis the proof only uses on the tuple's support.

• TauCeti/Data/Sym/Family.lean:73 — sumSubtype plus its lemma list (coe, exists_mem_of_mem, filter_mem, card_filter, injective, exists_eq, mem_range, continuous, isOpenMap, isOpenEmbedding) strictly subsumes the two-set appendSubtype (Data/Sym/Disjoint.lean:52-171, Topology/Sym/Disjoint.lean:65-84), whose identical lemma list is proved separately and is now used by nothing; two canonical names for "the symmetric power is locally a product" result. The same holds, at m ≡ 1, for isOpenEmbedding_ofFn_map (Topology/Sym/Disjoint.lean:93) modulo Sym (U i) 1 ≃ U i. Fix: Derive the pair case from the family case (index by Bool/Fin 2, composing with the product equivalence), or, since Tau Ceti keeps no obsolete surface, delete the subsumed appendSubtype development in this PR and repoint the doc references at sumSubtype.
• TauCeti/Topology/Sym/Family.lean:100 — Under-generalized: the concatenation exists only for families of subtypes, so continuous_sumSubtype/isOpenMap_sumSubtype conflate the hypothesis-free concatenation (∀ i, Sym α (m i)) → Sym α n with functoriality for the inclusions U i ↪ α; hU belongs only to the latter. The pair case performs exactly this factorization. Fix: Define the un-subtyped family concatenation, prove Continuous/IsOpenMap for it with no hypotheses, and get sumSubtype = that ∘ Pi.map (Sym.map Subtype.val) with hU entering through isOpenMap_map hU.isOpenMap_subtype_val.
• TauCeti/Topology/Sym/Family.lean:145 — exists_mem_range_sumSubtype_of_t2 assumes ∀ a, IsOpen (W a) and ∀ a, a ∈ W a for every point of α, but the proof only ever evaluates these at points of (w : Multiset α).toFinset — a stronger hypothesis than proved, asymmetric with the conclusion, whose V is indexed by that support. Fix: Weaken to (hWo : ∀ a ∈ w, IsOpen (W a)) (hWm : ∀ a ∈ w, a ∈ W a); the sole call site (Geometry/Manifold/SymmetricPower.lean:78) supplies a global family and needs only fun a _ => ….

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 185s · 15 in / 13.7k out tokens · reviewing this diff · rubric}

[brettkoonce]

Re: your reply on generality — re-reviewed on 271df2e; the finding stands — The family concatenation is the right general statement, but the PR leaves the strictly special-case appendSubtype development standing as a full parallel copy rather than deriving or removing it, states the concatenation only for subtype families instead of factoring through a hypothesis-free family concatenation as the pair case does, and carries a globally quantified neighbourhood hypothesis the proof only uses on the tuple's support.

_{claude/claude-opus-5 · addresses your replies through comment 3839170716.}

[sqrt-of-2]

Addressing this review in parts:

• I removed the superseded appendSubtype development and updated every in-repository reference.
• I weakened exists_mem_range_sumSubtype_of_t2 so openness and membership are assumed only on the tuple's support.
• I am contesting only the request to add a second, hypothesis-free family concatenation API.

That requested declaration is not a prerequisite of the roadmap target or of any proof in this PR. The sole downstream construction needs exactly the subtype-family map (∀ i, Sym (U i) (m i)) → Sym α n, because its range, injectivity, and openness over disjoint coordinate patches are the data used to construct the chart. Factoring it through a new map (∀ i, Sym α (m i)) → Sym α n would add public mathematics with no consumer and then add another theorem solely to recover the map already used.

This also conflicts with the earlier generality approval on the same implementation, which said: “The declarations are stated at their natural level: finite-family results are genuinely used by the chart construction” (scoreboard), and with the current-head scope approval, which identifies the family decomposition as a direct prerequisite in one coherent dependency chain (scoreboard). Adding an unused generic layer would regress those approved scope/API constraints and would violate the repository rule that new mathematical declarations must be needed by a specific roadmap target.

Empirically, the narrower construction is sufficient: after the other requested changes, lake build completed successfully (8948 jobs), and lake exe axioms audited 67736 TauCeti declarations with all axioms in the allowlist.

No code change was made for this one subfinding.

[brettkoonce]

🟡 placement — request_changes claude/claude-opus-5

File placement and imports of the four new modules are correct, but one generic lemma is still in the wrong home: TauCeti.Sym.coe_ofFn_eq_sum is a plain ofFn lemma living in the disjoint-family file.

• TauCeti/Data/Sym/Family.lean:55 — TauCeti.Sym.coe_ofFn_eq_sum takes fresh {β} {k} (g : Fin k → β) and mentions nothing from this file (U, m, n, disjointness, sumSubtype); it is a general fact about the multiset underlying ofFn, sitting in a file about splitting along a pairwise disjoint family. Fix: Move it to TauCeti/Data/Sym/Basic.lean beside coe_ofFn, adding whatever big-operator import it needs there; Data/Sym/Family.lean reaches that file transitively via TauCeti.Data.Sym.Disjoint.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 176s · 35 in / 13.3k out tokens · reviewing this diff · rubric}

[brettkoonce]

✅ naming — now passing on 271df2e.

[brettkoonce]

🟡 documentation — request_changes claude/claude-opus-5

Documentation coverage is complete and mostly accurate, but the new manifold file still claims the result "is" a topological 2g-manifold when the declaration delivers only a ChartedSpace instance, and a docstring in a file this PR edits still points at the two-set concatenation as what splits a general tuple.

• TauCeti/Geometry/Manifold/SymmetricPower.lean:17 — Overclaim: the module title (line 13), line 17 ("This is the statement that Sym^g(Σ) is a topological 2g-manifold") and the instChartedSpaceSym docstring (line 102) promise manifold status, but the statement is only ChartedSpace (Fin n → K) (Sym α n) — no second countability is assumed or concluded. Fix: Say the symmetric power is charted by / locally homeomorphic to Fin n → K, and note that Hausdorffness comes from the separate TauCeti.Sym.instT2Space while second countability is neither assumed nor proved; reserve "topological 2g-manifold" for a statement that carries those.
• TauCeti/Analysis/Polynomial/SymmetricPower.lean:190 — Stale cross-reference: the docstring of isOpenEmbedding_coeffEquiv_comp_map says "a general tuple is split into such groups by TauCeti.Sym.isOpenEmbedding_appendSubtype", but that map splits into exactly two groups; the general k-group splitting added by this PR is TauCeti.Sym.isOpenEmbedding_sumSubtype. Fix: Point the sentence at TauCeti.Sym.isOpenEmbedding_sumSubtype, as the PR already did for this file's module docstring (lines 50-51).

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 99s · 19 in / 7.1k out tokens · reviewing this diff · rubric}

[brettkoonce]

🟡 proof-quality — request_changes claude/claude-opus-5

Two proofs remain factorable or defeq-reliant: an undocumented rfl closes a goal that Mathlib's Fin.univ_val_map states outright, and the count-sum computation is duplicated verbatim across two files (once inline inside a theorem statement). The regrouping homeomorphism is also constructed twice.

• TauCeti/Data/Sym/Family.lean:59 — In coe_ofFn_eq_sum, rw [coe_ofFn, List.ofFn_eq_map] is followed by an undocumented rfl that unfolds (Finset.univ : Finset (Fin k)).val through the Fin.fintype instance and Multiset.map's quotient lift. Fix: Replace the two lines with rw [coe_ofFn, Fin.univ_val_map] (or simp [coe_ofFn]), which is the named lemma for exactly this equality.
• TauCeti/Topology/Sym/Family.lean:150 — The proof that the multiplicities of a tuple sum to n is duplicated verbatim: an inline by rw [Finset.sum_coe_sort …, Multiset.toFinset_sum_count_eq]; exact w.2 embedded in the statement of exists_mem_range_sumSubtype_of_t2, and the identical script as hm in TauCeti/Geometry/Manifold/SymmetricPower.lean:82-85. Fix: Add a lemma next to sumSubtype, e.g. theorem sum_count_toFinset (w : Sym α n) : ∑ i : ↥(w : Multiset α).toFinset, Multiset.count (i : α) (w : Multiset α) = n, and use it in both places so no tactic block sits inside a theorem statement.
• TauCeti/Topology/PiCurry.lean:58 — piFinSumHomeomorph and the local R in Sym.isOpenMap_regroup (TauCeti/Topology/Sym/Family.lean:73-75) are the same (piCurryHomeomorph …).symm.trans (Homeomorph.piCongrLeft …) construction, built twice because the public one fixes a constant fibre. Fix: State the dependent version once in PiCurry.lean, (e : (Σ i, Fin (m i)) ≃ Fin n) : (∀ i, Fin (m i) → Z i) ≃ₜ (∀ j : Fin n, Z (e.symm j).1), and define piFinSumHomeomorph and R as its constant-fibre and Z i = ↥(U i) instances.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 218s · 15 in / 15.2k out tokens · reviewing this diff · rubric}

[brettkoonce]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
🟡	correctness	changes requested	claude/claude-opus-5	The concatenation, its range description, the Hausdorff separation and the chart assembly are all faithful, and the ChartedSpace instance is exactly what is proven. But the new module's title and two docstrings assert a topological manifold, which is strictly stronger than the ChartedSpace structure established, and the advertised non-vacuity check does not establish what its docstring says.
🟡	reuse	changes requested	claude/claude-opus-5	The new family-indexed sumSubtype API clones the existing two-set appendSubtype API declaration for declaration (12 pairs, same proofs) and leaves that API with zero consumers. Two proofs also re-derive located lemmas: IsOpenQuotientMap.isOpenMap_iff (already used twice in this repo) and Mathlib's OpenPartialHomeomorph.isOpenEmbedding_restrict.
♻️	scope	stale (re-run pending)	claude/claude-opus-5	The PR advances the first clause of Lane F4.1 (HeegaardFloer/README.md:224) via the step STATUS.md:37 names as concrete and independent, continuing the monicEquiv → homeomorphism → local product chain. It is a single topic: four files in one dependency chain plus two doc-sentence edits.
♻️	attribution	stale (re-run pending)	claude/claude-opus-5	The paper source (Ozsváth–Szabó arXiv:math/0101206 §2.1) is cited in the module docs of both new mathematical files and matches the roadmap's own reference for Lane F4.1; the Mathlib declarations built on (Equiv.piCurry, Homeomorph.piCurry) and the in-repo predecessors (appendSubtype, coeffEquiv chart) are named where they are followed. No vendored or uncredited external work.
🟡	api-design	changes requested	claude/claude-opus-5	The canonical post-PR ChartedSpace (Fin n → K) (Sym α n) instance is built from Classical.choose of a bare existence statement, so no chartAt/atlas lemma is possible and the next roadmap step (holomorphic transitions) cannot use it; piFinSumHomeomorph likewise ships with no characterizing lemma, and the superseded appendSubtype API is left with no consumer.
🟡	generality	changes requested	claude/claude-opus-5	The family concatenation is the right general statement, but the PR leaves the strictly special-case appendSubtype development standing as a full parallel copy rather than deriving or removing it, states the concatenation only for subtype families instead of factoring through a hypothesis-free family concatenation as the pair case does, and carries a globally quantified neighbourhood hypothesis the proof only uses on the tuple's support.
🟡	placement	changes requested	claude/claude-opus-5	File placement and imports of the four new modules are correct, but one generic lemma is still in the wrong home: TauCeti.Sym.coe_ofFn_eq_sum is a plain ofFn lemma living in the disjoint-family file.
✅	naming	approved	claude/claude-opus-5	Names mirror the adjacent appendSubtype API, describe their conclusions, and none overstates its statement; no notation is introduced. The prior round's sum_count_toFinset_eq finding is resolved — the declaration is gone and the fact is proved inline.
🟡	documentation	changes requested	claude/claude-opus-5	Documentation coverage is complete and mostly accurate, but the new manifold file still claims the result "is" a topological 2g-manifold when the declaration delivers only a ChartedSpace instance, and a docstring in a file this PR edits still points at the two-set concatenation as what splits a general tuple.
🟡	proof-quality	changes requested	claude/claude-opus-5	Two proofs remain factorable or defeq-reliant: an undocumented rfl closes a goal that Mathlib's Fin.univ_val_map states outright, and the count-sum computation is duplicated verbatim across two files (once inline inside a theorem statement). The regrouping homeomorphism is also constructed twice.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 271df2e. rubrics @ f854a7e. Review spend: $30.18.}

[raresbuhai]

🟡 reuse — request_changes codex/gpt-5.6-sol

One public theorem is an unnecessary specialization of an existing Mathlib result.

• TauCeti/Data/Sym/Family.lean:210 — TauCeti.sum_count_toFinset_eq merely repackages Mathlib's Multiset.toFinset_sum_count_eq with an extra cardinality hypothesis. Fix: Delete the wrapper and use Multiset.toFinset_sum_count_eq followed by w.2 (with Finset.sum_coe_sort only where the subtype-indexed form is required).

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 68s · 379.2k in / 2k out tokens · reviewing this diff · rubric}

[raresbuhai]

🟡 api-design — request_changes codex/gpt-5.6-sol

The public API unnecessarily exposes the implementation of the sigma-index currying homeomorphism despite already providing characteristic simp lemmas.

• TauCeti/Topology/PiCurry.lean:38 — piCurryHomeomorph is marked @[expose], making its body part of the downstream interface solely to support unfolding in a later proof. Fix: Remove @[expose] and rewrite isOpenMap_regroup/hfun using the public apply and symm-apply lemmas (adding another characteristic lemma if required).

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 37s · 68.7k in / 890 out tokens · reviewing this diff · rubric}

[raresbuhai]

🟡 generality — request_changes codex/gpt-5.6-sol

One public multiplicity theorem is unnecessarily specialized to an arbitrary target degree instead of stating the natural cardinality identity.

• TauCeti/Data/Sym/Family.lean:210 — sum_count_toFinset_eq assumes card w = n merely to replace the natural right-hand side card w by n, creating an under-general public wrapper. Fix: State the subtype-indexed theorem with conclusion ∑ i : ↥w.toFinset, w.count i = w.card, then derive the required degree equality locally using w.2.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 58s · 141.7k in / 1.4k out tokens · reviewing this diff · rubric}

[raresbuhai]

🟡 naming — request_changes codex/gpt-5.6-sol

One declaration is misleadingly named and placed outside the namespace of the object it describes.

• TauCeti/Data/Sym/Family.lean:210 — TauCeti.sum_count_toFinset_eq is solely a theorem about Multiset, while toFinset misleadingly appears as the sum’s argument rather than the subtype indexing it; this conflicts with the adjacent namespaced Mathlib terminology. Fix: Move it to namespace Multiset and name it after the actual conclusion, e.g. Multiset.sum_attach_toFinset_count_eq_of_card_eq, or state the cardinality conclusion directly as ..._eq_card.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 45s · 118.9k in / 1.3k out tokens · reviewing this diff · rubric}

[raresbuhai]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The family decomposition, Hausdorff separation, local elementary-symmetric coordinates, and resulting ChartedSpace instance faithfully formalize the stated topological-manifold step.
🟡	reuse	changes requested	codex/gpt-5.6-sol	One public theorem is an unnecessary specialization of an existing Mathlib result.
✅	scope	approved	codex/gpt-5.6-sol	The PR is a coherent implementation of the chart step explicitly named in Heegaard Floer Lane F4.1 and STATUS.md. Its family decomposition, topological regrouping, separation, and chart construction are proximate prerequisites assembled toward that single target.
✅	attribution	approved	codex/gpt-5.6-sol	The new manifold and local-product modules credit Ozsváth–Szabó §2.1 in code, and identify the central pre-existing Tau Ceti and Mathlib inputs they build on. No uncredited copied or closely adapted external formalization was found.
🟡	api-design	changes requested	codex/gpt-5.6-sol	The public API unnecessarily exposes the implementation of the sigma-index currying homeomorphism despite already providing characteristic simp lemmas.
🟡	generality	changes requested	codex/gpt-5.6-sol	One public multiplicity theorem is unnecessarily specialized to an arbitrary target degree instead of stating the natural cardinality identity.
✅	placement	approved	codex/gpt-5.6-sol	The new declarations are placed in natural algebraic, topological, and manifold modules, and the diff shows no evidently wrong import.
🟡	naming	changes requested	codex/gpt-5.6-sol	One declaration is misleadingly named and placed outside the namespace of the object it describes.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive files have useful module documentation, and the public definitions and main theorems are documented accurately without overstating the constructed charted structure as a complex manifold.
✅	proof-quality	approved	codex/gpt-5.6-sol	The new proofs are readable and appropriately factored, with no undocumented change/show, unjustified revert, excessive proof length, or materially brittle automation.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 4f918be. rubrics @ f854a7e. Review spend: $2.48.}

[CBirkbeck]

🟡 placement — request_changes codex/gpt-5.6-sol

Three imports are redundant through other imports in the same files.

• TauCeti/Data/Sym/Family.lean:8 — Mathlib.Algebra.BigOperators.Group.Finset.Basic is redundant. Fix: Delete this import.
• TauCeti/Topology/Sym/Family.lean:8 — Mathlib.Topology.Separation.Hausdorff is redundant. Fix: Delete this import.
• TauCeti/Geometry/Manifold/SymmetricPower.lean:10 — TauCeti.Topology.PiCurry is redundant. Fix: Delete this import.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 46s · 157k in / 1.5k out tokens · reviewing this diff · rubric}

[CBirkbeck]

🟡 documentation — request_changes codex/gpt-5.6-sol

The new public declarations are documented, but one module docstring reverses the direction of the existing API it describes.

• TauCeti/Data/Sym/Family.lean:15 — The module docstring says appendSubtype “splits an unordered tuple,” but appendSubtype takes two symmetric-power inputs and concatenates them into Sym α (n + m). Fix: Replace “splits an unordered tuple along two disjoint sets” with “concatenates unordered tuples drawn from two disjoint sets,” or equivalent directionally accurate wording.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 54s · 189.9k in / 1.9k out tokens · reviewing this diff · rubric}

[CBirkbeck]

🟡 proof-quality — request_changes codex/gpt-5.6-sol

The chart construction closes its critical source-membership goal through an opaque simpa, making the proof depend on simplifier unfolding across several partial-homeomorphism wrappers.

• TauCeti/Geometry/Manifold/SymmetricPower.lean:97 — simpa using hmem hides why membership in range (Sym.sumSubtype V m hm) implies membership in the source of the composed chart and relies on non-obvious unfolding of toOpenPartialHomeomorph, symm, and trans. Fix: Rewrite the composite source explicitly using OpenPartialHomeomorph.trans_source, symm_source, and the generated source/target lemmas for IsOpenEmbedding.toOpenPartialHomeomorph, then discharge the resulting range-membership goal with hmem.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 34s · 128.3k in / 1.3k out tokens · reviewing this diff · rubric}

[CBirkbeck]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The family decomposition, Hausdorff separation, local elementary-symmetric charts, and resulting ChartedSpace instance faithfully establish the claimed topological manifold structure without vacuous assumptions or placeholders.
✅	reuse	approved	codex/gpt-5.6-sol	The new family concatenation, sigma-indexed currying homeomorphism, local product construction, and charted-space instance are not duplicated in TauCeti or Mathlib; the implementation reuses the available pairwise, quotient-map, separation, and product-homeomorphism APIs.
✅	scope	approved	codex/gpt-5.6-sol	The PR directly advances HeegaardFloer Lane F4.1 by constructing the charted structure explicitly identified as an independent frontier task. Its family decomposition, topology, tuple-regrouping, and chart construction form one coherent dependency chain.
✅	attribution	approved	codex/gpt-5.6-sol	The central informal source, Ozsváth–Szabó §2.1, is credited in the relevant module documentation, and the reused Tau Ceti constructions are identified by declaration. No uncredited vendored or closely adapted external formalization is evident.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical public surface is appropriately scoped: reusable concatenation and regrouping constructions have characteristic lemmas, implementation-only chart assembly helpers remain private, and normal-form application/coercion lemmas carry @[simp]. No compatibility-only or materially incomplete API is introduced.
✅	generality	approved	codex/gpt-5.6-sol	The declarations are stated at their natural level: finite-family results are genuinely used by the chart construction, and the Hausdorff, charted-space, algebraic-closure, and properness hypotheses match the separation and symmetric-polynomial inputs.
🟡	placement	changes requested	codex/gpt-5.6-sol	Three imports are redundant through other imports in the same files.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names describe their conclusions using established TauCeti and Mathlib terminology, and no new notation is introduced.
🟡	documentation	changes requested	codex/gpt-5.6-sol	The new public declarations are documented, but one module docstring reverses the direction of the existing API it describes.
🟡	proof-quality	changes requested	codex/gpt-5.6-sol	The chart construction closes its critical source-membership goal through an opaque simpa, making the proof depend on simplifier unfolding across several partial-homeomorphism wrappers.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head fc7374e. rubrics @ f854a7e. Review spend: $2.77.}