TwoD: refactor SemiDegenerate + PureQuartic through AddSeparable (Tide 13)#16
Open
dmurfet wants to merge 2 commits into
Open
TwoD: refactor SemiDegenerate + PureQuartic through AddSeparable (Tide 13)#16dmurfet wants to merge 2 commits into
dmurfet wants to merge 2 commits into
Conversation
Refactor the two existing 2D files to use the Laplace.TwoD.AddSeparable abstraction landed in Tide 12, instead of re-deriving the partition factorisation and integral_pow_pow_factor case-by-case. Public theorem statements unchanged; only internal proofs change. Three pieces: 1. AddSeparable.lean: drop the unused integrability hypotheses on `partitionFunction_addSeparable_factor` and `integral_separable_addSeparable` (the proof bodies are unchanged since `MeasureTheory.integral_prod_mul` is unconditional). The `gibbsExpectation_separable_addSeparable` and `gibbsCov_addSeparable_fst_snd_eq_zero` lemmas also lose the no-longer-needed weight integrability hypotheses; the `≠ 0` hypotheses on the partition functions stay (those are load-bearing). 2. SemiDegenerate.lean: add `[simp]` bridge lemma `semiDegeneratePotential_eq_addSeparable` and rewrite the proofs of `partitionFunction_factor` and `integral_pow_pow_factor` as one-line applications of the AddSeparable lemmas through the bridge. The `exp_neg_t_semiDegenerate_eq_mul` lemma becomes a corollary of `exp_neg_t_addSeparable_eq_mul` via the bridge. 3. PureQuartic.lean: same refactor with `pureQuarticPotential_eq_addSeparable`. Net delta: −22 lines across the three files, 0 sorry/axiom/native_decide. The headline `cov_affine_*` theorems and the moment lemmas (`gibbsExpectation_fst`/`snd`/`fst_mul_snd`/`fst_sq`/`snd_sq`) are unchanged and continue to build through the refactored proofs. Tide deliberation log: sri/projects/primer/tide-log/2026-05-06-tide-twod-cleanup.md Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5-page narrative covering the deliberation, the bridge-lemma + simp_only refactor strategy, the worktree-isolated tide run as the first concrete demonstration of the structural fix to the recurring concurrent-agent branch race, the Mathlib-vs-new accounting (nothing new from Mathlib; just two bridge lemmas of new content), lessons, and follow-ups. Includes the deliberate API regression on AddSeparable.lean dropping the integrability hypotheses that Tide 12 added as discipline (Tide 13's concrete refactor demonstrates that the discipline blocked rather than helped downstream callers). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Refactors
Laplace/TwoD/SemiDegenerate.leanandLaplace/TwoD/PureQuartic.leanto use the generic separable-potential factorisation introduced intide/separable-potential(AddSeparable.lean), which has just merged.Both 2D files were independently re-deriving the partition-function and observable factorisations for separable potentials
L(x,y) = U(x) + V(y). TheAddSeparableinfrastructure abstracts that pattern once, and this refactor specialises both 2D files to it.Per-tide retrospective at
retrospectives/2026-05-06-tide-twod-cleanup.tex.Test plan
lake buildclean.scripts/sorriesclean.cov_affine_semiDegenerate,cov_affine_pureQuartic) preserved verbatim with the new generic backend.🤖 Generated with Claude Code