feat: calculate the nonlinear parameter projection

[sqrt-of-2]

This PR computes the nonlinear parameter projection in a regular chart of a universal Fredholm level set. It defines levelSetParameterMap, proves that its derivative at the chart origin is exactly the existing linear map parameterProj D₁ D₂, and derives the expected surjectivity, Fredholm, and index statements. It then applies the local Sard--Smale theorem to show that critical values coming from a sufficiently small chart neighbourhood form a closed nowhere dense set.

The exact roadmap target is TauCetiRoadmap/HeegaardFloer/README.md, Lane F0, milestone “the moduli space = zero set of a Fredholm section, generically a manifold of dimension = index” package. This is the most effective current step because parameterProj, the complemented-kernel theorem for universal linearizations, smooth regular-level-set charts, and Sard--Smale are all on main, while the only open HeegaardFloer PR (#5018) develops the independent split-quadratic Morse-flow model in Lane M. After this PR, the Lane F0 milestone still needs smooth compatibility and a countable localization across universal-level-set charts to obtain a residual set of regular parameters globally; the separate strip-operator target d/ds + A(s) also remains.

The new module TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean is 252 lines. Its public API keeps the level-set chart construction generic over a nontrivially normed field, specializes Fredholmness only to the existing RCLike setting, and specializes Sard--Smale only to real Banach spaces. No Mathlib code or external formalization is vendored. The construction follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3, and Smale, An infinite dimensional version of Sard's theorem (1965), as credited in the module documentation.

Roadmap: HeegaardFloer

🤖 Prepared with Codex

[roed-math]

🟡 reuse — request_changes claude/claude-opus-5

No existing declaration is duplicated wholesale; the linear parameterProj API is properly reused. But the file contains a private lemma that restates a public one, and two proofs that re-derive results already provided by Mathlib and by an earlier line of the same file.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:93 — The private levelSetParameterMap_eq is exactly the funext of the public levelSetParameterMap_apply (line 80); the two state the same fact pointwise and as functions. Fix: Delete levelSetParameterMap_eq and replace its two uses (lines 124, 146) with rw [funext (levelSetParameterMap_apply hf hD hker hxl)] — the same idiom already used at TauCeti/Analysis/Fredholm/SardSmale.lean:173 (rw [funext (pkg.obstructionSlice_apply hT y.1)]).
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:138 — hcomp := (ContinuousLinearMap.snd K E Λ).hasStrictFDerivAt.comp 0 hchart re-derives Mathlib's HasStrictFDerivAt.snd, which already gives HasStrictFDerivAt (fun x => (f x).2) ((snd 𝕜 F G).comp f') x — the exact statement, with the exact composite map hlinear then rewrites. Fix: Use have hcomp := hchart.snd, matching the hchart.snd already used at line 125 for the ContDiffAt version.
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:239 — hFred is reproved by rw [hg']; exact isFredholm_parameterProj D₁ D₂ hD₁, duplicating isFredholm_fderiv_levelSetParameterMap proved 50 lines earlier (line 189), which has no other consumer in the repo. Fix: Replace lines 239-241 with have hFred := isFredholm_fderiv_levelSetParameterMap hf hD hker hxl hD₁; it applies over ℝ since RCLike ℝ gives IsRCLikeNormedField ℝ (mathlib/Mathlib/Analysis/RCLike/Basic.lean:1298) and CompleteSpace ℝ holds.

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 · 136s · 2.3k in / 9.9k out tokens · reviewing this diff · rubric}

[roed-math]

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

The exported surface is minimal and bodies stay hidden, but the headline Sard--Smale theorem is stated with let-bound hypotheses instead of taking hker like every other declaration in the file, the main derivative computation lacks @[simp], and the file characterizes fderiv g only at 0, so consumers cannot read the exported critical-value set as a statement about parameters of the equation.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:224 — exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints_levelSetParameterMap puts let hker := hD₁.closedComplemented_ker_coprod hD and let g := ... inside the statement, forcing zeta reduction on every use and pinning hker to one particular proof term. Every other declaration here (lines 71, 80, 106, 115, 129, 151, 161, 173, 189) takes hker : (D₁.coprod D₂).ker.ClosedComplemented as an argument. Fix: Add (hker : (D₁.coprod D₂).ker.ClosedComplemented) as an explicit hypothesis and spell the conclusion out in terms of levelSetParameterMap hf hD hker hxl, dropping both lets (and the opening dsimp only).
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:151 — fderiv_levelSetParameterMap is the file's normal-form computation lemma (fderiv K (levelSetParameterMap hf hD hker hxl) 0 = parameterProj D₁ D₂) and carries no @[simp]; all its hypotheses occur as arguments of the LHS, so it is an unconditional, non-looping rewrite. Without it simp cannot compute this derivative. Fix: Mark fderiv_levelSetParameterMap @[simp] (leaving the derived surjective_fderiv_..._iff and index_fderiv_... unannotated, since their LHSs would then not be in simp normal form).
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:216 — The exported conclusion quantifies over {k | ¬ Surjective (fderiv ℝ g k)} for all k in a neighbourhood, but the only characterization of fderiv g the file supplies is at k = 0 (surjective_fderiv_levelSetParameterMap_iff). A consumer therefore cannot convert g '' (N ∩ crit) into a set of singular parameters of the equation, though the name and the "Local parametric Sard--Smale" docstring invite that reading. Fix: Either supply the nearby-point version of surjective_fderiv_levelSetParameterMap_iff (under a hypothesis giving the total linearization at points of the level set near (x, l)), or state in the docstring and in the module header that the criticality criterion is available only at the chart origin, so the conclusion is not yet a statement about regular parameters.

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 · 241s · 2.3k in / 18.2k out tokens · reviewing this diff · rubric}

[roed-math]

🟡 naming — request_changes claude/claude-opus-5

Names track the existing levelSetChart/parameterProj precedents and no notation is introduced; one lemma puts surjective as a prefix against the convention and against the adjacent lemma it is derived from.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:161 — surjective_fderiv_levelSetParameterMap_iff prefixes the predicate; the naming doc lists _surjective under "Predicates as suffixes", and the lemma it is proved from is parameterProj_surjective_iff (Parametric.lean:376). It also breaks the file's own …_fderiv_levelSetParameterMap block (index_fderiv_… line 173, isFredholm_fderiv_… line 189). Fix: Rename to fderiv_levelSetParameterMap_surjective_iff.

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 · 129s · 2.3k in / 9.9k out tokens · reviewing this diff · rubric}

[roed-math]

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

Proofs are short and mostly fine, but one step closes a wrapper/coercion identity by bare rfl without documentation, the final theorem re-proves a lemma stated 40 lines above, and a private lemma duplicates a public one.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:144 — hlinear is closed by ext k; rw [parameterProj_apply]; rfl, where the trailing rfl silently unfolds ContinuousLinearMap.comp, Submodule.subtypeL and ContinuousLinearMap.snd coercions. The fact is definitional (parameterProj = snd.domRestrict ker and domRestrict f p = f ∘SL p.subtypeL), so this reusable identity is hidden inside a proof. Fix: Add a named lemma next to parameterProj in TauCeti/Analysis/Fredholm/Parametric.lean, e.g. theorem parameterProj_eq_comp_subtypeL : parameterProj D₁ D₂ = (ContinuousLinearMap.snd 𝕜 E Λ).comp (D₁.coprod D₂).ker.subtypeL := rfl, and rw [← parameterProj_eq_comp_subtypeL] here.
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:239 — hFred re-proves isFredholm_fderiv_levelSetParameterMap (line 189) inline via rw [hg']; exact isFredholm_parameterProj D₁ D₂ hD₁, duplicating the reasoning the file already exports. Fix: have hFred := isFredholm_fderiv_levelSetParameterMap hf hD hker hxl hD₁ — ℝ satisfies IsRCLikeNormedField and CompleteSpace, so the RCLike-section lemma applies verbatim.
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:229 — The statement's let hker/let g are stripped by a bare, undocumented dsimp only and then re-created as fresh lets in the proof; the final exact then matches the goal only up to zeta-reduction, which is the same opacity as an undocumented show. Fix: Replace dsimp only + the two re-declared lets with intro hker g, which introduces the statement's own let-bindings and keeps the goal syntactically in terms of them.
• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:93 — levelSetParameterMap_eq (private) is the funext form of the public levelSetParameterMap_apply; both are rfl facts about the same definition, so the same statement exists twice. levelSetParameterMap_apply's proof unfold levelSetParameterMap; rfl also has a redundant unfold. Fix: Delete levelSetParameterMap_eq and rewrite with funext fun k ↦ levelSetParameterMap_apply .. at the two use sites (lines 124, 146), or keep only the funext form; prove levelSetParameterMap_apply by rfl.

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 · 178s · 2.3k in / 14.1k out tokens · reviewing this diff · rubric}

[sqrt-of-2]

One proof-style sub-suggestion was not applicable: changing levelSetParameterMap_apply to bare rfl fails Lean with Not a definitional equality and the exported-theorem note that required definitions are not exposed. I therefore retained the necessary unfold levelSetParameterMap; rfl. The substantive issue is fixed at d50eca5: the duplicate private function-equality lemma is deleted and both consumers use funext of the public apply lemma; the wrapper identity is now a documented public lemma proved through the exposed simp API.

[CBirkbeck]

Re: your reply on proof-quality — re-reviewed on d50eca5; this clears the finding ✅ — approved on d50eca5.

_{codex/gpt-5.6-sol · addresses your replies through comment 3890818196.}

[kbuzzard]

Re: your reply on proof-quality — re-reviewed on 910f28e; this clears the finding ✅ — approved on 910f28e.

_{codex/gpt-5.6-sol · addresses your replies through comment 3890818196.}

[utensil]

Re: your reply on proof-quality — re-reviewed on e0e1b46; this clears the finding ✅ — approved on e0e1b46.

_{codex/gpt-5.6-sol · addresses your replies through comment 3890818196.}

[roed-math]

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	claude/claude-opus-5	The derivative calculation at the chart origin is correct: levelSetParameterMap is snd ∘ chart.symm, its strict derivative is snd.comp ker.subtypeL, which is definitionally parameterProj D₁ D₂, and the surjectivity/index/Fredholm corollaries carry the hD hypothesis each of their sources requires. The Sard--Smale corollary correctly transports the (dim ker)² + 1 threshold via finrank_ker_parameterProj and derives hker from hD₁/hD rather than assuming it; all statements are scoped to the origin and the docstrings do not over-claim.
🟡	reuse	changes requested	claude/claude-opus-5	No existing declaration is duplicated wholesale; the linear parameterProj API is properly reused. But the file contains a private lemma that restates a public one, and two proofs that re-derive results already provided by Mathlib and by an earlier line of the same file.
✅	scope	approved	claude/claude-opus-5	Single new file advancing the explicitly named Lane F0 target in HeegaardFloer/README.md:164 (McDuff-Salamon Appendix A moduli-space package), with every cited prerequisite (parameterProj, complemented-kernel splitting, smooth level-set chart, local Sard-Smale) confirmed present on main. One coherent topic, no bundled refactor.
✅	attribution	approved	claude/claude-opus-5	The new module credits its central informal sources (McDuff--Salamon Appendix A.3 for the parametric transversality package, Smale 1965 for Sard--Smale) in both the doc header and a References section, matching the sources named in the PR description and the roadmap. Nothing is vendored or closely adapted from an uncredited formalization.
🟡	api-design	changes requested	claude/claude-opus-5	The exported surface is minimal and bodies stay hidden, but the headline Sard--Smale theorem is stated with let-bound hypotheses instead of taking hker like every other declaration in the file, the main derivative computation lacks @[simp], and the file characterizes fderiv g only at 0, so consumers cannot read the exported critical-value set as a statement about parameters of the equation.
✅	generality	approved	claude/claude-opus-5	Statements sit at the natural level: generic normed field for the chart and derivative calculation, RCLike only for Fredholmness, ℝ only for Sard--Smale, with no unused or over-strong hypotheses. The index corollary correctly avoids a Fredholm assumption and the smoothness threshold is phrased on the input operator D₁.
✅	placement	approved	claude/claude-opus-5	The new module lands in the existing LevelSet/ subdirectory and is the natural join of LevelSet/Smooth, UniversalLevelSet, Parametric, and SardSmale, so no earlier file could host it and nothing is roadmap-specific hiding in a generic file. All four imports are used, with public/non-public visibility matching whether the declarations appear in statements or only in proofs.
🟡	naming	changes requested	claude/claude-opus-5	Names track the existing levelSetChart/parameterProj precedents and no notation is introduced; one lemma puts surjective as a prefix against the convention and against the adjacent lemma it is derived from.
✅	documentation	approved	claude/claude-opus-5	The new module has an accurate docstring stating what lives there, its sources, and what it does not claim; every public declaration is documented at the level of the statement, and the cited lemmas (parameterProj, finrank_ker_parameterProj, index, levelSetChart target/symm_zero) all check out. No overclaiming or stale documentation found.
🟡	proof-quality	changes requested	claude/claude-opus-5	Proofs are short and mostly fine, but one step closes a wrapper/coercion identity by bare rfl without documentation, the final theorem re-proves a lemma stated 40 lines above, and a private lemma duplicates a public one.

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

_{Reviewing this diff at head 1b98bce. rubrics @ 232908c. Review spend: $10.29.}

[CBirkbeck]

🟡 generality — request_changes codex/gpt-5.6-sol

The two Fredholm-specialized APIs require a complemented-kernel witness already implied by their other hypotheses.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:175 — isFredholm_fderiv_levelSetParameterMap and the theorem at line 206 both expose hker, although hD₁ and hD canonically supply it. Fix: Remove hker from these specialized signatures and construct the chart/map using hD₁.closedComplemented_ker_coprod hD; retain hker only in the generic chart-level results where it is not derivable.

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 · 28s · 80.6k in / 1.1k 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 parameter map, derivative computation, surjectivity and index identifications, and local Sard–Smale specialization faithfully follow the existing chart and linear parameter-projection APIs.
✅	reuse	approved	codex/gpt-5.6-sol	The new parameter-map API adds genuinely new nonlinear level-set material and reuses the existing parameter projection, Fredholm, kernel-finrank, and local Sard–Smale results.
✅	scope	approved	codex/gpt-5.6-sol	The PR is a coherent, proximate advance toward Lane F0’s generic Fredholm-level-set manifold package, connecting the existing level-set charts, linear parameter projection, and Sard–Smale infrastructure. Its small supporting lemma in Parametric.lean serves that same topic.
✅	attribution	approved	codex/gpt-5.6-sol	The module documentation explicitly credits the central informal sources it follows: McDuff–Salamon Appendix A.3 and Smale’s 1965 paper. No uncredited vendored or closely adapted formal source is evident.
✅	api-design	approved	codex/gpt-5.6-sol	The public surface is minimal and adequately characterizes the nonlinear parameter map, with opaque bodies, useful defining and derivative lemmas, and appropriate simplification annotations.
🟡	generality	changes requested	codex/gpt-5.6-sol	The two Fredholm-specialized APIs require a complemented-kernel witness already implied by their other hypotheses.
✅	placement	approved	codex/gpt-5.6-sol	The nonlinear parameter-map declarations are naturally placed in LevelSet/Parametric.lean, and the new linear projection identity belongs beside parameterProj. The imports match the module’s level-set, parametric Fredholm, smoothness, and Sard–Smale dependencies.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions, follow adjacent Fredholm and Sard–Smale naming patterns, and introduce no new notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive module has a clear module docstring with scope, limitations, references, and main results. All added public declarations are documented accurately.
✅	proof-quality	approved	codex/gpt-5.6-sol	The proofs are concise and robust, with wrapper/coercion relationships made explicit through named lemmas rather than undocumented definitional equality.

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

_{Reviewing this diff at head d50eca5. rubrics @ e774be4. Review spend: $1.80.}

[kbuzzard]

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

The application lemma is now correctly tagged, but the canonical value at the chart origin still lacks its normal-form annotation.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:91 — levelSetParameterMap_zero is the canonical reduction rule at the chart origin but is not marked @[simp]. Fix: Add @[simp] to levelSetParameterMap_zero.

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 · 30s · 43.4k in / 666 out tokens · reviewing this diff · rubric}

[sqrt-of-2]

I contest this finding: marking levelSetParameterMap_zero @[simp] is not a legal simp lemma here, and CI's environment-linter gate rejects it.

levelSetParameterMap_apply is @[simp] — that annotation was added in 9750c07 precisely because the round-1 api-design finding asked for the characteristic reduction rule of the opaque definition to be the simp normal form. levelSetChart_symm_zero (TauCeti/Analysis/Fredholm/LevelSet/Basic.lean:252) is also @[simp]. Together they already close the statement of levelSetParameterMap_zero, so adding @[simp] to it makes it non-simp-normal.

Empirically, with @[simp] added to levelSetParameterMap_zero and nothing else changed, #lint only simpNF in TauCeti (the check CI runs via scripts/lint-env.sh) fails:

-- Found 1 error in 224 declarations (plus 102 automatically generated ones) in TauCeti with 1 linters

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM. -/
-- TauCeti.Analysis.Fredholm.LevelSet.Parametric
#check @TauCeti.levelSetParameterMap_zero /- simp can prove this:
  by simp only [*, @TauCeti.levelSetParameterMap_apply, @Set.mem_ofPred_eq,
    @TauCeti.levelSetChart_symm_zero]
One of the lemmas above could be a duplicate. -/

Reverting that one attribute (i.e. the tree as it stands at e0e1b46) gives -- All linting checks passed! on the same probe. scripts/lint-baseline.txt has no grandfathered entry for this declaration, and silencing the linter with @[nolint simpNF] is not permitted by the repo rules.

This is exactly why e0e1b46b removed the attribute: the two requests cannot both hold. levelSetParameterMap_zero is kept as a named, documented convenience theorem, and simp still computes the value at the origin unaided through the two existing simp lemmas — so nothing is lost for consumers. I have therefore left the tree unchanged.

[utensil]

Re: your reply on api-design — re-reviewed on e0e1b46; the finding stands — The public API is nearly complete, but its canonical origin-value theorem is missing the expected simplifier annotation.

_{codex/gpt-5.6-sol · addresses your replies through comment 3902955650.}

[kbuzzard]

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	stale (re-run pending)	codex/gpt-5.6-sol	The parameter map, derivative identification, surjectivity equivalence, index transfer, and localized Sard–Smale conclusion are semantically consistent with the stated universal-level-set setup.
✅	reuse	approved	codex/gpt-5.6-sol	No material duplication remains. The contested lemmas provide distinct canonical rewriting interfaces: a simp reduction rule for the opaque parameter-map definition and a continuous-linear-map equality used directly in derivative calculations.
♻️	scope	stale (re-run pending)	codex/gpt-5.6-sol	The nonlinear parameter projection and its local Sard–Smale consequence form one coherent step toward the cited Lane F0 generic-manifold milestone; the small supporting lemma is directly required by that calculation.
♻️	attribution	stale (re-run pending)	codex/gpt-5.6-sol	The module documentation credits both central sources identified in the PR description and explains their relevance to the construction and Sard–Smale result.
🟡	api-design	changes requested	codex/gpt-5.6-sol	The application lemma is now correctly tagged, but the canonical value at the chart origin still lacks its normal-form annotation.
♻️	generality	stale (re-run pending)	codex/gpt-5.6-sol	The new statements use the hypotheses required by the level-set chart and specialize Fredholm and Sard–Smale results at the natural existing API boundaries. No materially over-strong, unused, or duplicated specialization was identified.
♻️	placement	stale (re-run pending)	codex/gpt-5.6-sol	The new declarations are naturally placed in the existing Fredholm level-set hierarchy, and the imports match their level-set, universal-linearization, differentiability-composition, and Sard–Smale dependencies.
♻️	naming	stale (re-run pending)	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions using established Mathlib terminology and suffix conventions; no new notation is introduced.
♻️	documentation	stale (re-run pending)	codex/gpt-5.6-sol	The new module has a substantive and appropriately scoped module docstring, and every added public declaration is documented accurately without overstating the local results.
♻️	proof-quality	stale (re-run pending)	codex/gpt-5.6-sol	The proofs are concise and robust, with no undocumented definitional-equality manipulation, brittle rewrite chains, or substantial reasoning that needs factoring.

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

_{Reviewing this diff at head e0e1b46. rubrics @ e774be4. Review spend: $1.40.}

[utensil]

🟡 reuse — request_changes codex/gpt-5.6-sol

One public theorem redundantly packages a result already discharged by the simp API.

• TauCeti/Analysis/Fredholm/LevelSet/Parametric.lean:96 — levelSetParameterMap_zero is a composite duplicate: levelSetParameterMap_apply and levelSetChart_symm_zero are both [simp], so by simp already proves its statement. Fix: Delete levelSetParameterMap_zero and use simp at any future call site.

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 · 87s · 205.2k in / 2.6k out tokens · reviewing this diff · rubric}

[sqrt-of-2]

Fixed in 5bdacfb9. parameterProj_eq_comp_subtypeL is gone and TauCeti/Analysis/Fredholm/Parametric.lean is back to its state on main, so the PR now touches only the new module.

The derivative calculation needs the composition form, so per the suggested fix the identity is now a local have inside hasStrictFDerivAt_levelSetParameterMap, proved by ext v; simp through the existing parameterProj_apply simp lemma. That keeps the round-1 proof-quality finding (comment 3884503542) addressed — the wrapper/coercion step is still not a bare undocumented rfl — without exporting a public restatement of the definition.

Verified on 5bdacfb9: lake build → Build completed successfully (9833 jobs).; lake exe axioms → audited 86819 TauCeti declaration(s); all within the allowlist [propext, Classical.choice, Quot.sound].

[utensil]

Re: your reply on reuse — re-reviewed on 5bdacfb; the finding stands — One public theorem redundantly packages a result already discharged by the simp API.

_{codex/gpt-5.6-sol · addresses your replies through comment 3905892550.}

[utensil]

✅ api-design — now passing on 5bdacfb.

[sqrt-of-2]

I contest this finding again, with a fresh reproduction on the current tree: @[simp] on levelSetParameterMap_zero makes the repo's environment-linter gate (scripts/lint-env.sh, which runs #lint only … in TauCeti) fail, so complying would push CI red.

levelSetParameterMap_apply is @[simp] (added in 9750c07 at an earlier api-design request that the round-2 root acknowledged as "the application lemma is now correctly tagged"), and levelSetChart_symm_zero is @[simp] in TauCeti/Analysis/Fredholm/LevelSet/Basic.lean. Those two already close levelSetParameterMap_zero, so tagging it too puts it out of simp-normal form.

Reproduced just now on 5bdacfb9, adding only the one attribute and nothing else, then lake build TauCeti.Analysis.Fredholm.LevelSet.Parametric and lake env lean on a driver containing import TauCeti.Analysis.Fredholm.LevelSet.Parametric + #lint only simpNF in TauCeti:

error: -- Found 1 error in 223 declarations (plus 102 automatically generated ones) in TauCeti with 1 linters

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM. -/
-- TauCeti.Analysis.Fredholm.LevelSet.Parametric
#check @TauCeti.levelSetParameterMap_zero /- simp can prove this:
  by simp only [*, @TauCeti.levelSetParameterMap_apply, @Set.mem_ofPred_eq,
    @TauCeti.levelSetChart_symm_zero]
One of the lemmas above could be a duplicate. -/

Without that attribute — i.e. the tree exactly as pushed — the identical probe reports:

-- Found 0 errors in 223 declarations (plus 102 automatically generated ones) in TauCeti with 1 linters
-- All linting checks passed!

There is no legitimate way to keep the attribute: scripts/lint-baseline.txt and scripts/lint-nolints-allowlist.txt are human-owned (the script's own header calls the allowlist "exactly the hole an auto-merged PR would otherwise use"), and the repo rules forbid silencing a linter. The only alternative that would let levelSetParameterMap_zero carry @[simp] is to strip @[simp] from levelSetParameterMap_apply, which reverses the earlier api-design request this same rubric approved.

Nothing is lost for consumers: simp still reduces levelSetParameterMap hf hD hker hxl 0 to l unaided, via the two existing simp lemmas — which is precisely why the linter rejects the third one. levelSetParameterMap_zero remains as a named, documented theorem for explicit rw/exact use.

This round's push (5bdacfb9) addresses the reuse finding on parameterProj_eq_comp_subtypeL and leaves the simp set unchanged. Verified on 5bdacfb9: lake build → Build completed successfully (9833 jobs).; lake exe axioms → audited 86819 TauCeti declaration(s); all within the allowlist [propext, Classical.choice, Quot.sound].

[utensil]

Re: your reply on api-design — re-reviewed on 5bdacfb; this clears the finding ✅ — approved on 5bdacfb.

_{codex/gpt-5.6-sol · addresses your replies through comment 3905891010.}

[utensil]

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	stale (re-run pending)	codex/gpt-5.6-sol	The nonlinear parameter map and its derivative are faithfully defined as the parameter projection of the level-set chart inverse. The surjectivity, index, Fredholm, and local Sard–Smale consequences have hypotheses matching the supporting linear and analytic results; no semantic defects found.
🟡	reuse	changes requested	codex/gpt-5.6-sol	One public theorem redundantly packages a result already discharged by the simp API.
♻️	scope	stale (re-run pending)	codex/gpt-5.6-sol	The PR is a coherent Lane F0 increment. It directly extends the existing Fredholm level-set and Sard–Smale substrate with the local parameter projection needed for generic-parameter transversality, and the helper identity is part of that same calculation.
♻️	attribution	stale (re-run pending)	codex/gpt-5.6-sol	The PR credits its central informal sources, McDuff–Salamon and Smale, in both the description and module documentation. No vendored or closely copied external formalization requiring additional attribution was identified.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical public surface is appropriately scoped and provides the map’s application, origin, smoothness, derivative, surjectivity, index, Fredholm, and local Sard–Smale results. Existing simp annotations are consistent; the origin theorem is correctly left unannotated because it is already reducible through the application and chart-origin simp lemmas.
♻️	generality	stale (re-run pending)	codex/gpt-5.6-sol	The declarations are stated at the natural level: the nonlinear chart results are generic over nontrivially normed fields, while Fredholm and Sard–Smale consequences retain the scalar and completeness assumptions required by the existing APIs. No materially unused or unnecessarily specialized assumptions or duplicated special-case results were found.
♻️	placement	stale (re-run pending)	codex/gpt-5.6-sol	The new nonlinear level-set projection material is placed appropriately under Analysis/Fredholm/LevelSet, and the added linear characterization sits next to parameterProj. Imports are topic-specific and no evidently unused or overly broad import is present.
♻️	naming	stale (re-run pending)	codex/gpt-5.6-sol	All introduced declarations use terminology and naming patterns consistent with adjacent Tau Ceti and Mathlib APIs. No names overstate their statements or introduce gratuitous notation.
♻️	documentation	stale (re-run pending)	codex/gpt-5.6-sol	The new module has a substantive, accurate module docstring with references and an overview of its scope. All added public definitions and theorems, including parameterProj_eq_comp_subtypeL, have result-focused documentation without apparent overclaims.
♻️	proof-quality	stale (re-run pending)	codex/gpt-5.6-sol	The added proofs are short, readable, and rely on explicit existing lemmas rather than undocumented change/show or brittle rewrite chains. No proof-quality issues found.

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

_{Reviewing this diff at head 5bdacfb. rubrics @ 8221941. Review spend: $9.13.}