refactor(AmbientLattice): first-order correlationAlongExhaustion family equations and magnetization twin retirement by phasetr · Pull Request #4839 · phasetr/ising-model

phasetr · 2026-08-01T06:41:10Z

Progress on #4837 (stage A1 of the #4830 refactor programme).

Purpose

The six magnetizationAlongExhaustion regularity proofs in
IsingModel/AmbientLattice/SpecialCases/Magnetization.lean each unfolded
correlationAlongExhaustion and discharged its dite by hand
(simp only [hi, dif_pos] / dif_neg), and the same six statements existed a
second time, verbatim, as _gen-suffixed twins in
IsingModel/AmbientLattice/BetaDerivativeMagnetization.lean. Stage A1 gives the
case split a name, uses it, and removes the duplicates.

Changes

1. Two first-order family equations (new)

IsingModel/AmbientLattice/Exhaustion.lean, adjacent to the existing pointwise
correlationAlongExhaustion_of_subset / _of_not_subset:

correlationAlongExhaustion_family_eq_of_subset — for A ⊆ Λ.volume n,
(fun t => correlationAlongExhaustion G Λ (p t) A n) = fun t => correlationΛ G (Λ.volume n) (p t) (liftFinset A hA);
correlationAlongExhaustion_family_eq_zero_of_not_subset — for
A ⊄ Λ.volume n, the same family is the zero function.

The subset condition does not mention the family parameter, so the dite case
split factors out of any family p : α → IsingParams ℝ. Both are ordinary
equations between functions (hence rw-usable), and p is an explicit argument
so that rewriting never has to solve for a function-valued metavariable. No
@[simp]; documented against Glimm–Jaffe §4.6 (pp. 67–70) and §5.1 (pp. 72–75).

2. The six regularity proofs consume them

The by_cases hi : ({i} : Finset V) ⊆ Λ.volume n split in
magnetizationAlongExhaustion_{continuous, differentiable}_{beta, field, J}
now closes each branch with a plain rw of the corresponding family equation
instead of unfolding correlationAlongExhaustion. Both lemmas rewrote directly;
no have heq := ... fallback was needed.

3. Six duplicate `_gen` twins retired (deleted, no alias)

Removed from IsingModel/AmbientLattice/BetaDerivativeMagnetization.lean:
magnetizationAlongExhaustion_continuous_beta_general_h_gen,
_differentiable_beta_general_h_gen, _continuous_field_gen,
_differentiable_field_gen, _continuous_J_gen, _differentiable_J_gen.
Each was statement-identical (same binders, same conclusion) to the SpecialCases
survivor it duplicated. The two h = 0 corollaries
magnetizationAlongExhaustion_{continuous, differentiable}_beta_gen keep their
exact names but move to SpecialCases/Magnetization.lean, where they are
one-line instantiations of the general-h statements at h := 0. The module
docstring of BetaDerivativeMagnetization.lean is rewritten for its reduced
content: only the two HasDerivAt wrappers remain.

4. Concrete consumers repointed

Concrete/LatticeGraphCorrelation/MagnetizationPointwiseRegularity.lean and
MagnetizationPointwiseRegularityFieldJ.lean previously derived their six ℤ^d
pointwise wrappers from the deleted _gen twins via .continuousAt /
.differentiableAt. They now instantiate the ambient pointwise wrappers
magnetizationAlongExhaustion_{continuousAt, differentiableAt}_{beta, field, J}
(SpecialCases/Magnetization.lean:263-320) at G := IsingModel.latticeGraph d
directly. Those six ambient wrappers were reference-0 before this PR (on main
each occurs only at its own definition site). Imports
made dead by the change were dropped as reported by lake exe shake.

5. Documentation synchronized in this PR

docs/index.md: the Step 213 and Step 250 passages now state which names were
retired here and where the survivors live; the stale "reduce via
magnetizationAlongExhaustion_apply to correlationAlongExhaustion_*_gen"
claim for the h = 0 pair is replaced by the true derivation (instantiation of
the general-h statement at h := 0); the PR feat: along-exhaustion ContinuousAt + DifferentiableAt wrappers GJ-命題-bundle #1635 row records that the ℤ^d
concrete wrappers are now direct instantiations of the ambient *At_* ones.
tex/proof-guide.tex: the "already exist in BetaDerivative.lean under the
_gen suffix" passage is disambiguated — the correlation-side _gen wrappers
are untouched and still live in BetaDerivative.lean / BetaDerivativeFieldJ.lean,
while the magnetization-side ones are the unsuffixed statements in
SpecialCases/Magnetization.lean. A new \paragraph{} documents the two family
equations with the Glimm–Jaffe citations.
scripts/test_dead_candidate_scan.py: the declaration census pin moves
10571 → 10567 (net −4: eight declarations left
BetaDerivativeMagnetization.lean, six retired and two re-homed; four added —
the two re-homed corollaries and the two family equations) and one
tex/proof-guide.tex line anchor 26785 → 26821 is resynced mechanically.

6. Location claims corrected after cross review (`3b7c84f3`)

The cross-CLI review found three documentation statements that the retirement
left wrong, all fixed in the second commit: the module docstring called the
survivors "strictly more general" when every retired declaration was
proposition-identical to its survivor (the β pair included — it was already at
general h); the tex/proof-guide.tex PR #1628 paragraph placed the two
magnetizationAlongExhaustion_hasDerivAt_beta* wrappers in BetaDerivative.lean
while its own closing sentence placed them in BetaDerivativeMagnetization.lean
(the opening now records the PR #2063 move); and docs/index.md carried both
defects in the same row. The docs/index.md and tex/proof-guide.tex fixes are
in-place rewordings that keep the line counts identical, so the hardcoded
anchors in scripts/test_dead_candidate_scan.py stay valid.

Verification

All re-run on this branch at 3b7c84f3:

Gate	Result
`lake build IsingModel.AmbientLattice.Exhaustion`	PASS
`lake build IsingModel.AmbientLattice.SpecialCases.Magnetization`	PASS
`lake build IsingModel.AmbientLattice.BetaDerivativeMagnetization`	PASS
`lake build IsingModel.AmbientLattice`	PASS
`lake build IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationPointwiseRegularity`	PASS
`lake build IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationPointwiseRegularityFieldJ`	PASS
`lake build IsingModel.Concrete.LatticeGraphCorrelation.Umbrella.MagnetizationAndMayer`	PASS
`lake build` (root, 4944 jobs)	PASS, zero warnings
`lake exe GKSTest`	PASS
`python3 scripts/audit_gate.py --full`	PASS (V1–V4)
`python3 scripts/dead_candidate_scan.py --self-test`	PASS (139 tests)
`#print axioms` on all 14 new/changed declarations	`{propext, Classical.choice, Quot.sound}` only
`latexmk -pdf proof-guide.tex`	PASS (529 pages, no undefined control sequences)
`rg -n "[ぁ-んァ-ン一-龯]" tex/proof-guide.tex`	0 hits

lake exe shake still exits 1 on this repository's pre-existing backlog (329
file blocks). None of them names any module touched here, and neither
BetaDerivativeMagnetization nor either of its two importers appears in the
report, i.e. the import edits in this PR are shake-clean.

latexmk -lualatex (the recipe in README.md) fails in this environment with
(pdf backend): invalid font identifier when asking 'fontsize' during the
preamble. This reproduces identically on the unmodified main version of
proof-guide.tex, so it is a pre-existing local TeX Live issue and not a
regression from this PR; pdflatex compiles the modified file end to end.

Cross review

Reviewed with codex exec over git diff main...HEAD, two rounds. Round 1
returned four findings, no Lean-code defects among them; three were documentation
location claims and are fixed in 3b7c84f3 (§6 above). The fourth — that
docs/index.md:1828 still names the retired declarations and that the
scripts/test_dead_candidate_scan.py fixture keeps those tokens — was not
accepted: that line is the sentence documenting the retirement (the same wording
this table uses for the PR #4749 retirements), the fixture is a tokenizer test
rather than an existence claim, its neighbour at :952 guards the surviving
re-homed _beta_gen theorem, and the scanner reports coverage warnings: 0.
Round 2 verdict: approve, with the fourth point's reasoning accepted and the
three fixes confirmed.

Out of scope

Stage A2 (the hand-inlined case splits in AmbientLattice/BetaDerivative.lean
and BetaDerivativeFieldJ.lean) is untouched.

🤖 Generated with Claude Code

Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com

…ations) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…ly equations Progress on #4837 (stage A1). Adds the two first-order family equations for `correlationAlongExhaustion` next to the existing pointwise unfolding lemmas, migrates the six `magnetizationAlongExhaustion` regularity proofs onto them, and retires the duplicated `_gen` magnetization twins. * `AmbientLattice/Exhaustion.lean`: new `correlationAlongExhaustion_family_eq_of_subset` and `correlationAlongExhaustion_family_eq_zero_of_not_subset`. The subset condition does not mention the family parameter, so the `dite` case split factors out of a parameter family `p : α → IsingParams ℝ`. Both are plain equations between functions (usable by `rw`), with `p` explicit so that rewriting never solves for a function-valued metavariable. * `AmbientLattice/SpecialCases/Magnetization.lean`: the six global regularity wrappers now rewrite with the family equations instead of unfolding `correlationAlongExhaustion` and discharging `dif_pos` / `dif_neg` by hand; the two `h = 0` corollaries `magnetizationAlongExhaustion_{continuous,differentiable}_beta_gen` are re-homed here as instantiations of the general-`h` statements at `h := 0`. * `AmbientLattice/BetaDerivativeMagnetization.lean`: retires the six `_gen` twins (`_{continuous,differentiable}_beta_general_h_gen`, `_{continuous,differentiable}_field_gen`, `_{continuous,differentiable}_J_gen`), which duplicated the SpecialCases statements verbatim. The module keeps only the two `HasDerivAt` wrappers. * `Concrete/LatticeGraphCorrelation/MagnetizationPointwiseRegularity{,FieldJ}.lean`: the six ℤ^d pointwise wrappers now instantiate the ambient `magnetizationAlongExhaustion_{continuousAt,differentiableAt}_{beta,field,J}` wrappers directly (previously reference-0). * Imports made dead by the above were dropped, as reported by `lake exe shake`. * `docs/index.md` and `tex/proof-guide.tex` are synchronized in this commit; the declaration census pin and one `tex/proof-guide.tex` line anchor in `scripts/test_dead_candidate_scan.py` are resynced mechanically. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

… retirement Progress on #4837 (stage A1). Follow-up to b8e0dbb, from the cross-CLI review of PR #4839. * `AmbientLattice/BetaDerivativeMagnetization.lean`: the module docstring called the surviving `SpecialCases` statements "strictly more general" than the six retired `_gen` twins. They are not: each retired declaration was proposition- identical to its survivor, the beta pair included (it was already stated at general `h`). The docstring now says that. * `tex/proof-guide.tex`: the PR #1628 paragraph located the two `magnetizationAlongExhaustion_hasDerivAt_beta*` wrappers in `BetaDerivative.lean` while its own closing sentence, rewritten in b8e0dbb, put them in `BetaDerivativeMagnetization.lean`. The opening now records the PR #2063 move, so the paragraph no longer contradicts itself. * `docs/index.md`: the same row carried both defects -- the identical `BetaDerivative.lean` location for the `hasDerivAt` pair, and a "companion `Continuous*` / `Differentiable*` wrappers already present in `BetaDerivative.lean` under the `_gen` suffix" sentence that is now only true on the correlation side. Both are corrected in place, so no line numbers move and the hardcoded anchors in `scripts/test_dead_candidate_scan.py` stay valid. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…its to the family equations Progress on #4837 (stage A2). Completes stages A1+A2 of #4837. Migrates every hand-inlined `by_cases A ⊆ Λ.volume n` block in the two `correlationAlongExhaustion` regularity modules onto the first-order family equations added by stage A1 (PR #4839). * `AmbientLattice/BetaDerivative.lean` (4 declarations) and `AmbientLattice/BetaDerivativeFieldJ.lean` (4 declarations): each of the 16 branches (8 subset, 8 non-subset) previously built a local `have heq : (fun t => correlationAlongExhaustion ...) = ...` by `funext` plus a pointwise `correlationAlongExhaustion_of_{subset,not_subset}` rewrite, then `rw [heq]`. Each is now a single `rw` by `correlationAlongExhaustion_family_eq_of_subset` resp. `correlationAlongExhaustion_family_eq_zero_of_not_subset`, followed by the pre-existing closer verbatim. The subset closers discharge the resulting `correlationΛ` goal by defeq (`correlationΛ` is a `def` for `IsingModel.correlation (inducedGraph G Λ)`), so no `correlationΛ_apply` step is needed. * Proof-only: all 8 theorem statements, names, binders and `by_cases` hypothesis names are byte-identical; no declaration is added or removed. * Count correction: issue #4837 estimated "approximately 12" hand-inlined case splits. The remeasurement it mandates gives 8 declarations containing 16 blocks. The estimate is superseded, not silently corrected; its plausible origin is 8 plus the 4 β-direction thin wrappers in `BetaDerivative.lean`, which carry no case split. * Module docstrings and the `correlationAlongExhaustion_hasDerivAt_beta` doc comment now name the family equations instead of describing a hand unfold. * `docs/index.md` and `tex/proof-guide.tex` are synchronized in this commit. While updating the Step 205/209/212 cells, three stale file paths naming `AmbientLattice/BetaDerivative.lean` for declarations moved to `AmbientLattice/BetaDerivativeFieldJ.lean` by PR #2064 were corrected. * One `tex/proof-guide.tex` line anchor in `scripts/test_dead_candidate_scan.py` is resynced mechanically (26821 -> 26835, +14 lines from the two tex edits), exactly as PR #4839 resynced 26785 -> 26821. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…se splits to the first-order family equations (#4837 stage A2) (#4840) Progress on #4837 (stage A2). Completes stages A1+A2 of #4837. Stage A1 (PR #4839) added the first-order family equations `correlationAlongExhaustion_family_eq_of_subset` and `correlationAlongExhaustion_family_eq_zero_of_not_subset` (`IsingModel/AmbientLattice/Exhaustion.lean`) and migrated the six `magnetizationAlongExhaustion` regularity proofs onto them. Stage A2 migrates the remaining hand-inlined case splits in the two `correlationAlongExhaustion` regularity modules, which were explicitly out of scope in A1. ## Count correction (superseded, not silently fixed) Issue #4837 estimated "approximately 12" hand-inlined case splits in these two modules. The remeasurement that A2 mandates gives, on `6147071c`, **8 `by_cases A ⊆ Λ.volume n` declarations containing 16 hand-inlined `have heq` blocks** (8 subset + 8 non-subset). The "~12" estimate is **superseded, not silently corrected**; its plausible origin is 8 plus the 4 β-direction thin wrappers in `BetaDerivative.lean`, which carry no case split and were never in A2's scope. `.self-local/issues/4837.md` carries the same correction. ## The 8 declarations | File | Declaration | Family λ | |---|---|---| | `AmbientLattice/BetaDerivative.lean` | `correlationAlongExhaustion_hasDerivAt_beta` | `fun β' => ⟨J, 0, β'⟩` | | | `correlationAlongExhaustion_hasDerivAt_beta_general_h_gen` | `fun β' => ⟨J, h, β'⟩` | | | `correlationAlongExhaustion_continuousAt_beta_general_h_gen` | `fun β' => ⟨J, h, β'⟩` | | | `correlationAlongExhaustion_differentiableAt_beta_general_h_gen` | `fun β' => ⟨J, h, β'⟩` | | `AmbientLattice/BetaDerivativeFieldJ.lean` | `correlationAlongExhaustion_continuousAt_field_gen` | `fun h' => ⟨J, h', β⟩` | | | `correlationAlongExhaustion_differentiableAt_field_gen` | `fun h' => ⟨J, h', β⟩` | | | `correlationAlongExhaustion_continuous_J_gen` | `fun J' => ⟨J', h, β⟩` | | | `correlationAlongExhaustion_differentiable_J_gen` | `fun J' => ⟨J', h, β⟩` | The 6 thin wrappers in `BetaDerivative.lean` and the 2 in `BetaDerivativeFieldJ.lean` (`_continuous_field_gen`, `_differentiable_field_gen`) have no case split and are untouched. ## Invariants (this is a proof-only change) * `git diff -U0 main...HEAD` over the two modules contains **no** `[-+]theorem` line and no changed binder line: all 8 statements, names, binders and `by_cases` hypothesis names are byte-identical. * No declaration added or removed; the declaration census is unchanged. * 8 occurrences of `correlationAlongExhaustion_family_eq_of_subset` and 8 of `correlationAlongExhaustion_family_eq_zero_of_not_subset` across the two files; `funext` and `have heq` occurrences are now 0 in both. * Lean diffstat: 56 insertions, 96 deletions. ## Verification | Gate | Result | |---|---| | `lake build` (full, 4944 jobs) | pass, 0 warnings (`warningAsError = true`) | | `lake exe GKSTest` | all tests passed | | `python3 scripts/audit_gate.py --full` | PASS | | `python3 scripts/dead_candidate_scan.py --self-test` | OK, 139 tests | | `#print axioms` on all 8 migrated theorems | `[propext, Classical.choice, Quot.sound]` for each | | `rg -n "[ぁ-んァ-ン一-龯]" tex/proof-guide.tex docs/index.md` | 0 matches | | codex cross-review | round 1 Request changes (3 doc-accuracy findings, fixed in 86178a4), round 2 **Approve** | Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: Codex <noreply@openai.com>

Follow-up to 0a52f59 after independent review. Documentation only: Lean doc comments, `docs/index.md` rows, and `tex/proof-guide.tex`. No statement, proof term, or public name changes. 1. Off-by-one in the identical-statement group. The pilot canonicalizes three of *four* declarations that share the statement, not three of three. `freeEnergyComplexAlongExhaustion_closedBallBranchDeviationRelCompact_patch` (`ClosedBallPatches/RelCompact.lean`, PR #2745) carries the byte-identical statement as well, but was deliberately excluded from the pilot: it proves the statement by the independent `toDeviationData` route into `freeEnergyComplexAlongExhaustion_branchDeviationRelCompact_patch`, and it still has its own in-repo consumers (`BranchLocallyBoundedPatches/ RelCompact.lean`, its own `_of_isCompact`, and the Z^d wrapper). The owner doc comment, the excluded theorem's doc comment, the two `docs/index.md` rows, and the PR #2745/#2752/#2756/#2768 proof-guide theorem environments now say "owner for the three pilot-scoped declarations" and disclose the fourth instead of implying an exhaustive three-element group. 2. Stale construction path in the PR #2756 proof-guide environment. It stated that the direct-range endpoints build their relatively compact range data "through the PR #2757 direct-route data alias". Since 0a52f59 none of the three endpoints listed there calls `toRangeRelCompactData_direct`: the abstract one forwards to the owner, the `_of_isCompact` one calls the abstract one, and the positive-real one calls the `_of_isCompact` one; the owner calls `toRangeRelCompactData_closedBallLocal_direct`. The data alias itself remains in use by the other closed-ball conversions (`toRangeRelCompactData_viaDeviation_direct` and the eventual-overlap conversion), so it is not orphaned. The sentence now states the actual post-PR path. 3. Correction to the 0a52f59 commit message (left as pushed; not rewritten). It justified keeping `...ClosedBallBranchDeviationAscoliData.toRangeRelCompactData_viaLocal_direct` with the blanket claim "this repo does not run reference-0 deletion campaigns". That claim is false: deliberate zero-consumer deletions have happened repeatedly (272b310/#4641, 3fbc873/#4749, 051aa85/#4751, f891116/#4764), as have duplicate retirements (6147071/#4839, 2613222/#4851), and `lean-coding-conventions` points the other way (reference-0 declarations are decorative and should generally be removed). The real, narrower reason is that removing or re-pointing that declaration is outside the minimal scope of the #4854 pilot. The `docs/index.md` rows and the via-local proof-guide environment are reworded to that narrower claim and now say explicitly that this is a scope statement about this PR, not a general exemption for reference-0 declarations. Verification: `lake build` full, zero warnings and zero errors; `lake exe GKSTest` passes; `latexmk -g -pdf proof-guide.tex` clean with zero Overfull/Underfull boxes, zero LaTeX/package warnings and zero undefined references; no Japanese characters in the proof guide. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…dit ratchet (#4830 AC4) (#4871) * docs: qualify the four bare .lean citations #4839/#4840 introduced `scripts/citation_audit.py` fails its ratchet with four `BASENAME_ONLY` findings above the committed baseline, so #4830's AC4 ("build/GKSTest/audit gate/#print axioms/documentation & citation checks pass with zero warnings") cannot be satisfied while they stand. All four are prose this session's own merged children wrote: #4839 (`6147071c`) named the retired-duplicate files by basename when describing where the surviving wrappers live, and #4840 (`e3a0dc01`) did the same for the migrated case-splitting theorems. R4 charges a citation that resolves to exactly one file but carries no `/`, because a basename is not evidence: it happens to be unique today and stops being a citation the moment a homonym lands. Give each one the directory it already had in the sentence next to it, so the fix is a spelling change and nothing about which file is meant: * `docs/index.md` -- `BetaDerivativeFieldJ.lean` (twice) -> `AmbientLattice/BetaDerivativeFieldJ.lean`, the spelling the same document already uses at the §17.5 row; * `docs/index.md` -- `MagnetizationPointwiseRegularityFieldJ.lean` -> `Concrete/LatticeGraphCorrelation/MagnetizationPointwiseRegularityFieldJ.lean`, matching its sibling named in the same clause; * `tex/proof-guide.tex` -- `\texttt{BetaDerivativeMagnetization.lean}` and `\texttt{BetaDerivativeFieldJ.lean}` -> `\path{IsingModel/AmbientLattice/...}`, the spelling the same paragraph already uses two sentences later. The two guide edits wrap onto their own lines and push everything below them down by three, which moves the second row `QualifiedGlobCitationTest` hard-pins; repin 26910 -> 26913 against the position measured by the scanner's own `load_docs()`, renaming the attributes with the number as in `6f363d44`. The counts 13/7/20 and the 4/1/4/4/7 resolution shape are unchanged: this is a coordinate fix, not a weakening of the test. Ratchet now passes (31 cleared, 0 new); no `.lean` file is touched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs: keep the qualified BetaDerivativeMagnetization citation inside the margin PR #4871's qualification of the bare `BetaDerivativeMagnetization.lean` citation put a 58-character `\path{...}` in the middle of a clause, where TeX could not break it: the box ran 89.17pt past the right margin (plus a 9.15pt knock-on box further down the same paragraph), taking the repo-wide Overfull count from 771 to 772. Reorder the clause so the path ends it -- "moved by PR #2063 to the file <path>:" -- which is the shape the paragraph's other `\path` citations already have. The citation token itself is untouched, so `citation_audit.py` still resolves it (R1, one component-aligned match) and no bare basename comes back. Measured with `latexmk -g -pdf` on the whole guide: the paragraph now has zero Overfull boxes (main had one, 3.33pt; this branch before the fix had two, 89.17pt and 9.15pt), and the document total goes 772 -> 770. Diffing the full ordered list of Overfull overshoots against a main build shows a single deletion and no other movement, so nothing was pushed elsewhere. The rewrap costs one source line, so the `tex/proof-guide.tex` citation the scanner test pins moves 26913 -> 26912; repinned as measured through the scanner's own `load_docs()`. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

phasetr and others added 3 commits August 1, 2026 15:40

chore: start stage A1 of #4837 (correlationAlongExhaustion family equ…

63a96b1

…ations) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

phasetr marked this pull request as ready for review August 1, 2026 08:09

phasetr merged commit 6147071 into main Aug 1, 2026
4 of 8 checks passed

phasetr deleted the refactor/4837-a1-correlation-family-equations branch August 1, 2026 08:12

phasetr mentioned this pull request Aug 1, 2026

refactor(AmbientLattice): migrate the 8 correlationAlongExhaustion case splits to the first-order family equations (#4837 stage A2) #4840

Merged

This was referenced Aug 1, 2026

[P0 refactor] Replace correlationAlongExhaustion case-split boilerplate with first-order family equations #4837

Closed

[P1 refactor] Simplify architecture and retire technical debt; treat build speed as a supporting metric #4830

Closed

This was referenced Aug 3, 2026

refactor: canonicalize closedBallBranchDeviation aliases (#4854 audit-gate pilot) #4868

Merged

docs: qualify the four bare .lean citations that fail the citation-audit ratchet (#4830 AC4) #4871

Merged

phasetr mentioned this pull request Aug 3, 2026

refactor: retire the duplicate toRangeRelCompactData_viaLocal_direct (#4869) #4876

Merged

Navigation Menu

refactor(AmbientLattice): first-order correlationAlongExhaustion family equations and magnetization twin retirement - #4839

refactor(AmbientLattice): first-order correlationAlongExhaustion family equations and magnetization twin retirement#4839
phasetr merged 3 commits into
mainfrom
refactor/4837-a1-correlation-family-equations

phasetr commented Aug 1, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

phasetr commented Aug 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Purpose

Changes

1. Two first-order family equations (new)

2. The six regularity proofs consume them

3. Six duplicate _gen twins retired (deleted, no alias)

4. Concrete consumers repointed

5. Documentation synchronized in this PR

6. Location claims corrected after cross review (3b7c84f3)

Verification

Cross review

Out of scope

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

phasetr commented Aug 1, 2026 •

edited

Loading

3. Six duplicate `_gen` twins retired (deleted, no alias)

6. Location claims corrected after cross review (`3b7c84f3`)