This document captures conventions and review criteria distilled from the project’s refactoring rounds. It is applied as the review checklist for every pull request, not only refactor PRs.
The knowledge is grouped by phase / category so that reviewers can locate the relevant criteria quickly.
The following table is the canonical menu of test idioms used in this project. Each PR that adds or changes tests should be checkable against it.
| Method | Code shape | Use |
|---|---|---|
| A. decide-based universal | example : ∀ x : Fin n, P x := by decide |
Pin the meaning of a finite, Decidable predicate. Most refactor-resistant. |
B. matrix entry-wise on small Fin n |
ext i j; fin_cases i <;> fin_cases j <;> simp [defn_apply] |
Cross-check small matrix-valued definitions. Catches meaning changes immediately. |
| C. bridge identity | example : defn_A = defn_B := rfl |
Pin the consistency of two definitions of the same object. Refactor detector. |
| D. signature-preservation shim | example : <type> := named_thm args |
Limited to public API freeze. Survives rename only of the body, not of the name. |
E. Plausible |
(POC only) | Not primary. Generator integration cost is high for our ℂ / matrix setting. |
F. #guard_msgs |
/-- expected msg -/ #guard_msgs in <command> |
Pin diagnostic output: @[deprecated] warnings, intended failures, linter behaviour. Not for theorem regression. |
G. small exhaustive (Fin n; fin_cases) |
example : ∀ x : Fin n, P x := by intro x; fin_cases x <;> simp |
Pin meaning of a parameterised lemma on a small but complete sample. The most refactor-resistant for parameterised statements. |
Primary axis: A + C + G. Limited use: D, B. Niche: F. Not primary: E.
For canonical examples of methods A / B / C / F / G in
working code, see LatticeSystem/Tests/Foundation.lean —
the test-method POC file from Phase 0 (#280). Each method has
a labelled subsection with at least one minimal example.
When a PR introduces or modifies tests, the reviewer checks:
ℂ props
are not Decidable).Module split criteria, all four required:
Each split module retains a façade module that re-imports the new files. This preserves backward-compatible import paths:
LatticeSystem/Quantum/NeelState.lean -- façade (re-imports NeelState.*)
LatticeSystem/Quantum/NeelState/Definition.lean
LatticeSystem/Quantum/NeelState/Definition2D.lean
...
Old import LatticeSystem.Quantum.NeelState works unchanged.
Core.lean sub-pattern (cycle avoidance)When the original module’s bulk stays put and only a new
feature file is extracted, the naive façade pattern would
require the new feature file to import the (now-trimmed)
original — and the original-as-façade would import the new
feature file. That is a cycle.
The fix: rename the (trimmed) original to <Module>/Core.lean
and create a fresh <Module>.lean façade that imports both
<Module>/Core.lean and the new feature file:
LatticeSystem/Quantum/SpinDot.lean -- façade (~30 lines)
LatticeSystem/Quantum/SpinDot/Core.lean -- bulk of original
LatticeSystem/Quantum/SpinDot/Hamiltonian.lean -- new feature
Now Hamiltonian.lean imports SpinDot.Core (not SpinDot),
and SpinDot.lean (façade) imports both. No cycle.
When to use: any time the new sub-file would need to import the original file’s content (which, if not renamed, would be the façade).
Origin: PR #317 (SpinDot/Hamiltonian extraction). See the cumulative roadmap history Phase 2 entries for cumulative usage.
When the parent file already contains the core concept and the sub-file extends it with derived material (eigenvalue calculations, companion-theorem families, additional algebraic structure that doesn’t fit the parent’s responsibility), the parent stays as content (not turned into a façade) and the sub-file imports the parent. Downstream code that wants the extension content imports the sub-file directly. The parent’s module-header docstring must list the extension sub-files in a table.
LatticeSystem/Quantum/HeisenbergChain.lean -- content
LatticeSystem/Quantum/HeisenbergChain/Eigenvalues.lean -- extension
LatticeSystem/Quantum/HeisenbergChain/Gibbs.lean -- extension
Now Eigenvalues.lean and Gibbs.lean import HeisenbergChain,
and HeisenbergChain.lean does not import them. Users who
just need the basic chain Hamiltonian + Hermiticity import
Quantum.HeisenbergChain; users who want the eigenvalue or Gibbs
companion family import the specific sub-file. This keeps the
parent file’s import surface small.
When to use vs Core.lean sub-pattern: use content + extensions when the parent’s identity as a content-bearing module is more important than convenience for downstream; use Core.lean when you want a single import to give the full module surface.
Examples in this codebase:
TotalSpin.lean + TotalSpin/Casimir.lean + TotalSpin/Rotation.leanHeisenbergChain.lean + HeisenbergChain/Eigenvalues.lean
HeisenbergChain/Gibbs.leanSpinHalfRotation.lean + SpinHalfRotation/Conjugation.leanGibbsState.lean + GibbsState/Covariance.leanTimeReversalMulti.lean + TimeReversalMulti/SpinOpEquivariance.lean
TimeReversalMulti/Heisenberg.leanWhen extracting a helper lemma from one file to another, if the
helper is referenced by other downstream files, it must be lifted
from private lemma to lemma at extraction time. Document the
visibility change in the PR body.
Examples:
spinHalfSign_mul_antiparallel from
private lemma to public theorem so the new generic
inner_neelStateOf_szsz_neelStateOf_antiparallel could use it.
Also documented in the interim legacy catalogue per §6 below._aux private lemmas had to be lifted
when their parent file was split (e.g., prod_alternating_neg_one,
onSite_conjTranspose). Each PR body explicitly documented the
visibility change with a one-line “Visibility lift” note.[simp] lemmas surveyed before split (cross-file
dependencies on global simp set noted).When consolidating duplicated patterns:
(hpart : G.IsBipartiteWith s t) with s t : Set V).σ : V → Bool) for simp ergonomics.IsBipartite (Colorable 2) at entry points;
prefer the explicit IsBipartiteWith witness form.When generalising a definition, keep the specialised version
with a @[deprecated <replacement> (since := "YYYY-MM-DD")]
annotation. The deprecation window is at least one minor version
of the project (or one feature-cluster of subsequent PRs).
Concrete current policy: 6 months from since — see
deprecations.html for the live tracking
table, removal-PR checklist, and current entries.
Do not deprecate until all bridge lemmas are in place and verified.
When @[deprecated] cannot use a target name (because the
generic replacement requires a lambda argument the deprecation
syntax can’t express), use the message form
@[deprecated "use the generic ... with the ... indicator ..."
(since := "YYYY-MM-DD")] to give callers a concrete migration
hint.
Internal companion theorems on the deprecated name continue to
exist (they are the migration scaffolding). Suppress the
deprecation linter for the block of companions immediately after
the deprecated declaration with a single
set_option linter.deprecated false and a comment explaining
why. Tests that exercise the deprecated names for backward-compat
coverage do the same at file level (test files exempt). The
deprecation warning text itself is captured by #guard_msgs
(method F) at the end of the test file.
@[deprecated ... (since := ...)] annotation present with
explicit date.#guard_msgs test pinning the deprecation
warning text (per §1 method F).inner_basisVec_spinHalfDot_basisVec_antiparallel (52 chars)
are at the edge — acceptable only if no shorter alternative
exists.def / noncomputable def / theorem / lemma must
have a docstring.Tasaki §2.5 eq. (2.5.3), p. 37).set_option linter.* false in source files
(test files exempt only with comment justification).set_option linter.flexible false in etc. are
acceptable only when no proof-level rewrite achieves the goal;
must include comment explaining why. Track every remaining
per-theorem suppression in docs/deprecations.md
for transparency.lake build should produce zero linter warnings in steady
state.linter.unusedSectionVars / linter.unusedDecidableInType:
use omit [Fintype Λ] in or omit [DecidableEq Λ] in directly
before the affected theorem, instead of a file-level
set_option. The variable is still in scope as a variable
declaration; omit just tells Lean not to auto-include it in
this specific theorem’s signature.linter.deprecated triggered by internal companions on a
deprecated definition: place a single
set_option linter.deprecated false after the deprecated
declarations and before the companion theorems with a comment
pointing to the deprecation rationale. The companions are
migration scaffolding (see §3 “Deprecation window” above).linter.unusedSimpArgs: trim the dead arguments. If the
argument is needed in some sub-cases of a <;>-chained simp
but not others, accept the warning per-theorem with comment
rather than refactoring into separate per-case proofs.linter.flexible (simp [...] after fin_cases): ideally
refactor to simp only [...] with the explicit lemma list
(use simp? interactively to find it), or use suffices to
state the simplified form. Per-theorem
set_option linter.flexible false in with comment is
acceptable as a temporary measure when interactive simp? is
not available.set_option linter.* false introduced (without
comment justification).omit [...] directives preferred over
set_option linter.unused* false.lake build warning count not increased (record before /
after in PR description if relevant).docs/deprecations.md
transparency table.For every PR adding def / theorem / lemma, the same PR must:
docs/formalization/legacy/
(Lean name + statement + file + citation). This is the interim update path
until Issue #5228 performs the structured-data cutover.tex/proof-guide.tex if relevant.This is enforced by review and not by CI.
When chaining git commit && git push inside a single background
shell command, the git push step can fail silently — for
example due to a transient network error or an interrupted
background task — without aborting the chain or surfacing the
failure on subsequent commands. The PR API will then report a
successful merge of an empty diff, silently dropping the
intended changes.
git push (especially in chained / background
invocations), verify with git ls-remote origin <branch>
that the remote SHA matches the local HEAD.gh pr merge, run git pull on main and confirm
the expected files are present (ls the new file paths).Origin: PR #311 (intended JordanWigner Operators extraction) merged with empty diff; redone via PR #312.
This document is itself the single source of truth for review criteria. When new conventions emerge (e.g., from a Phase 2 split surfacing a new pitfall), the convention is added here in the same PR that demonstrates it.
The goal is that anyone reviewing a PR can apply this checklist mechanically and catch most regressions / drift.
lake env lean LatticeSystem/Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIILocalSigns.lean,
measured real 17.19s (user 3.67s, sys 3.46s) on the first run and
real 5.71s (user 3.62s, sys 1.97s) on a warm rerun. The structural
sign-transfer and shifted-matrix files measured real 4.22s and real 3.70s,
while the block PF/min bridge measured real 4.00s. The warm local-sign time
and small downstream times do not justify a module split yet; the first run is
tracked as dependency/cache cost. The PR therefore keeps the checkpoint narrow
and removes one now-unnecessary set_option linter.style.longLine false in
wrapper from the case-(ii) block PF/min bridge.lake env lean LatticeSystem/Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean
completed in real 5.59s (user 8.22s, sys 1.65s), and
lake env lean LatticeSystem/Quantum/SpinS/AnisotropicHeisenbergSpinSObligation2FromSU2Unique.lean
completed in real 3.82s (user 2.88s, sys 1.53s). Both are below the
prior PR #4070 measurement and well below the recorded roughly-18s threshold
for reconsidering a split of Theorem24SU2GlobalUniquenessFromMLM.lean, so
no module split was performed. The PR also removed unnecessary
set_option linter.style.longLine false in wrappers from the recent general
spin-S target/obligation modules after focused Lean checks showed they were
no longer needed.Quantum/SpinS module:
lake env lean LatticeSystem/Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean
completed in real 15.83s (user 9.13s, sys 3.29s) on updated
main. A preliminary size survey also measured the next largest
Quantum/SpinS files at roughly 4–5s focused elaboration, so
Theorem24SU2GlobalUniquenessFromMLM.lean is the only near-threshold file.
No module split was performed: the consumer-facing SU(2)-endpoint theorems
are a suffix of the same proof chain, but they depend on the zero-Casimir,
outside-sector, common-energy, and sector-PF infrastructure earlier in the
file. A suffix extraction would therefore create a serial parent/suffix
dependency rather than an independent parallel build target, while adding
import churn to the active Theorem 2.4 / Problem 2.5.c consumers. Revisit a
real split if this file persistently exceeds about 18s or if a future theorem
creates an independent downstream-facing endpoint cluster.lake env lean LatticeSystem/Quantum/SpinS/Theorem23Final.lean
completed in real 9.02s (user 4.39s, sys 3.68s);
lake env lean LatticeSystem/Quantum/SpinS/Theorem23OutsideGround.lean
completed in real 7.99s (user 9.93s, sys 3.74s);
lake env lean LatticeSystem/Quantum/SpinS/Theorem23IntervalCasimirMinimality.lean
completed in real 7.77s (user 3.02s, sys 3.62s);
lake env lean LatticeSystem/Quantum/SpinS/SaturatedLadderJointEigenspace.lean
completed in real 6.33s (user 4.48s, sys 3.43s);
cached lake build LatticeSystem.Quantum.SpinS.Theorem23Final
completed in real 3.73s (user 1.76s, sys 2.60s). No module split
was performed: the newest work routed public final wrappers through the
common-energy boundary, but the measured focused elaboration times remain
below the previous split trigger range and the remaining public route audit
is still actively moving.lake env lean LatticeSystem/Quantum/SpinS/Theorem23OutsideGround.lean
completed in real 17.13s (user 3.29s, sys 4.10s);
lake env lean LatticeSystem/Quantum/SpinS/Theorem23Final.lean
completed in real 6.93s (user 2.43s, sys 3.15s);
lake env lean LatticeSystem/Quantum/SpinS/Theorem23Sectors.lean
completed in real 9.07s (user 3.13s, sys 2.88s);
cached lake build LatticeSystem.Quantum.SpinS.Theorem23OutsideGround
completed in real 3.71s (user 1.68s, sys 2.37s). No module
split was performed: the active wrapper files are modest in size
(Theorem23OutsideGround.lean 526 lines, Theorem23Final.lean
403 lines, Theorem23Sectors.lean 262 lines), and the newest side-case
callbacks are still close to the final admissible-reach boundary. The
next extraction should wait until the outside-sector callback chain either
lands in the final Theorem 2.3 proof body or exposes a stable heavier
suffix.Theorem23DominancePredictedGS.lean now keeps the
three adjacent predicted-GS successor common-energy steps (293 lines), while
Theorem23DominancePredictedGSPredecessor.lean contains the predecessor
common-energy step (100 lines). The new module imports the parent (the
predecessor step reuses a successor step). The predecessor step has no Lean
importer, so the new module is wired into LatticeSystem.lean per
[[tasaki23-tree-wired-into-build-root]] (job count 3292 → 3293).Theorem23SectorExistenceInterval.lean now keeps the
off-A/on-A dominance and lowered-site-sum interval chains (287 lines),
while Theorem23SectorExistenceIntervalMarshall.lean contains the
lowered-vector-Marshall interval chain (106 lines). The new module imports
the parent (the Marshall chain reuses the lowered-site-sum chain). The sole
consumer (Theorem23FinalLoweredMarshall) adds a direct import of the new
module.Theorem23.lean now keeps the adjacent common-energy successor steps
(212 lines), while Theorem23CommonEnergyPredecessor.lean contains the two
predecessor common-energy steps (site-sum / Casimir-non-kernel) (186 lines).
The new module imports the parent (the predecessor steps are independent of
the successor steps but reuse the same upstream API). Both consumers
(Theorem23Dominance, Theorem23PredictedCasimirEnergy) also use the
successor steps, so they switch their Theorem23 import to the new module
(which re-exports the parent transitively).Theorem23PredictedSourceWeight.lean now keeps the Ŝ^3
source-weight building blocks (172 lines), while
Theorem23PredictedSourceWeightCross.lean contains the four re-embedded
cross-ladder source-weight identities at a lowering predecessor (278 lines).
The new module imports the parent. The private
magSumS_single_site_lowering_predecessor helper is duplicated into the new
module (same per-module private-copy pattern). Consumers of the moved
identities (Theorem23OutsideGroundPredecessorRaising, Theorem23Interval,
Theorem23OutsideGroundPredecessor) switch their import to the new module;
the Ŝ^3 building-block consumers
(Theorem23OutsideGroundCrossLadderReembedded and its Unpacked) keep
importing the parent.Theorem23FinalLoweredSiteSum.lean now keeps the source predicted-GS
lowered-site-sum final wrappers (260 lines), while
Theorem23FinalLoweredSiteSumLeft.lean contains the left-endpoint threaded
predicted-GS lowered-site-sum final wrapper and the two named-callback
abbrevs (159 lines). The new module imports the parent (the named-callback
abbrev reuses a source final wrapper). The new module is an orphan tip (no
Lean importer), so it is wired into LatticeSystem.lean per
[[tasaki23-tree-wired-into-build-root]] so the default lake build / CI
elaborates it (job count 3288 → 3289).Theorem23LocalDifferenceRaising.lean now keeps the raw single-site raising
component formulas (165 lines), while
Theorem23LocalDifferenceRaisingPositivity.lean contains the single-site
raising positivity/negativity, non-negativity/non-positivity, and the
off-A/on-A raised sign-sum bounds (298 lines). The new module imports the
parent. The private magSumS_single_site_raising_successor helper is
duplicated into the new module (same per-module private-copy pattern as in
PR #3532). Only Theorem23LocalDifferenceRaisingSiteSum consumes the moved
theorems; it switches its import to the new module.Theorem23OutsideGroundCrossLadderLoweredJoint.lean now keeps the
lowered-joint magnetization-subspace component / coefficient final wrappers
(212 lines), while
Theorem23OutsideGroundCrossLadderLoweredJointCross.lean contains the
lowered-joint cross-ladder component / coefficient final wrappers (218
lines). The new module imports the parent (the cross-ladder wrappers reuse
the magSubspace-component final wrapper). Only
Theorem23OutsideGroundCrossLadderUnpacked consumes a moved wrapper; it
switches its import to the new module.Theorem23Local.lean now keeps the lowered-direction
ladder/site-sum machinery (361 lines), while
Theorem23LocalRaisedSiteSum.lean contains the three raised-direction
site-sum expansion theorems (total + on-A + off-A) (101 lines). The new
module imports the parent. Consumers Theorem23LocalDifferenceMarshall
(total raised expansion) and Theorem23Predicted (two sublattice raised
expansions) each add a direct import of the new module (they previously
reached the theorems transitively through the parent).Theorem23LocalDifferenceUnpacked.lean now keeps the lowered Marshall
positivity theorem (208 lines), while
Theorem23LocalDifferenceUnpackedSiteSum.lean contains the strict lowered
site-sum positivity theorem and the callback-adapter abbrev (232 lines). The
new module imports the parent (the site-sum theorem reuses the lowered
Marshall positivity theorem). Only Theorem23Interval consumes the moved
declarations; it switches its import to the new module.
Theorem23IntervalCallbacks imports the parent but uses none of its
declarations and is left unchanged.Theorem23LocalLowering.lean now keeps the raw
single-site lowering component formulas and the signed coefficient identities
(303 lines), while Theorem23LocalLoweringPositivity.lean contains the
single-site positivity (off-A) / negativity (on-A) theorems (194 lines).
The new module imports the parent. The private
magSumS_single_site_lowering_predecessor helper is duplicated into the new
module (the existing codebase already keeps per-module private copies in
Theorem23LocalLowering, Theorem23PredictedSourceWeight, and
Theorem23LocalCoefficient), since a private declaration is not visible
across the new module boundary. Consumers: Theorem23LocalLoweringSignSum
switches its import to the new module; Theorem23LocalDifferenceRaising adds
an import; Theorem23LocalDifferenceSiteSum reaches it transitively.Theorem23SectorExistenceDominance.lean now keeps
the successor/predecessor predicted-Casimir dominance wrappers (230 lines),
while Theorem23SectorExistenceDominancePredictedGS.lean contains the
successor/predecessor predicted-GS dominance wrappers (228 lines). The new
module imports the parent and is itself a leaf endpoint; the parent has no
other Lean consumer than this new suffix. Focused per-module
lake build / lake env lean checks verify both (these tip modules are not
in the default lake build closure, so per-module checks are the real
verification).Theorem23PredictedLadder.lean now keeps the
predicted-GS lowering/raising closures, the lowered sublattice-Casimir
bridges, and the joint sublattice-Casimir / lowered joint-magnetization
definitions (365 lines), while Theorem23PredictedLadderJointExtract.lean
contains the four extractor lemmas unpacking tasaki23LoweredJointMagSubspace
membership (98 lines). Focused checks cover the split modules and the
interval / cross-ladder unpacked downstream modules. Build-speed: the parent
module’s focused lake env lean dropped to ~6.9s (it was the heaviest
active Theorem 2.3 module).Theorem23LocalCoefficient.lean now keeps the predecessor/coefficient
definitions and the positive-source coefficient theorems (317 lines), while
Theorem23LocalCoefficientSignedSum.lean contains the signed-coefficient
identities (signed predecessor coefficient = positive-source coefficient,
signed lowering site-contribution = ±coefficient, and the off-A/on-A
filtered signed-lowering sum identities) (166 lines). Focused checks cover
the split modules and the local-difference / outside-ground predecessor
downstream modules.Theorem23LocalCoefficientRaisingSource.lean now keeps the
lowerable-positive-source coefficient bridges (158 lines), while
Theorem23LocalCoefficientRaisingSourceSum.lean contains the
tasaki23RaisingPredecessorSourceCoefficient definition and the
raising-predecessor-source sum / positivity / dominance machinery and final
callback (326 lines). Focused checks cover the split modules and the local
difference / outside-ground predecessor difference downstream modules.Theorem23LocalDifferenceEnergy.lean now keeps the base adjacent-sector
energy step and the with-nonzero packages (232 lines), while
Theorem23LocalDifferenceEnergyCasimir.lean contains the
Casimir-non-vanishing and site-sum-positivity adjacent-sector packages
(254 lines). Focused checks cover the split modules and the Theorem23.lean
downstream module.Theorem23IntervalJoint.lean now keeps the joint-component, lowered-joint
magSubspace-component, and lowered-joint cross-ladder-component wrappers
(335 lines), while Theorem23IntervalJointUnpacked.lean contains the
unpacked lowered-joint cross-ladder wrapper (161 lines). Focused checks
cover the split modules and the outside-ground cross-ladder unpacked
downstream module.Theorem23SectorExistence.lean now keeps the Theorem 2.3 statement, the
base per-sector existence step, and the successor sector-existence chain
links (384 lines), while Theorem23SectorExistencePredecessor.lean contains
the predecessor sector-existence chain link with the raised
predicted-Casimir variant (123 lines). Focused checks cover the split
modules and the sector-existence dominance downstream module.Theorem23OutsideGroundCrossLadderReembedded.lean now keeps the basic
re-embedded cross-ladder source-sector site-sum and source-weight final
wrappers (315 lines), while
Theorem23OutsideGroundCrossLadderReembeddedUnpacked.lean contains the
unpacked re-embedded source-weight final wrapper (178 lines). Focused checks
cover the split modules and the outside-ground predecessor downstream module.Theorem23OutsideGroundPredictedGS.lean now keeps the left-endpoint
predicted-GS off-A/on-A dominance final wrappers (213 lines), while
Theorem23OutsideGroundPredictedGSLoweredMarshall.lean contains the
left-endpoint threaded predicted-GS lowered-Marshall final wrappers and the
outside-real-sector wrapper (298 lines). Focused checks cover the split
modules and the outside-ground cross-ladder downstream module.Theorem23Final.lean now keeps the outside-ground
final-boundary aliases (161 lines), while
Theorem23FinalLoweredSiteSum.lean contains the direct lowered-site-sum
final wrappers and named-callback aliases (395 lines). Focused checks cover
the split final modules and the lowered-Marshall downstream module.Theorem23OutsideGroundPredictedCasimir.lean now keeps the source
predicted-Casimir final wrappers (259 lines), while
Theorem23OutsideGroundPredictedCasimirThreaded.lean contains the
left-endpoint threaded predicted-Casimir final wrappers (269 lines). Focused
checks cover the split modules and the predicted-GS downstream module.Theorem23Interval.lean now keeps the direct interval-chain
wrappers (349 lines), while Theorem23IntervalCallbacks.lean contains the
named left-endpoint predicted-GS, source predicted-GS,
predecessor-difference, and lowered-site-sum callback propositions (217
lines). Focused checks cover the split interval modules and representative
downstream final-boundary consumers.Theorem23IntervalCasimir.lean now keeps the dominance-form
predicted-Casimir interval chains (314 lines), while
Theorem23IntervalCasimirSiteSum.lean contains the lowered site-sum and
lowered Marshall suffix (267 lines). Focused checks cover the split
interval-Casimir modules and the outside-ground predicted-GS downstream
module.Theorem23OutsideGround.lean now
keeps the outside-sector lower-bound callbacks, sector-minimality bridge,
and common-energy final packaging, while
Theorem23OutsideGroundConditional.lean contains the conditional
final-wrapper suffix. Focused checks cover the split outside-ground modules
and the predicted-Casimir / predicted-GS downstream modules.Theorem23OutsideGroundPredecessor.lean now keeps the source-weight and
positive-source final-wrapper layers, while
Theorem23OutsideGroundPredecessorLowerable.lean contains the lowerable and
explicit lowerable final-wrapper suffix consumed by the real source-weight
and raising-source downstream module. Focused checks cover the split
predecessor modules and the predecessor-difference downstream module.Theorem23.lean now keeps the site-sum and
Casimir-nonvanishing adjacent common-energy links, while
Theorem23PredictedCasimirEnergy.lean contains the predicted-Casimir
adjacent common-energy and ladder-image packages consumed by the dominance
and sector-existence layers. Focused checks cover the split base /
predicted-Casimir modules and the dominance / sector-existence downstream
consumers.Theorem23LocalDifference.lean
now keeps the sublattice coefficient and predecessor raising-source
difference identities, while Theorem23LocalDifferenceUnpacked.lean
contains the fully threaded unpacked callback adapters consumed by the
interval and outside-ground wrappers. Focused checks cover the split local
difference modules and the interval / outside-ground downstream consumers.Theorem23OutsideGroundCrossLadder.lean now keeps the sublattice-component,
joint-component, and joint-coefficient final-wrapper layers, while
Theorem23OutsideGroundCrossLadderLoweredJoint.lean contains the
lowered-joint suffix. Focused checks cover the split cross-ladder modules and
the unpacked / re-embedded downstream modules.Theorem23IntervalCasimir.lean now keeps
the predicted-Casimir interval-chain wrappers (559 lines), while
Theorem23IntervalCasimirMinimality.lean contains the minimality bridge and
named callback suffix (152 lines). Focused checks cover the split
interval-Casimir modules and the outside-ground / final downstream modules.Theorem23PredictedLadder.lean now keeps
the predicted-GS ladder closure, joint sublattice-Casimir structure, and
lowered joint-magnetization package (437 lines), while
Theorem23PredictedLadderCasimirTransfer.lean contains the
scalar-cancellation and total-Casimir transfer suffix (249 lines). Focused
checks cover the split predicted-ladder modules and the dominance /
sector-existence downstream consumers.Theorem23Final.lean now keeps the outside-ground and direct
lowered-site-sum final boundaries (536 lines), while
Theorem23FinalLoweredMarshall.lean contains the lowered-vector-Marshall
final suffix (256 lines). Focused checks cover the split final modules and
downstream outside-ground predicted-GS documentation references.Theorem23Interval.lean kept the named callbacks and direct
interval-chain wrappers at that point (543 lines), while
Theorem23IntervalPredictedGS.lean contains the predicted-GS-aware interval
suffix (242 lines). Focused checks cover the split interval modules and the
joint interval downstream consumer.Theorem23SectorExistence.lean now keeps the final
theorem proposition, per-sector Theorem 2.2 wrapper, and predicted-Casimir
existential packages (483 lines), while
Theorem23SectorExistenceDominance.lean contains the dominance-form
sector-existence suffix (433 lines). Focused checks cover the split modules
and interval-chain downstream modules.Theorem23LocalCoefficient.lean now keeps the lowered signed and
positive-source coefficient layers (457 lines), while
Theorem23LocalCoefficientRaisingSource.lean contains the predecessor
raising-source suffix (459 lines). Focused checks cover the split modules and
the local-difference / outside-ground predecessor downstream modules.Theorem23Dominance.lean now keeps the base and
predicted-Casimir dominance layers (323 lines), while
Theorem23DominancePredictedCasimirTransfer.lean contains the successor
predicted-Casimir transfer suffix (269 lines). Focused checks cover the split
modules and the interval-Casimir downstream module.Theorem23LocalDifferenceRaising.lean now keeps the single-site raising
components and weak filtered sign bounds (398 lines), while
Theorem23LocalDifferenceRaisingSiteSum.lean contains the named
contribution, strict off-A witness, vacancy bridge, and dominance-form
raised site-sum positivity wrapper (168 lines). Focused checks cover the
split modules and dominance / sector-existence downstream modules.Theorem23Predicted.lean now keeps the canonical
predicted-GS and cross-ladder bridges, while
Theorem23PredictedEndpoint.lean contains the lowering/raising real
endpoint inequalities and complex endpoint-mismatch wrappers. Focused checks
cover the split modules and the predicted-Casimir adjacent-energy consumer.Theorem23Dominance.lean now keeps the base dominance and
predicted-Casimir dominance layers (568 lines), while
Theorem23DominancePredictedGS.lean contains the predicted-GS dominance
suffix (369 lines). Focused checks cover the split modules and the
sector-existence downstream module.Theorem23Predicted.lean now keeps the
predicted-Casimir, predicted-GS, and cross-ladder bridge layer (559 lines),
while Theorem23PredictedSourceWeight.lean contains the diagonal
source-weight and lowering-predecessor bridge suffix (384 lines). Focused
checks cover the split modules and the interval / outside-ground downstream
modules.Theorem23OutsideGroundPredecessor.lean now keeps the source-weight,
positive-source, lowerable, and explicit lowerable final-wrapper layers
(589 lines), while Theorem23OutsideGroundPredecessorRaising.lean contains
the real source-weight and raising-source final-wrapper suffix (357 lines).
Focused checks cover the split modules and the predecessor-difference
downstream module.Theorem23OutsideGroundCrossLadder.lean now keeps the sublattice-component,
joint-component, lowered-joint, and packed cross-ladder final-wrapper layers
(683 lines), while Theorem23OutsideGroundCrossLadderUnpacked.lean
contains the unpacked lowered-joint cross-ladder final-wrapper suffix
(288 lines). Focused checks cover the split modules and the re-embedded
downstream module.A witness and lowered
site-sum dominance bridges became a stable suffix.
Theorem23LocalDifference.lean now keeps the predecessor-difference
callback layer (689 lines), while Theorem23LocalDifferenceSiteSum.lean
contains the lowered site-sum dominance suffix (280 lines). Focused checks
cover the split modules and the Marshall wrapper downstream module.A/on-A filtered sign-sum
bounds became a stable suffix. Theorem23Local.lean now keeps the
local ladder and site-sum expansion layer (440 lines), while
Theorem23LocalLowering.lean contains the lowering component suffix
(527 lines). Focused checks cover the split modules and the local
coefficient downstream module.Theorem23LocalLowering.lean now keeps the single-site component formulas
and strict local Marshall sign identities, while
Theorem23LocalLoweringSignSum.lean contains the non-negative/non-positive
boundary-inclusive sign-sum bounds. Focused checks cover the split modules
and the local-difference site-sum downstream module.Theorem23OutsideGround.lean now keeps
the outside-sector lower-bound, sector-minimality, and common-energy
final-packaging layers (580 lines), while
Theorem23OutsideGroundPredictedCasimir.lean contains the
predicted-Casimir final-wrapper suffix (512 lines). Focused checks cover
the split modules and the predicted-GS downstream module.Theorem23OutsideGroundPredecessor.lean now keeps the
predecessor-specialized source-weight and raising-source final-wrapper
layers (924 lines), while
Theorem23OutsideGroundPredecessorDifference.lean contains the
predecessor-difference outside-sector boundary suffix (258 lines).
Focused checks cover the split modules and the final downstream module.Theorem23SectorExistence.lean now keeps the final
statement, per-sector Theorem 2.2 reuse wrapper, and adjacent
sector-existence wrappers (892 lines), while
Theorem23SectorExistenceInterval.lean contains the predicted-GS
interval-chain suffix (371 lines). Focused checks cover the split modules
and the outside-ground / final downstream modules.Theorem23Interval.lean now keeps
the named callbacks plus the basic predecessor-difference, lowered-Marshall,
and predicted-GS sublattice-component interval chains (805 lines), while
Theorem23IntervalJoint.lean contains the joint-component and lowered-joint
cross-ladder interval-wrapper suffix (474 lines). Focused checks cover the
split modules and the interval-Casimir / outside-ground downstream modules.Theorem23OutsideGroundCrossLadder.lean now keeps the sublattice-component,
joint-component, lowered-joint, and unpacked lowered-joint final-wrapper
layers (948 lines), while Theorem23OutsideGroundCrossLadderReembedded.lean
contains the re-embedded / source-weight final-wrapper suffix (466 lines).
Focused checks cover the split modules and the predecessor / final
downstream modules.Theorem23OutsideGround.lean now keeps the outside-sector lower-bound,
sector-minimality, and predicted-Casimir final-wrapper layers (1073 lines),
while Theorem23OutsideGroundPredictedGS.lean contains the predicted-GS and
lowered-Marshall final-wrapper suffix (488 lines). Focused checks cover the
split modules and the cross-ladder / predecessor / final downstream modules.Theorem23Predicted.lean now keeps the predicted-Casimir,
predicted-GS, cross-ladder, and source-weight bridge layer (919 lines),
while Theorem23PredictedLadder.lean contains the ladder-closure and
scalar-transfer suffix (662 lines). Focused checks cover the split modules,
Theorem23, dominance, sector-existence, interval, and outside-ground
downstream modules.Theorem23.lean now keeps the site-sum and
predicted-Casimir common-energy links (709 lines), while
Theorem23Dominance.lean contains the dominance-form and predicted-GS
common-energy wrappers (916 lines). Focused checks covered Theorem23,
Theorem23Dominance, Theorem23SectorExistence, Theorem23Interval,
Theorem23IntervalCasimir, the outside-ground downstream modules, and
LatticeSystem.lean.lake env lean LatticeSystem/Quantum/SpinS/Theorem23.lean
completed in real 33.36s (user 47.27s, sys 8.53s);
cached lake build LatticeSystem.Quantum.SpinS.Theorem23
completed in real 6.55s (user 2.00s, sys 3.40s). No
module split was performed: Theorem23.lean remains large and
the final Theorem 2.3 adjacent-sector callback chain is still
actively being collapsed through the predecessor difference and
site-sum bridges. Splitting now would add import churn while the
proof boundary is still moving; keep extraction deferred until the
final adjacent-sector theorem wrapper lands.lake env lean LatticeSystem/Quantum/SpinS/Theorem23.lean
completed in real 22.50s (user 34.64s, sys 4.83s);
cached lake build LatticeSystem.Quantum.SpinS.Theorem23
completed in real 3.55s (user 1.70s, sys 2.46s). No
module split was performed: Theorem23.lean is large
(8837 lines), but the current proof still has one critical
lowered-Marshall-positivity callback in flight, and the newest
predicted-GS/Casimir bridges are tightly coupled to the adjacent
sublattice-lowering chain. Splitting now would add import churn
without a measured build-speed win. Revisit extraction after the
lowered-sector Marshall positivity step lands.lake env lean LatticeSystem/Quantum/SpinS/Theorem23.lean
completed in real 18.40s (user 19.60s, sys 4.23s);
cached lake build LatticeSystem.Quantum.SpinS.Theorem23
completed in real 3.60s (user 1.70s, sys 2.40s). No
module split was performed: Theorem23.lean is large
(4400 lines), but the current proof is still in-flight and the
latest additions are tightly coupled interval-chain wrappers.
Splitting now would add import churn without a measured
build-speed win. Revisit extraction once the remaining
predicted-GS membership or lowered-dominance input is proved.git push failure.neelStateOf, _antiparallel per-bond
primitives), Marshall sign generic + @[deprecated] window,
2D / 3D Heisenberg companion family parity. PRs #329 / #330 /
#331 / #332 / #333 / #334.lake build is zero warnings + zero errors), §3
expanded with concrete deprecation policy (6-month window from
since, message-form when target name unavailable, internal
companions linter-suppression pattern, #guard_msgs capture),
§5 with common linter-rewrite patterns (per-theorem omit
instead of file-level set_option linter.unused*, etc.), §2
with content + extensions pattern + helper-visibility examples,
§1 cross-reference to Tests/Foundation.lean POC, §6b
push-verification origin, docs/deprecations.md Jekyll page
(live tracking + removal checklist + remaining linter-
suppression transparency), all parent module-header docstrings
now document their extension sub-files (NeelState, SpinDot,
JordanWigner facades; TotalSpin, HeisenbergChain,
SpinHalfRotation, GibbsState, TimeReversalMulti content +
extensions). PRs #335–#372.SublatticeMagWeightComponent 2.73s,
SublatticeMagProjection 3.00s, Theorem23ToyWitness 2.86s,
JointCasimirEigenspaceLadderInvariant 2.82s,
CasimirSpectralLowerBound 2.84s) — well under the historical
split trigger (~16s); each file is small (40–130 lines) and split
at the one-theorem / few-theorem grain, so no split warranted.
A lake exe shake import audit flagged several “remove”
suggestions on the chain, but each was build-verified to be
wrong (the flagged imports — e.g. SublatticeSpinLadder in
SublatticeMagShift, ToyHamiltonian in
Theorem23ToyGroundEnergyBound — are genuinely required), so the
chain’s imports are already minimal. Both build-speed and import
hygiene healthy; no code change.Ŝ⁺_tot-kernel = the
minimal-total-spin highest-weight state). The ~20 new modules each
rebuild in ~2.4s (JointDiagonalKernel 2.42s, JointDiagonalRaiseImage
2.41s, JointLadderRaiseA 2.40s, SublatticeLadderLI 2.39s,
JointLadderIterateSublatticeMag 2.41s) — well under the historical
split trigger (~16s); each file is small (one-/few-theorem grain), so
no split warranted. The chain is well-factored; build-speed healthy;
no code change.= μ, the Ŝ³=½ block finrank ≤ 1, and the full E3b raising
machinery — sign-free single/total raising action, tower eigenvalue
tracking, termination, conditional highest weight, the coefficient-sum
functional and recursion, hard-core preservation, and the Marshall
positivity non-vanishing). The ~30 new TJ*.lean modules are all small
(≤ 282 lines; the largest is TJExchangeBondSum.lean at 282, then
TJSpinSymmetry.lean 251, TJStepMatrixEntry.lean 242) — every file is
split at the one-/few-theorem grain and each single-file rebuild is
light (a few seconds), well under the historical split trigger
(~2000–4000 lines / ~16s). The chain carries zero linter warnings (the
only warnings in the build are pre-existing in Quantum/SpinS/Rayleigh*).
No split warranted; the chain is well-factored; build-speed and
import hygiene healthy; no code change.Refactoring checkpoint at 17 feature PRs since the previous refactor (#4303):
PRs #4304–#4313 (Prop 11.24 capstone) and #4315–#4321 (Theorem 11.26
half-filling: kinetic vanishing, exchange reduction, all-up spin-dot/ground,
singlet annihilation, the Heisenberg-bond CAR identity, and the bond
= ½ Δ†Δ / positive-semidefiniteness).
Code change (dedup): TJAllUpSpinDot.lean (#4317) had carried a private
copy of fermionDownAnnihilation_commute_fermionSiteSpinMinus_of_ne; the same
cross-site annihilation–site-spin commutator was later published in
TJCrossSiteSpinCommute.lean (#4320). TJAllUpSpinDot.lean now imports
TJCrossSiteSpinCommute and reuses the public lemma, removing the ~20-line
duplicated CAR proof (and a redundant CrossSiteOfNe/FermionSiteSpin
transitive import).
Build-speed evaluation: the 82 TJ*.lean modules total ≈ 8.3k lines, all
small (≤ 282 lines; largest TJExchangeBondSum.lean 282, TJSpinSymmetry.lean
251). Single-file rebuilds are light (TJAllUpSpinDot ≈ 5 s incremental, ≈ 11 s
with dependency replay), well under the historical split trigger
(~2000–4000 lines / ~16 s). Zero linter warnings in the t-J chain. No split
warranted; the only structural improvement this cycle is the dedup above.
Cadence counter reset.