refactor(ldt): de-tacticize main induction fields - #2639
Conversation
|
@codex review |
|
@claude review |
|
Codex Review: Didn't find any major issues. Another round soon, please! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
There was a problem hiding this comment.
Pull request overview
This PR completes the MainInductionStep portion of the #2599 de-tacticization effort by replacing the remaining tactic-style proof fields embedded in record/structure literals with term-mode proofs, while keeping public statements and computational content unchanged.
Changes:
- Replaced remaining tactic-mode record-field proofs in
MainInductionSteptheorems with term-mode rewrites (▸),Prod.ext, and direct lambdas. - Factored the strong self-consistency derivation into a narrow private helper lemma that only consumes the required
SDDRelwitness. - Simplified several small “restrictedGood” fields to direct constructors (
fun _ => ⟨le_rfl, …⟩) and tightened equivalence inverses to explicitProd.extproofs.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| MIPStarRE/LDT/MainInductionStep/Theorems/StageDataConstructors.lean | Converts slice-restriction proof fields to term-mode via equality transport (▸) and removes now-unnecessary simpa blocks. |
| MIPStarRE/LDT/MainInductionStep/Theorems/SelfImprovementAssembly/Core.lean | Extracts strongSelfConsistency_of_sddRel helper and rewrites the induction-section conclusion constructor as a record literal with term-mode fields. |
| MIPStarRE/LDT/MainInductionStep/Theorems/SelfImprovementAssembly/AnswerSlice.lean | Replaces a tactic proof of covariance transport invariance with a term proof using an existing transport lemma. |
| MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/Core.lean | Converts restrictedGood field to a direct term-mode lambda constructor. |
| MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/Base.lean | Rewrites pointAppendProdEquiv inverse proofs in term mode using Prod.ext and existing append/truncate lemmas. |
| MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/AnswerValued.lean | Converts restrictedGood fields in answer-valued restricted probability statements to term-mode lambdas. |
| MIPStarRE/LDT/MainInductionStep/Theorems/MainTheorems/Base.lean | Replaces small equivalence inverse proofs in the base cases with Prod.ext + Subsingleton.elim term proofs. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
|
@codex review |
|
@claude review |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Category A — Blueprint ↔ Lean equivalence: ✅ Clean
This PR is a pure proof-body refactoring (tactic-mode → term-mode). It:
- Changes no Lean declaration signatures
- Adds no
sorry,admit, oraxiom - Modifies no blueprint
.texfiles - Renames or removes no public declarations
The existing \leanok on \lean{MIPStarRE.LDT.MainInductionStep.mainInductionBaseCase} / \lean{MIPStarRE.LDT.MainInductionStep.answerMainInductionBaseCase} (ch10_induction.tex:243–245) remains valid — the statement signatures are unchanged and the proofs contain no sorry.
The new private theorem strongSelfConsistency_of_sddRel is a pure proof factoring with no blueprint entry needed.
0 equivalence mismatches, 0 stale \leanok, 0 stale \notready.
Category B — Prose quality: ✅ Clean
- No banned software-engineering terms (
pipeline,wrapper,package,raw,oneShot,liveBlock) in the diff. - No banned LLM writing patterns.
- No new Lean jargon in prose — the PR adds no docstrings, comments, or prose of any kind.
- The existing Copilot comment about the missing docstring on
strongSelfConsistency_of_sddRelis already raised and not a banned-language violation.
0 prose issues.
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
There was a problem hiding this comment.
Review: refactor(ldt): de-tacticize main induction fields
Verdict: Approve. This is a pure proof-refactoring PR — it replaces by blocks in structure/Equiv construction fields with term-mode proofs across seven MainInductionStep modules. I verified there is no source-statement drift: every change is confined to proof bodies and field values; no public signature, hypothesis, conclusion, error parameter, or quantifier structure is altered. No sorry or axiom is introduced. CI reports a successful lake build.
Checks performed
- Source-statement fidelity (🔴): clean.
selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusion(SelfImprovementAssembly/Core.lean:106),mainInductionBaseCase/answerMainInductionBaseCase,pointAppendProdEquiv, the*RestrictedProbabilitiesStatement.ofWeightedBoundslemmas,dummyDiagonalCovariantMeasurement, andSliceRestrictionData.ofAnswerall keep their exact prior signatures. Only field-value proofs changed. - New helper
strongSelfConsistency_of_sddRel(Core.lean:63): this is not a proof-debt bundle or conditional wrapper. It is an unconditional lemma factoring out the pre-existing inline strong-self-consistency derivation; its hypothesishclose : SDDRel …is the genuine closeness input that was alreadyhfinal.selfClosenessin the prior proof. The paper-facing theorem that calls it retains its original statement, so no source-statement drift is introduced. - Proof correctness (🔴): the term-mode replacements are faithful —
Prod.ext rfl (Subsingleton.elim _ _)for theAxisParallelTestSample ≃ Pointinverses;fun _ => ⟨le_rfl, le_rfl, le_rfl⟩forrestrictedGood;▸rewrites inSliceRestrictionData.ofAnswerin place ofsimpa(relying on definitional unfolding of the*_eqequalities);sub_nonneg.mp (hfinal.dualDominatesAveragedPoint h)fordominatesAveragePointOperator; andtransportInvariantvia the existingProjMeas.transport_trivialDistinguishedOutcome+DiagonalLinePolynomial.reparamAt_default(both confirmed present in the tree). All typecheck under the passing build. - Type safety / performance: term-mode fields remove several
simp/simpainvocations, which is neutral-to-positive for elaboration cost. No new instances or coercions introduced.
Advisory (non-blocking)
- ℹ️
strongSelfConsistency_of_sddRel(Core.lean:63) has no docstring. It is a private, single-use proof-factoring helper, so this is not a documentation-policy violation, but a one-line doc comment (mirroring the neighboringmainInductionOfWitness) would aid maintenance. This was already raised by Copilot and that thread was resolved by the author, so I am not re-posting it inline.
No 🔴 or 🟡 issues found.
There was a problem hiding this comment.
Review Summary
This is a clean, correct proof refactor that de-tacticizes 22 fields across 7 modules by converting by blocks to term-mode proofs. There are no blockers — every change is mathematically equivalent to the original, and all files compile.
✅ Verification checklist
| Category | Verdict | Notes |
|---|---|---|
| 🔴 Proof integrity | Pass | No sorry or axiom introduced; all proofs preserve the same statement. |
| 🔴 Proof correctness | Pass | Every refactored proof is mathematically equivalent to the original. |
| 🔴 Source-statement fidelity | Pass | No public statement signatures changed. |
| 🟡 Mathlib style | Pass | Term-mode fun _ => preferred over by intro;; Prod.ext rfl (Subsingleton.elim _ _) is idiomatic. |
| 🔴 Type safety | Pass | No type mismatches; definitional equalities correctly identified. |
| 🟡 Performance | Improved | Term-mode proofs are generally lighter than tactic blocks. |
| 🟡 Modularity | Pass | Private strongSelfConsistency_of_sddRel helper appropriately isolates the SDD→bipartite-SSC transport. |
| 🟡 Documentation | Pass | New helper has a docstring; existing docstrings unchanged. |
Key changes examined
-
selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusion(Core.lean): The direct field assignments replacingsimpablocks are valid because:selfImprovementInInductionErrorignores its_gammaargument (it is an underscore-prefixed binder), soselfImprovementError params eps delta = selfImprovementInInductionError params eps delta 0is definitionally equal toselfImprovementInInductionError params eps delta gamma.projectiveBoundednessGapunfolds toev strategy.state (projectiveResidualOperator ...), andprojectiveResidualOperatorunfolds to the sameleftTensor * rightTensorexpression thattensorFailureExpectationuses — sobounded := hfinal.projectiveResidualBoundtype-checks.averagedPointOperatorandIdxPolyFamily.averagedPointEvaluationOperatorboth unfold toaverageOperatorOverDistribution (uniformDistribution (Point params)) (fun u => (strategy.pointMeasurement u).toSubMeas.outcome (h u))— sodominatesAveragePointOperator := fun h => sub_nonneg.mp (hfinal.dualDominatesAveragedPoint h)is correct.
-
dummyDiagonalCovariantMeasurement(AnswerSlice.lean):transportInvariantusesProjMeas.transport_trivialDistinguishedOutcomeandDiagonalLinePolynomial.reparamAt_defaultas a direct chain, replacing the oldsimp-based proof. Correct. -
SliceRestrictionData.ofAnswer(StageDataConstructors.lean): The▸-based casts using the*_eqlemmas are equivalent to the previoussimpaproofs; theaxisAverageBound/selfAverageBound/diagonalAverageBounddirect assignments work because thelet profile := ...binder is transparent to definitional reduction. -
Equivalence
left_inv/right_inv(Base.lean, RestrictedProbabilities/Base.lean): Correctly usesProd.extandSubsingleton.elimin term mode.
Resolved previous feedback
The Copilot review thread about the missing docstring on strongSelfConsistency_of_sddRel was addressed in commit 44e5657 — the docstring /-- Convert same-register closeness ... into bipartite strong self-consistency. -/ is present.
Verdict: ✅ APPROVE
No 🔴 or 🟡 issues found. This is a well-executed, mathematically sound refactor that improves code quality by 48 net lines.
There was a problem hiding this comment.
Review: Category A & B only — refactor(ldt): de-tacticize main induction fields
Verdict: ✅ APPROVE. No issues in either category.
Category A — Blueprint ↔ Lean equivalence: ✅ Clean (0 issues)
This PR is a pure proof-body refactoring (tactic→term) across 7 files. It changes no declaration signatures, no blueprint .tex, and no \lean{...}/\leanok/\notready tags. The only new declaration is private, so it needs no blueprint entry.
- A.1 Mathematical equivalence. All statement signatures are unchanged. The main theorem
selfImprovementInInductionSection(Core.lean:148) retains the same hypotheses, quantifiers, and conclusion as its blueprint entrythm:self-improvement-in-induction-section(ch10_induction.tex:71–108). The error parameterselfImprovementInInductionErrorhas an unused_gammabinder (Defs.lean:484), soSelfImprovement.selfImprovementError params eps deltais definitionally equal toselfImprovementInInductionError params eps delta gamma— the direct field assignments in the refactored proof are equivalent to the oldsimparewrites. - A.2
\leanokaccuracy. The statement\leanok(line 73) and proof\leanok(line 111) both remain valid. Nosorry,admit, oraxiomin any changed file. - A.3
\notreadyaccuracy. No\notreadytags in scope. - A.4 Tag presence. No new public declarations needing blueprint entries; no renames/removals.
Category B — Prose quality: ✅ Clean (0 issues)
The only new prose in the diff is the docstring on strongSelfConsistency_of_sddRel (Core.lean:63):
Convert same-register closeness of a projective submeasurement into bipartite strong self-consistency.
Checked against the banned-terms tables in docs/mathematical_language.md:
- No Lean jargon, no software-engineering terms (
pipeline,wrapper,package,raw,oneShot,liveBlock). - No banned LLM writing patterns.
- All terminology ("same-register closeness", "projective submeasurement", "bipartite strong self-consistency") is mathematically descriptive and aligns with the paper's vocabulary.
All other changes are pure code (term-mode proofs) with no new comments or prose.
Previous feedback
The Copilot review thread (missing docstring) was resolved by commit 44e5657; the thread is already marked resolved.
Summary: 0 equivalence mismatches, 0 stale \leanok, 0 stale \notready, 0 prose issues.
There was a problem hiding this comment.
Review: refactor(ldt): de-tacticize main induction fields — Approve
Proof-only refactor (#2599 batch): 22 proof-valued construction fields across seven MainInductionStep modules converted from by-blocks to term-mode. Reviewed against the 🔴/🟡 categories, emphasis on proof integrity and source-statement fidelity.
Source-statement fidelity 🔴 — clean
- No public signature changed.
selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusion(paper originreferences/ldt-paper/self_improvement.tex:631-811,\label{thm:self-improvement}) keeps its exact hypotheses/conclusion and merely becomes a direct structure literal. - The
simpa [selfImprovementError, selfImprovementInInductionError] using hfinal.X→hfinal.Xreplacements (completeness,pointConsistency,selfCloseness,bounded) rely on definitional equality of the error terms; the greenbuildjob confirms defeq holds. No weakened conclusion or altered error parameter.
Proof integrity 🔴 — clean
- The new
private theorem strongSelfConsistency_of_sddRelis not a proof-debt bundle / conditional helper / wrapper in the flagged sense: it is fully proved (nosorry), takes exactly theSDDRelwitness already available at the call site (hfinal.selfCloseness), and reproduces the prior inline derivation verbatim. Genuine proof factoring that preserves content; docstring makes the SDD→bipartite-SSC transport clear. - No
sorry/axiomintroduced (proof-debt audit, proof-evasion audit, axiom check all green).
Proof correctness 🔴 — clean
dominatesAveragePointOperator := fun h => sub_nonneg.mp (hfinal.dualDominatesAveragedPoint h)correctly rewrites0 ≤ A - BtoB ≤ A.- Equiv
left_inv/right_invconversions (e.g.pointAppendProdEquiv) match thetoFun/invFuncomponent structure viaProd.ext+truncatePoint_appendPoint/pointHeight_appendPoint. AnswerSlice.leantransport now uses the reusableProjMeas.transport_trivialDistinguishedOutcome+reparamAt_default— cleaner and more modular.
Other categories
- Style/type-safety/performance: term-mode proofs are idiomatic;
▸rewrites inStageDataConstructors.leanare localized and compile; net −48 lines, no timeout risk. - Documentation: the one prior reviewer request (docstring on
strongSelfConsistency_of_sddRel) was addressed in 44e5657.
No 🔴 or 🟡 issues found. Approving.
Summary
Completes the final folder-scoped batch for #2599 by replacing all remaining genuine proof-valued construction fields in
MainInductionStepwith term-mode proofs.completenessandaxisParallelTest)SDDRelwitnesssorryoraxiomThis exhausts the corrected syntax-context audit for the umbrella issue.
Closes #2599.
Verification
lake build MIPStarRE(8992 jobs)git diff --checkNote
Low Risk
Proof-only refactors in formal Lean with preserved types and no new axioms; risk is limited to accidental proof breakage, which the described build checks are meant to catch.
Overview
Completes the MainInductionStep batch for de-tacticizing proof-valued construction fields: 22 fields across seven modules now use term-mode proofs instead of
byblocks, with no change to public signatures or computational data.Pattern changes: equivalence proofs (
left_inv/right_inv) are shortened withProd.extandSubsingleton.elim; failure-profilerestrictedGoodfields usefun _ => ⟨le_rfl, le_rfl, le_rfl⟩; answer-slice restriction proofs use definitional equality (▸) instead ofsimpa; dummy diagonal transport usesProjMeas.transport_trivialDistinguishedOutcomeinstead of a localsimpproof.Self-improvement assembly: the Section 9 → Section 6 transport is refactored so
selfImprovementInInductionSectionConclusion_ofSelfImprovementConclusionis a direct structure literal; strong self-consistency is isolated in privatestrongSelfConsistency_of_sddRel, and dual dominance usessub_nonneg.mpon the averaged-point witness.Reviewed by Cursor Bugbot for commit 44e5657. Bugbot is set up for automated code reviews on this repo. Configure here.