Interim authority. This lossless catalogue chunk remains authoritative for formalization status and capstone identification until Issue #5228. The version 1 JSON catalogue is still a non-authoritative prototype.
Interim catalogue › Spin models, Chapters 3–7, and spectral tools
| Lean name | Statement | File |
|—|—|—|
| staggeredCasimirOpS / shenQiuTian_ferrimagnetic_lro | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/FerrimagneticLROUniversalFinal.lean + …UniversalFinalCore.lean + FerrimagneticLRO.lean + …ComponentAlgebra.lean + …CrossTerm.lean + …TotalSpin.lean + …TotalSpinCore.lean + …Capstone.lean + …Universal.lean |
| raiseLowerReachableS_of_connected | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/ConnectedRaiseLower.lean + …ConnectedDressedPF.lean + …ConnectedSectorIrreducible.lean + …ConnectedTheorem23Core.lean + …ConnectedTheorem23.lean + …ConnectedFerrimagneticLRO.lean + …StaggeredCasimirSU2Invariance.lean + …SU2ExpectationLadderInvariant.lean + …SU2ExpectationLadderIterated.lean + …ConnectedSectorFinrankLeOne.lean + …WeightPreservingExpectationSum.lean + …StrictHOutsideFerrimagnetic.lean + …StrictHOutsideFerrimagneticCore.lean + …FerrimagneticLROUniversal.lean |
| reflectionPositivity_averaging | Lemma 4.5 (§4.1.2, PROVED; eqs. (4.1.55)–(4.1.57)): the abstract reflection-positivity averaging inequality used in the proof of Thm 4.1. For F : (Fin 2n → V) → ℝ (arbitrary V) invariant under the cyclic shift and satisfying the reflection bound F f ≥ ½(F(reflectLeft f)+F(reflectRight f)), one has (1/2n)·Σ_j F(j↦f j) ≤ F f. Discharged axiom-free via Tasaki’s G_min=0 collapse argument: minimise G f = F f − (2n)⁻¹Σ_j F(const f_j) over the finite carrier {f∘σ}; at a minimiser the reflection bound is an equality, and a leading-run doubling collapses the minimiser to a constant string where G = 0 (PR #4598) | Math/ReflectionPositivityAveraging.lean |
| HypercubicTorus / torusNNCoupling / staggeredRaisingOpS / tower_lowLying_energy_bound | Theorem 4.6 (§4.2.2, Anderson’s tower, now PROVED — axiom discharged, PR #4769/#4773; eqs. (4.2.2)–(4.2.4)): low-lying tower states. Builds the d-dim hypercubic torus model Fin d → ZMod L (L^d sites, NN coupling, parity sublattice) + staggered raising/lowering order operators Ô_L^± = Σ_x ε_x Ŝ_x^±. The two-sided tower states towerState M = (Ô_L^{sgn M})^{\|M\|} Φ_GS (M : ℤ, raising for M≥0 / lowering for M<0) satisfy ⟨ψ_M,Ĥψ_M⟩/⟨ψ_M,ψ_M⟩ ≤ E_GS + C₂M²/L^d for \|M\| ≤ C₁L^{d/2} (Rayleigh-ratio form, scale-invariant). Conditional on LRO (q₀>0 premise: ⟨(Ô_L/L^d)²⟩ = ⟨Ô²⟩/(⟨Φ,Φ⟩·(L^d)²) ≥ q₀, eq. 4.1.7), so vacuous in d=1 per Cor 4.3. Proof (axiom-clean, #print axioms = propext/Classical.choice/Quot.sound): the variational double-commutator bound (★, tower_numerator_double_commutator_le) reduces the gap to ⟨Φ,[(ô⁻)^M,[Ĥ,(ô⁺)^M]]Φ⟩; this numerator is bounded ≤ M²(A/V·P_M + B M²/V²·P_M) via Lemma R2 (split-independent renormalized commutator estimate r2_split_independent) + locality decay of d̂=[ô⁺,[Ĥ,ô⁻]] and [Ĥ,ô⁺] + moment-factor→P_M conversions; the denominator ‖(ô±)^M Φ‖² ≥ ½P_M (Lemma R1, balanced-word orderWord_balanced_re_close); the LRO recursion 2q₀P_n ≤ P_{n+1} (phatMoment_succ_two_q0_le) needs the total-spin-singlet premise Ŝ³Φ=Ŝ¹Φ=0 (added to IsAndersonTowerConstants; faithful — the bipartite AFM GS is the unique singlet by MLM Thm 2.3). M<0 via Hermitian conjugation; constants C₁=min(√(q₀/6N),√(2^d)√(2q₀)/16N), C₂=288dN⁴/q₀+576C₁²dN³(1+1/√(2q₀))/q₀; N=0 vacuous (order op = 0) | Quantum/SpinS/AndersonTower.lean, Quantum/SpinS/AndersonTowerTheorem46.lean |
| orderWordProd_comm_eq_telescope | Step A telescope of the Lemma-R2 centering (Tasaki §4.2.2, eq. (4.2.68), p. 111; PR #5149): the commutator of an order-word product with G expands as the position-wise sum orderWordProd w · G − G · orderWordProd w = ∑_{i < w.length} telescopeTerm w G i (prefix · [ô^{w_i}, G] · suffix). Moving G from an end to the centre is the difference of two such partial telescopes, each term carrying one fewer order factor and the decayed commutator orderComm — the bookkeeping behind Tasaki’s bound ⟨ô_{s₁}···Â···ô_{s_{2M}}⟩ ≤ 3‖Â‖⟨p̂⟩^M used by r2_split_independent | Quantum/SpinS/AndersonTowerR2Centering.lean |
| tower_lowLying_eigenstates | Corollary 4.7 (§4.2.2, now PROVED — axiom discharged, PR #4775; eq. (4.2.7)): the tower of low-lying energy eigenstates. For a total-spin-singlet GS and each M ≠ 0 with \|M\| ≤ C₁L^{d/2} (nonzero tower state), ∃ an Ĥ-eigenstate Ψ_M in the Ŝ_tot^(3) sector M with E_GS < E_M ≤ E_GS + C₂M²/L^d. Proof (axiom-clean): Ψ_M = the minimum-energy eigenstate of Ĥ restricted to the magnetization sector of towerState M Φ (heisenbergHamiltonianS_magSector_min_eigenvector, lifting the restricted-Hermitian min eigenvector via magSectorEmbedding); its energy ≤ Rayleigh(towerState) (tower_sectorMin_mul_le, variational + norm/energy embedding bridges) ≤ E_GS + C₂M²/L^d (Theorem 4.6); strict gap from the ground-sector-exclusion premise (every ground eigenstate is a singlet) since Ψ_M sits in sector M ≠ 0. Distinct M → distinct sectors → O(L^{d/2}) distinct low-lying eigenstates (Anderson tower). Conditional on LRO (vacuous in d=1) | Quantum/SpinS/AndersonTowerEigenstates.lean |
| tanakaSSBState / tanakaSSB_lowLying_energy_bound | Theorem 4.8 (§4.2.1, Tanaka, PROVED axiom-free, #4958 PR-E; singlet-conditional on Ŝ³Φ=Ŝ¹Φ=0 per eq. (4.1.7); eqs. (4.2.10)–(4.2.11)): the Tanaka full-symmetry-breaking state Ξ_{(1,0,0)} = (1/√2)((Ô_L^(1))^M Φ/‖·‖ + (Ô_L^(1))^{M+1} Φ/‖·‖) (each term separately normalized via unitNormalize/vecNormSqRe; α=1 staggered op staggeredOrderOp1S) is low-lying: ⟨Ξ,ĤΞ⟩/⟨Ξ,Ξ⟩ ≤ E_GS + C₂{M+1}²/L^d for M>0, M+1 ≤ C₁L^{d/2} (∃ C₁ C₂, IsAndersonTowerConstants ∧ IsTanakaSSBConstants, one pair via C₁=min/C₂=max merge of the Thm 4.6 constants). Proof: scale-invariance drop (eq. 4.2.70) → per-tower-term Rayleigh bound from the double-commutator numerator (tanaka_numerator_bound, eq. 4.2.71) over the balanced-word denominator (orderSum_pow_two_denom_lower, eq. 4.2.67), collapsed by the central-binomial (Pascal) cancellation 2·C(2(k-1),k-1) ≤ C(2k,k) and the LRO moment step 2q₀P_{k-1}≤P_k; the two orthogonal parity-opposite tower terms (cross-term = 0, eq. 4.2.69) averaged via tanakaSSBState_expectationRatioRe_le. Conditional on LRO (vacuous in d=1) | Quantum/SpinS/AndersonTowerTanakaCapstone.lean |
| tanakaSSB_full_symmetry_breaking / IsTanakaFullSSBConstants | Theorem 4.9 (§4.2.2, Tasaki, PROVED #4967 PR5; eqs. (4.2.12)–(4.2.15)/(4.2.56)/footnote 21): the Tanaka state exhibits full SU(2) symmetry breaking in the (1,0,0) direction. The former axiom is now a proved theorem for the explicit slowly-diverging sequence M(L) := ⌊L^{d/4}⌋ (Tendsto M atTop atTop, with M+1 ≤ C₁L^{d/2} and M²/V → 0 both eventually). For that M, the per-site staggered moments (tanakaOrderMean1/2/3, tanakaOrderSecond1/2/3, Rayleigh-ratio via expectationRatioRe) satisfy liminf⟨Ô^(1)/L^d⟩≥mStar, liminf⟨(Ô^(1)/L^d)²⟩≥mStar² (liminf per footnote 21, from sqrt_q0_le_tanakaOrderMean1/q0_le_tanakaOrderSecond1 with mStar = √q₀), ⟨Ô^(α)/L^d⟩=0 (α=2,3, exactly, tanakaOrderMean2/3_eq_zero), lim⟨(Ô^(α)/L^d)²⟩=0 (α=2,3, from tanakaOrderSecond2_le + the clean fluctuation bound deltaFluctBound_le_clean and the M(L) squeeze, with axis-3 reduced to axis-2 via tanakaOrderSecond3_eq_tanakaOrderSecond2, eq. 4.2.56 — Ŝ_tot^(1) Ξ = 0 since Ô^(1) commutes with Ŝ_tot^(1)). The GS family is a total-spin singlet (Ŝ_tot^(3)Φ=0, Ŝ_tot^(1)Φ=0, eq. 4.1.7) that is axis-1 reversal invariant (ΘΦ=Φ, Θ=manyBodyReversalS); mStar = √q₀ > 0 existential (eq. 4.2.9 double limit not constructed); same C₁ as Thm 4.6. Conditional on LRO (vacuous in d=1). Axioms: [propext, Classical.choice, Quot.sound] | Quantum/SpinS/AndersonTowerTheorem49.lean |
| sqrt_q0_le_tanakaOrderMean1 / q0_le_tanakaOrderSecond1 / staggeredOrderOp1S_isHermitian / orderOp1_evenMoment_ratio_ge_q0 / tanakaSSBState_vecNormSqRe_eq_one | Theorem 4.9 lower bounds (§4.2.2, Tasaki Theorem 4.9 discharge PR3, #4970; eqs. (4.2.12)/(4.2.13)/(4.2.35)/(4.2.45)–(4.2.47), footnote 21): the Tanaka state order-parameter lower bounds at every finite volume. (4.2.12): √q₀ ≤ ⟨Ξ| Ô_L^(1)/L^d |Ξ⟩ (axis-1 per-site staggered moment, eq. 4.2.12 sqrt_q0_le_tanakaOrderMean1); (4.2.13): q₀ ≤ ⟨Ξ| (Ô_L^(1)/L^d)² |Ξ⟩ (squared moment, eq. 4.2.13 q0_le_tanakaOrderSecond1). Proof mechanism: log-convexity of even bare moments B_k := ‖(Ô_L^(1))^k Φ‖² (Cauchy–Schwarz, eq. 4.2.35) yields non-decreasing ratio R_k := B_{k+1}/(B_k V²) via real_logConvex_cross; base case R_0 ≥ q₀ from charge selection ⟨(Ô^(1))²⟩ = ⟨p̂⟩ V²/2 combined with proved long-range-order bridge ⟨p̂⟩ ≥ 2q₀ ‖Φ‖² (phatMoment_succ_two_q0_le); hence R_M ≥ q₀ via orderOp1_evenMoment_ratio_ge_q0; the Ξ sandwich tanakaSSBState_dotProduct_mulVec_re_eq with parity structure (odd-moment diagonals vanish, squared operator commutes with parity so cross-terms vanish) yields both bounds. Infrastructure: Hermiticity staggeredOrderOp1S_isHermitian, unit normalization tanakaSSBState_vecNormSqRe_eq_one. These bounds hold at every finite volume, so their liminf (footnote 21 form) is ≥ the same; the existential slowly-diverging M and full SU(2)-breaking limit remain axiomatized in Theorem 4.9. Unlike Theorem 4.8 (eqs. 4.2.34–4.2.44), no central-binomial cancellation needed—only ratio monotonicity. | Quantum/SpinS/AndersonTowerTanakaLowerBounds.lean / Math/Analysis/RealLogConvexSequence.lean |
| manyBodyReversalS_conj_staggeredOrderOp1S, manyBodyReversalS_conj_staggeredOrderOp2S, manyBodyReversalS_conj_staggeredOrderOpS, manyBodyReversalS_commute_staggeredOrderOp1S, manyBodyReversalS_mulVec_tanakaTowerTerm, manyBodyReversalS_mulVec_tanakaSSBState, tanakaOrderMean2_eq_zero, tanakaOrderMean3_eq_zero, tanakaSSBState_dotProduct_mulVec_re_eq, tanakaTowerTerm_cross_charge_conserving_eq_zero, manyBodyReversalS_conjTranspose | Theorem 4.9 machinery (§4.2.2, Tasaki Theorem 4.9 discharge PR2, #4969; eqs. (4.2.14), (4.2.45)–(4.2.49), (4.2.69)): the axis-1 spin reversal Θ = manyBodyReversalS conjugation infrastructure. Conjugation by Θ: Θ Ô^(1) Θ = Ô^(1) (axis-1 fix), Θ Ô^(2) Θ = −Ô^(2), Θ Ô^(3) Θ = −Ô^(3) (transverse reversal; staggeredOrderOp1/2/3S); Θ commutes with the axis-1 operator and fixes the Tanaka state Θ Ξ = Ξ when Θ Φ = Φ. Symmetry of Θ: real symmetric involution Θᴴ = Θ (manyBodyReversalS_conjTranspose). Transverse moment vanishing (Tasaki eq. 4.2.14): anti-invariance under a symmetric involution forces ⟨Ξ| Ô^(α) |Ξ⟩ = 0 for α = 2, 3 (proven for α=2,3 via tanakaOrderMean2/3_eq_zero). General Ξ sandwich expansion (Tasaki eqs. 4.2.45/4.2.49): for Hermitian O, ⟨Ξ| O |Ξ⟩.re decomposes into normalized tower-term expectations (tanakaSSBState_dotProduct_mulVec_re_eq). Charge-parity cross-term vanishing (Tasaki axis-3 analogue of eq. 4.2.69): for a charge-conserving operator O commuting with the parity Û = exp(iπ Ŝ_tot^(3)), the two adjacent tower terms (Ô^(1))^M Φ and (Ô^(1))^{M+1} Φ decouple (tanakaTowerTerm_cross_charge_conserving_eq_zero) because they are Û-eigenstates with distinct eigenvalues | Quantum/SpinS/AndersonTowerTanakaMoments.lean |
| orderWord_balanced_re_close_fine | Theorem 4.9 axis-2 decay — fine denominator closeness (§4.2.2, Tasaki Theorem 4.9 discharge PR4, #4971; eqs. (4.2.34)/(4.2.42)): the precision O(1/V) two-sided bound on balanced-word denominator. For a singlet Φ with size 3N(m+1)² ≤ 2q₀V, the summed-density even power D_{m+1} = ⟨Φ, (ô⁺ + ô⁻)^{2(m+1)} Φ⟩ is within the fine band C(2(m+1),m+1) · (m+1)² (N/V) (3/2 P_m) of C(2(m+1),m+1) · P_{m+1}. Proof: expand into the 2^{2(m+1)} order words, drop unbalanced words via singlet charge-selection, leaving C(2(m+1),m+1) balanced words, each pinched by the swap-chain kernel orderWord_balanced_re_close_step (retaining the (m+1)² N/V prefactor—not collapsing to crude ½ P); sum per-word deviations. This refinement (vs crude orderWord_balanced_re_close) resolves the central-binomial cancellation in axis-2 decay (Theorem 4.9 PR4) | Quantum/SpinS/AndersonTowerEnergyBoundR1.lean |
| orderSum_pow_two_denom_close / staggeredPhatS_manyBodyOperatorNormS_le / phatMoment_succ_le_normSq / orderSum_pow_phat_insert_close / tanakaOrderSecond2_eq_half_sum / tanaka_delta_eq / tanaka_delta_le / tanakaOrderSecond2_le | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/AndersonTowerEnergyBound.lean, Quantum/SpinS/AndersonTowerTanakaFluctuation.lean |
| solidAngleAverageTanaka / IsConjecture412Equality / tanakaSphereAverage_groundState | Proposition 4.10 (§4.2.1, PROVED (theorem, conditional), PR #5044; eqs. (4.2.17)–(4.2.22)): the solid-angle average of the symmetry-breaking states recovers the ground state. Direction states Ξ_n (directionStaggeredOp/directionTanakaState for n∈S²⊂ℝ³); the Bochner integral ∫_{|n|=1} Ξ_n dn over Metric.sphere in EuclideanSpace ℝ (Fin 3) (surface measure volume.toSphere). Conditional on Conjecture 4.12 (m*=√(3q*), a Prop hypothesis never asserted true) and the documented axiom orderSqMoment_ratio_le_mStarSq (ô² concentration, Koma–Tasaki [66] p̂ mirror parity): the normalized average converges (in the L²/Hilbert norm √⟨·,·⟩ via vecNormSqRe) up-to-phase to Φ_GS (∃z, ‖z‖=1, √(vecNormSqRe(unitNormalize(Ξ_avg)−z•Φ̂))<ε). The GS family is a total-spin singlet + axis-1 reversal invariant (ΘΦ=Φ, matching IsTanakaFullSSBConstants so the linked full-SSB premise is non-vacuous). qStar tied to the actual q* limit of Φ. Conditional on LRO (vacuous in d=1). Proof (axiom-conditional, #print axioms = propext/Classical.choice/Quot.sound/orderSqMoment_ratio_le_mStarSq): per-volume triangle bound splitting the normalized distance into the operator vs (ô²)ʲ remainder (Lemma L2, PR-6c-i) plus the (ô²)ʲ collapse distance (Lemma L5-a); operator remainder vanishes as O(1/V) (Lemma L3); collapse distance vanishes via ratio limit conditional on Conjecture 4.12 and the ô² axiom (Lemma L5-b-iii); capped diagonal diagonal_tendsto_zero_capped (S-6) extracts M(L) = 2m(L) with growth M+1 ≤ C₁L^{d/2} (PR #5043/#5044). | Quantum/SpinS/AndersonTowerSphereGroundState.lean |
| sqrt_vecNormSqRe_unitNormalize_sub_le / vecNormSqRe_orderSqPow_mulVec / sqrt_vecNormSqRe_sub_triangle / sphereAverage_op_unitNormalize_sub_le / diagonal_tendsto_zero_capped | Proposition 4.10 (PR-6c-i) deferral discharge (§4.2.2, Tasaki Proposition 4.10, eqs. (4.2.58)–(4.2.61), pp. 108–109; PROVED axiom-free, PR #5043): six-lemma analytic sub-tier for Prop 4.10 final assembly (PR-6c-ii). (S-1) Unit-vector perturbation (sqrt_vecNormSqRe_unitNormalize_sub_le): generic L²-norm perturbation bound ‖â − ŵ‖ ≤ 2 ‖a − w‖ / ‖w‖ via normed-space decomposition. (S-2) Order-squared norm (vecNormSqRe_orderSqPow_mulVec): ‖(ô²)ʲ Φ‖² = R_{2j} (moment identity). (S-3) Triangle inequality (sqrt_vecNormSqRe_sub_triangle): L²-norm triangle inequality for vecNormSqRe. (S-4) First-term bound (sphereAverage_op_unitNormalize_sub_le): normalized sphere integral and normalized (ô²)ʲ tower term differ by O(1/V) per-volume constant (the Φ-independent term of the triangle bound in PR-6c-ii). (S-5) Collapse reduction (deferred in 6c-i, built in PR-6c-ii L5-a/L5-b subcircuit via orderSq_collapse_vecNormSqRe + orderSq_collapse_ratio_tendsto_one): the (ô²)ʲ collapse distance shrinking via ô² moment ratio concentration. (S-6) Capped diagonal (diagonal_tendsto_zero_capped): extract M(L) = 2m(L) with growth M+1 ≤ ⌊(C₁ L^{d/2} − 1)/2⌋₊, closing the limit assembly. | Quantum/SpinS/AndersonTowerSphereDischargeParts.lean / Quantum/SpinS/AndersonTowerOrderSqMoment.lean / Math/DoubleSequenceDiagonal.lean |
| tanakaSSB_orderParameter_lowerBound | Theorem 4.11 (§4.2.1, Koma–Tasaki, PROVED (theorem, conditional), PR #5047; eq. (4.2.23)): the two order parameters satisfy √(3q₀) ≤ m* (the √3 reflects SU(2); √2 for U(1)/XXZ). To avoid the downward-closure of the SSB predicate, q₀ and m* are pinned as the exact infinite-volume limits via a single hFamily : IsRealizingTanakaGroundStateFamily d N q₀ m* C₁ Φ E₀ M (the diverging tower M with growth M+1 ≤ C₁L^{d/2}; Φ an eventual minimizing nonzero GS with well-defined Tanaka terms; exact LRO limit q₀; exact staggered-moment limit tanakaOrderMean1 → m*; IsTanakaFullSSBConstants connecting to Thm 4.9 for the same m). Unsatisfiable in d=1 (no LRO GS), so applies exactly where intended; m*>0 follows. Conditional on documented axiom orderSqMoment_ratio_le_mStarSq_family (ô² concentration, Koma–Tasaki [66]); Conjecture 4.12 not required. Proof (axiom-conditional, #print axioms = propext/Classical.choice/Quot.sound/orderSqMoment_ratio_le_mStarSq_family): assembles the Conjecture-4.12-free base-ratio limit s₀(L) = R₁/(R₀·V²) → 3q₀ (factor-3 isotropy, singlet) with the concentration axiom s₀(L) < (m*)²+ε eventually; comparing limits gives 3q₀ ≤ (m*)², and √-monotonicity with m*>0 yields the bound | Quantum/SpinS/AndersonTowerTheorem411.lean |
| IsRealizingTanakaGroundStateFamily | *(refactoring helper) the shared realizing ground-state family conditioning (tower M diverging with slow-divergence M(L) = o(L^{d/2}) per Tasaki Thm 4.9 fn. 21 / Lemma 4.16: for every c > 0, eventually M(L) + 1 ≤ c L^{d/2}; gate bound M+1 ≤ C₁L^{d/2} at c := C₁); eventual minimizing/nonzero GS that is a total-spin singlet + axis-1 reversal invariant (ΘΦ=Φ); exact LRO limit q₀; exact staggered-moment limit m*; IsTanakaFullSSBConstants) bundled into one predicate, used as the hFamily hypothesis of Thm 4.11 / Thm 4.13 / Lemma 4.15 (DRY) | Quantum/SpinS/AndersonTower.lean |
| conjecture_4_12 / IsConjecture412Equality | Conjecture 4.12 (§4.2.1, AXIOM-FREE Prop STATEMENT; eqs. (4.2.25)–(4.2.26)): the SSB and LRO order parameters coincide, m* = √(3q*). Registered as a def conjecture_4_12 (d N) : Prop — the unproven conjecture quantified over the realizing GS family (a total-spin singlet + axis-1 reversal invariant ΘΦ=Φ matching IsTanakaFullSSBConstants; LRO limit q, SSB order param m via IsTanakaFullSSBConstants), never asserted true (no axiom/theorem derives it; that would be unsound) | Quantum/SpinS/AndersonTowerSphereAverage.lean |
| tanakaSSB_realizingFamily_energyBound | Theorem 4.8 (companion trial-energy bound) (§4.2.2, Tasaki Theorem 4.8, eq. (4.2.11), p. 98; PROVED axiom-free, PR #5049): the proved trial-energy input for Theorem 4.13’s Rayleigh–Ritz variational argument. For the Tanaka symmetry-breaking state Ξ_L = tanakaSSBState (torusParitySublattice d L) N (M L) (Φ₀ L) (eq. (4.2.10)), with the tower growth M+1 ≤ C₁L^{d/2} and realizing family’s LRO limit q₀/2 ≤ ⟨Φ| Ô²Φ⟩ / (⟨Φ,Φ⟩ L^{2d}) eventually (via the family’s LRO conjunct), the per-site energy of Ξ is bounded: ⟨Ξ|ĤΞ⟩/⟨Ξ,Ξ⟩ ≤ E_{GS} + C₂(M+1)²/L^d for constants C₁, C₂ depending on q₀, N, d (from Theorem 4.8 at threshold q₀/2). Consumed by Theorem 4.13 as the error-term vanishing input. Unsatisfiable in d = 1 (Corollary 4.3), vacuous there. #print axioms = propext, Classical.choice, Quot.sound only. | Quantum/SpinS/AndersonTowerTheorem413.lean |
| staggeredFieldHamiltonianS / tanakaSSB_field_lowerBound | Theorem 4.13 (§4.2.1, PROVED (theorem, axiom-free), PR #5050; eqs. (4.2.27)–(4.2.28)): SSB under an infinitesimal staggered field. Field Hamiltonian Ĥ_h = Ĥ − h·Ô_L^(1); for the field ground state Φ_GS,h, lim_{h↓0} liminf_{L↑∞} ⟨Φ_GS,h\|Ô_L^(1)/L^d\|Φ_GS,h⟩ ≥ m* (ε–δ: inner L₀ depends on h). Proof (Rayleigh–Ritz variational method, §3.4 Theorem 3.2, Kaplan–Horsch–von der Linden): the Tanaka state Ξ_L (eq. (4.2.10)) is a trial state with energy bounded by tanakaSSB_realizingFamily_energyBound (Theorem 4.8 companion); linearity of Rayleigh quotient peels the field Ĥ_h = Ĥ − hÔ; per-site staggered moment of Ξ_L converges to m* by the family’s staggered-moment limit (eq. (4.2.12)). Neither Conjecture 4.12 nor Theorem 4.11 is consumed (#print axioms = propext, Classical.choice, Quot.sound only — completely axiom-free). m* pinned as the genuine order parameter (realizing unperturbed GS, IsTanakaFullSSBConstants); field GS a given eigenvector/minimizer/nonzero family. Combined with Thm 4.11 gives m* ≥ √(3q₀) > 0. Vacuous in d=1 | Quantum/SpinS/AndersonTowerTheorem413.lean |
| manyBodyOperatorNormS / staggeredPhatS / staggered_balanced_order_product_norm_le | Lemma 4.14 (§4.2.2, PROVED axiom-free; eqs. (4.2.30)–(4.2.34)): order-operator algebra estimate. Per-volume ops ô^± = Ô_L^±/V, p̂ = ½(ô^+ô^- + ô^-ô^+); for a balanced sign sequence s (length 2n, n pluses), ‖ô^{s₁}⋯ô^{s_{2n}} − p̂ⁿ‖ ≤ n²N^{2n−1}/L^d in the L² operator norm manyBodyOperatorNormS (o₀=2S=N, V=L^d). Now a proved theorem (Issue #4769): L²-norm algebra via the star-algebra equivalence toEuclideanCLM (submult/triangle), per-site ‖Ŝₓ^±‖≤N (C*-identity + diagonal Ŝ⁻Ŝ⁺ entries k(N-k+1)≤N²) ⟹ ‖ô^±‖≤N, staggered commutator [Ô⁺,Ô⁻]=2Ŝ³_tot ⟹ ‖[ô⁺,ô⁻]‖≤N/V, a permutation-free adjacent-swap telescoping (SwapChain/swapDist_le, diameter ≤n²) bounding any two balanced words’ products by n²N^{2n-1}/V, and the noncommutative binomial expansion of p̂ⁿ as the uniform (½)ⁿ-combination of the 2ⁿ block words | Quantum/SpinS/ManyBodyOperatorNorm.lean + Quantum/SpinS/OrderOperatorAlgebra.lean |
| mStar_eq_phat_ratio_limit | Lemma 4.15 (§4.2.2, AXIOM; eqs. (4.2.38)–(4.2.39), p. 105): the order parameter as a p̂-ratio double limit. Tasaki eq. (4.2.38) states m* = lim_n liminf_L √(⟨p̂^{n+1}⟩/⟨p̂^n⟩) with a square root (pdftotext dropped the √ radical from the PDF); squaring, the formal axiom equivalently records the bare (unrooted) ratio limit (m*)² = lim_n liminf_L ⟨p̂^{n+1}⟩/⟨p̂^n⟩ (consistent with p̂=(ô¹)²+(ô²)² having density-squared dimension ⟨p̂^n⟩≃(m*)^{2n} and with eqs. (4.2.37)/(4.2.39)). Sound liminf-lower direction (∀ε ∃n₀ ∀n≥n₀, eventually-in-L bare ratio > (m*)²−ε); also the U(1)-optimal bound √(2q₀) ≤ m* (√2 companion of Thm 4.11’s √3). m* pinned via realizing GS + IsTanakaFullSSBConstants; p̂-moments positive under LRO. Vacuous in d=1 | Quantum/SpinS/OrderOperatorAlgebra.lean |
| orderSqMoment_ratio_le_mStarSq | Proposition 4.10 (§4.2.2, ô² concentration upper bound, AXIOM; eqs. (4.2.40), (4.2.59)–(4.2.61), pp. 105–109): the ô²-moment concentration upper bound. For the staggered ground-state family Φ with successive moments R_k = ⟨(ô²)^k⟩, the V²-normalised ratio s_n = R_{n+1}/(R_n·V²) satisfies the limsup-upper direction: for all n and ε > 0, eventually in L, s_n < (m∗)² + ε. Mirror of the p̂-field axiom mStar_eq_phat_ratio_limit already documented; per the 2026-07-12 no-overreach boundary, this ô² concentration defers with parity to that mirror rather than rebuilding the Koma–Tasaki [66] machinery. Conditional on Conjecture 4.12 (never asserted), singlet hypothesis hsinglet, axis-3 LRO limit hlim3 → q∗, moment positivity hR. Unsatisfiable in d = 1 (no LRO), hence vacuous (PR #5035) | Quantum/SpinS/AndersonTowerOrderSqConcentration.lean |
| orderSqMoment_ratio_le_mStarSq_family | Theorem 4.11 (§4.2.2, AXIOM; eq. (4.2.23), pp. 101, 105–109): the n = 0 ô² concentration upper bound, hFamily-pinned and hconj-free. Unlike its sibling orderSqMoment_ratio_le_mStarSq which requires Conjecture 4.12 as a hypothesis, this axiom pins m* to its genuine value via the realizing ground-state family (IsRealizingTanakaGroundStateFamily: exact infinite-volume limits, total-spin singlet, matching IsTanakaFullSSBConstants), making the base ratio s₀ = R₁/(R₀·V²) < (m*)² + ε true independent of Conjecture 4.12. Why hconj-drop is unsound: deleting the hconj constraint from the general axiom leaves m* free; taking m* = 0 while Φ is a genuine LRO singlet satisfies all remaining hypotheses yet yields the false inequality 0 < 3q* < ε — so the statement becomes FALSE without pinning. The pinned version captures only Theorem 4.11’s “easy half” ((m*)² ≥ 3q₀); the matching equality (m*)² = 3q₀ is Conjecture 4.12. SU(2)/ô² parity: SU(2) mirror of the already-documented p̂/U(1) axiom mStar_eq_phat_ratio_limit (same m* via IsTanakaFullSSBConstants, the √3 vs √2 isotropy factors, base-ratio limits 3q₀ vs 2q₀). Unsatisfiable in d = 1 (no LRO GS), hence vacuous | Quantum/SpinS/AndersonTowerOrderSqConcentration.lean |
| pow_sum_smul_eq_sum_smul_prod / prod_comp_eq_prod_pow_card | Noncommutative multinomial expansion (Tasaki §4.2.2, eq. (4.2.58), p. 108; PROVED axiom-free, Issue #4974, PR #5013): the fundamental algebra lemma for the operator sphere-average polynomial expansion. For scalars c : ι → ℂ and operators O : ι → A in a noncommutative ℂ-algebra A with finite index ι, the M-th power expands as (∑ α, c α • O α)^M = ∑ f : Fin M → ι, (∏ j, c (f j)) • ∏_j O (f j), where the ordered operator product is kept literally as (List.ofFn …).prod (no commutators introduced). Proved by induction on M via the Fin.snoc bijection of (Fin M → ι) × ι ≃ Fin (M + 1) → ι. Helper lemma prod_comp_eq_prod_pow_card reindexes the scalar product ∏_j c (f j) into the multiplicity form ∏ α, c α ^ #{j | f j = α}, matching the sphere-monomial-moment decomposition. Consumed by the operator sphere-average (Prop 4.10, eq. 4.2.59). Compare add_pow_eq_sum_ofFn (OrderOperatorAlgebra.lean, line 619): the analogous noncommutative binomial for (A + B)^n is a specialization with ι = Bool, binary choice of two operators. | Math/NoncommPowerExpansion.lean |
| sphereMonomialMoment_odd / sphereMonomialMoment_even / sphereMonomialMoment / sphereMonomialMoment_eq | Scalar sphere monomial moments (Tasaki §4.2.2, eq. (4.2.58), p. 108; PROVED axiom-free, Issue #4974, PR #5012): the spherical (Dirichlet) monomial integral ∫_{S²} ∏ᵢ nᵢ^{kᵢ} dσ(n) on the unit sphere with rotation-invariant surface measure σ = volume.toSphere. For exponent tuple k ∈ ℕ³ and total degree M = Σᵢ kᵢ: if some kᵢ is odd the integral vanishes (sphereMonomialMoment_odd); if all kᵢ are even it equals 4π · (∏ᵢ (kᵢ − 1)‼) / ((M + 1)‼) (sphereMonomialMoment_even) using double factorial (Nat.doubleFactorial). Attributed to Koma–Tasaki “(4.40) of [66]”; scalar substrate for the operator polynomial expansion (eq. 4.2.59). The double-factorial closed form is load-bearing: ratio (M-1)‼/(M+1)‼ = 1/(M+1) yields the 1/(M+1) coefficient in eq. (4.2.58). Public interface: sphereMonomialMoment (piecewise def) and sphereMonomialMoment_eq (evaluation to the closed form). Proof via isotropic Gaussian integral ∫_{ℝ³} (∏ᵢ xᵢ^{kᵢ}) e^{-‖x‖²/2} dx evaluated via both Cartesian factorisation (product of full-line moments) and polar decomposition (sphere moment × radial Gaussian); equating and solving uses antisymmetry of full-line Gaussian moments at odd indices, and closed values of half-moments at even indices | Math/SphereMoment.lean |
| stagOpVec / directionStaggeredOp_eq_sum / sphereAverage_directionStaggeredOp_pow | Operator sphere-average polynomial expansion (Tasaki §4.2.2, eq. (4.2.59), p. 108; PROVED axiom-free, Issue #4974, PR #5013): the principal machinery for Prop 4.10’s solid-angle average decomposition. The direction order operator Ô_L^n = Σ_x ε_x (Ŝ_x·n) decomposes along the three spin axes as Ô_L^n = Σ_α n_α ô^{(α)}, where stagOpVec A N : Fin 3 → ManyBodyOpS packages the three staggered axis operators (staggeredOrderOp1S, staggeredOrderOp2S, staggeredOrderOpS); directionStaggeredOp_eq_sum proves the decomposition. Raising to the M-th power and integrating over the sphere (unit sphere Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with measure volume.toSphere), the noncommutative multinomial expansion (pow_sum_smul_eq_sum_smul_prod) together with the scalar monomial moments (sphereMonomialMoment_eq) yields the capstone: ∫_{S²} (Ô_L^n)^M dσ(n) = Σ_{f : Fin M → Fin 3} sphereMonomialMoment(count f) • ∏_j ô^{(f j)}, with the ordered operator product kept literally (no commutators). Tuples with odd axis multiplicities contribute 0 (via sphereMonomialMoment). The operator order is preserved exactly. | Quantum/SpinS/AndersonTowerSphereMoment.lean |
| orderSqOp / orderSqOp_eq_smul_staggeredPhatS_add_sq | Squared order operator and transverse/longitudinal split (Tasaki §4.2.2, eq. (4.2.31), p. 108; PROVED axiom-free, Issue #4974, PR #5014): the rotationally invariant squared order operator ô² = Σ_α (ô^{(α)})² (orderSqOp), the sum of squared staggered axis operators over the three spin axes, whose (M/2)-th power carries the leading contribution to the sphere average after contraction. Transverse/longitudinal decomposition (orderSqOp_eq_smul_staggeredPhatS_add_sq, eq. 4.2.31): on the hypercubic torus, ô² = V² · p̂ + (ô^{(3)})², where V = L^d is the volume, p̂ = staggeredPhatS is the U(1)-symmetric order operator carrying the transverse part (ô^{(1)})² + (ô^{(2)})², and (ô^{(3)})² is the longitudinal part. The factor V² undoes the per-volume normalization in p̂, allowing the transverse contribution to be handled through the existing Theorem 4.9 p̂-moment machinery. | Quantum/SpinS/AndersonTowerOrderSq.lean |
| totalSpinSOp2_mulVec_eq_zero_of_singlet | Singlet closure of the third total-spin generator (Tasaki §4.2.2, p. 108; PROVED axiom-free, Issue #4974, PR #5014): if a state Φ is annihilated by the total-spin 3-axis and 1-axis generators (Ŝ³_tot Φ = 0, Ŝ¹_tot Φ = 0), then it is automatically annihilated by the 2-axis generator (Ŝ²_tot Φ = 0), via the SU(2) commutator identity Ŝ²_tot = −i[Ŝ³_tot, Ŝ¹_tot]. Thus a total-Ŝ³/Ŝ¹-singlet is a full total-spin singlet, so all three Cartesian generators can be pushed through the later commutator-contraction words in the Proposition 4.10 sphere-average argument. | Quantum/SpinS/AndersonTowerOrderSq.lean |
| staggeredOrderOp1S_commutator_staggeredOrderOp2S | Order×order commutator [Ô_L^{(1)}, Ô_L^{(2)}] = i Ŝ³_tot (Tasaki §4.2.1–§4.2.2; PROVED axiom-free, Issue #4974, PR #5015): the commutator of the first two staggered-axis order operators yields the unstaggered total-spin generator. Per-site mechanism [Ŝ_x^{(1)}, Ô^{(2)}] = ε_x · i Ŝ_x^{(3)} summed over sites; staggering squares ε_x² = 1 cancel. Essential for contraction-word telescoping in Proposition 4.10’s sphere-average argument and RP infrastructure (§4.1 Theorem 4.2) | Quantum/SpinS/AndersonTowerEnergyBoundSU2.lean |
| staggeredOrderOp2S_commutator_staggeredOrderOpS | Order×order commutator [Ô_L^{(2)}, Ô_L^{(3)}] = i Ŝ¹_tot (Tasaki §4.2.1–§4.2.2; PROVED axiom-free, Issue #4974, PR #5015): same staggering-cancellation mechanism via per-site [Ŝ_x^{(2)}, Ô^{(3)}] = ε_x · i Ŝ_x^{(1)} yields the unstaggered total-Ŝ¹. | Quantum/SpinS/AndersonTowerEnergyBoundSU2.lean |
| staggeredOrderOpS_commutator_staggeredOrderOp1S | Order×order commutator [Ô_L^{(3)}, Ô_L^{(1)}] = i Ŝ²_tot (Tasaki §4.2.1–§4.2.2; PROVED axiom-free, Issue #4974, PR #5015): same staggering-cancellation mechanism via per-site [Ŝ_x^{(3)}, Ô^{(1)}] = ε_x · i Ŝ_x^{(2)} yields the unstaggered total-Ŝ². | Quantum/SpinS/AndersonTowerEnergyBoundSU2.lean |
| cartWord / cartWord_cons / cartWord_append / cartWord_ofFn / cartWord_swap_diff_eq | cartWord basis (Tasaki §4.2.2, Prop 4.10; PROVED axiom-free, Issue #4974, PR #5016): Fin 3–indexed order-word basis for Cartesian decomposition of staggered-order operators. The order words w : List (Fin 3) encode products of the three staggered axis operators indexed by axis coordinate; cartWord A N w accumulates the operator product ŵ = ∏ᵢ ô^{(wᵢ)} with support on A; cartWord_cons and cartWord_append prove recursive list structure ((α :: w) and w ++ w' expansions); cartWord_ofFn constructs from finite indexing via Fin.ofFn; cartWord_swap_diff_eq records the operator identity for adjacent-transposition swap differences, the Cartesian analogue of Theorem 4.9’s orderWordProd_swap_diff_eq. Both swap-diff lemmas feed the sphere-average contraction in Prop 4.10’s combined word-cancellation argument. | Quantum/SpinS/AndersonTowerCartWord.lean |
| totalSpinSOp2_commutator_staggeredOrderOp1S / totalSpinSOp2_commutator_staggeredOrderOpS | Total×order commutators (Tasaki §4.2.2, p. 108; PROVED axiom-free, Issue #4974, PR #5016): off-diagonal commutation relations completing the full 3×3 Cartesian total-spin × staggered-order matrix. [Ŝ²_tot, Ô_L^{(1)}] = −i·Ô_L^{(3)} (totalSpinSOp2_commutator_staggeredOrderOp1S, per-site [Ŝ²_tot, ô^{(1)}] = −i·ô^{(3)} derived from SU(2) identity Ŝ² = −i[Ŝ³, Ŝ¹]) and [Ŝ²_tot, Ô_L^{(3)}] = i·Ô_L^{(1)} (totalSpinSOp2_commutator_staggeredOrderOpS, via Ŝ² = −i[Ŝ³, Ŝ¹]). Together with the diagonal [Ŝ³_tot, Ô^{(3)}] = 0 (Lemma 4.5, PR #4598) and three order×order commutators {(1,2), (2,3), (3,1)} (PR #5015), this completes all 9 matrix entries essential for Prop 4.10’s Cartesian sphere-average argument. | Quantum/SpinS/AndersonTowerEnergyBoundSU2.lean |
| leviCivita3 / totalSpinSOpVec / totalSpinSOp1_commutator_staggeredOrderOp1S / totalSpinSOp2_commutator_staggeredOrderOp2S / totalSpinSOp3_commutator_staggeredOrderOpS / totalSpinSOpVec_commutator_stagOpVec | Levi-Civita bookkeeping for total×order rotation commutators (Tasaki §4.2.2, p. 108; PROVED axiom-free, Issue #4974, PR #5017): the swap-band telescoping of Prop 4.10 lifts total-spin generators through staggered-order words via uniform rotation. Levi-Civita symbol leviCivita3 γ β δ : ℂ — the totally antisymmetric symbol ε_{γβδ normalized ε_{012}=1, taking ±1 on even/odd permutations and 0 when indices coincide, carrying the axis double-index in the rotation identity as a scalar coefficient folded by Finset.sum. Total-spin vector totalSpinSOpVec Λ N γ : Fin 3 → ManyBodyOpS — the three Cartesian generators Ŝ^{(γ)}_tot bundled over γ like stagOpVec. Diagonal commutators [Ŝ^{(γ)}_tot, ô^{(γ)}] = 0 for γ=1,2,3 (totalSpinSOp{1,2,3}_commutator_staggeredOrder{Op1S,Op2S,OpS}): same-axis generators commute with their own axis operators (ε_{γγδ}=0). Uniform single-letter rotation totalSpinSOpVec_commutator_stagOpVec: the capstone merging six off-diagonal + three diagonal commutators into one axiom-free statement [Ŝ^{(γ)}_tot, ô^{(β)}] = i Σ_δ ε_{γβδ} ô^{(δ)} — the one-letter step of Prop 4.10’s swap-band contraction; axis case split (fin_cases) isolated to this proof. | Quantum/SpinS/AndersonTowerLeviCivita.lean |
| stagOpVec_commutator_eq / totalSpinSOpVec_mul_cartWord_eq / totalSpinSOpVec_mulVec_cartWord_singlet / orderComm_mulVec_cartWord_singlet / cartWord_swap_dotProduct_eq | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/AndersonTowerTelescoping.lean |
| cartWord_swap_re_diff_le / cartWord_adjSwap_re_diff_le / cartWord_swapChain_re_diff_le / stagOpVec_manyBodyOperatorNormS_le / cartWord_manyBodyOperatorNormS_le / cartWord_expectation_re_abs_le / cartWord_swapChain_re_diff_norm_le | Cartesian real-part band inequalities (Tasaki §4.2.2, Prop 4.10 arc PR-3.3a; PROVED axiom-free, Issue #4974, PR #5019, p. 108): the band layer converting Cartesian order-word swap-difference equalities (PR #5018) into real-part bounds feeding Prop 4.10’s main-part identification (PR-3.3b). Three-level hierarchy: (1) Single adjacent-swap real band (cartWord_swap_re_diff_le): term-by-term bounding of the 9·|suf| triple-sum terms by uniform B, using the real-valued Levi-Civita coefficients (no imaginary-part cancellation needed unlike Theorem 4.9 Bool band). (2) AdjSwap / branching chain bands (cartWord_adjSwap_re_diff_le, cartWord_swapChain_re_diff_le): one transposition/length-k chain of transpositions changes the real expectation by 9n·B/k·9n·B respectively, with n = w.length. (3) Uniform operator-norm scale (stagOpVec_manyBodyOperatorNormS_le, cartWord_manyBodyOperatorNormS_le, cartWord_expectation_re_abs_le): concrete self-contained bound B = (V·N)^{n−2} · ⟨Φ, Φ⟩.re from axis-operator norm (via triangle inequality) and Cartesian word norm (via submultiplicativity) and operator Cauchy–Schwarz. (Capstone) cartWord_swapChain_re_diff_norm_le: the self-contained instantiation yielding the k · 9n · (V·N)^{n−2} · ⟨Φ, Φ⟩.re real band consumed by Prop 4.10’s ordered→grouped contraction. AdjSwap/SwapChain polymorphism: both Bool (Theorem 4.9) and Cartesian layers now use the abstract AdjSwap and SwapChain (OrderOperatorAlgebra.lean), enabling shared infrastructure. Band inequalities only; main-part identification & pinch (eq. 4.2.58–4.2.59 right-hand RHS) are PR-3.3b. | Quantum/SpinS/AndersonTowerCartWordReBand.lean |
| mulVec_toLp_norm_le / sqrt_vecNormSqRe_eq_toLp_norm / sqrt_vecNormSqRe_mulVec_le / totalSpinSOp1_manyBodyOperatorNormS_le / totalSpinSOp2_manyBodyOperatorNormS_le / stagOpVec_commutator_manyBodyOperatorNormS_le / cartWord_adjSwap_manyBodyOperatorNormS_diff_le / cartWord_swapChain_manyBodyOperatorNormS_diff_le | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/ManyBodyOperatorNorm.lean / Quantum/SpinS/AndersonTowerCartWordReBand.lean |
| bringToFront / swapDist_le_length_sq / groupedFin3 / groupedFin3_count / ofFn_swapChain_groupedFin3 | Grouped normal form via bounded swap chain (Tasaki §4.2.2, Prop 4.10 arc PR-3.3b-α; PROVED axiom-free, Issue #4974, PR #5021, p. 108): the purely combinatorial pinch-step prerequisites converting an arbitrary Cartesian order word into its canonical grouped normal form (all 0-letters, then all 1-letters, then all 2-letters) by an adjacent-swap sequence of bounded length. (1) Generic alphabet swap infrastructure in OrderOperatorAlgebra.lean: bringToFront {α : Type*} generalizes the binary-ladder version (Theorem 4.6) to arbitrary decidable-equality letters (Bool-independent proof), moving one letter a ∈ w to the head in ≤ w.countP (·≠a) transpositions; swapDist_le_length_sq : Perm w w' → ∃ k ≤ (w.length)², SwapChain k w w' bounds any two permutation-equivalent words by the loose length² diameter (feeds the Fin 3 case via List.Perm). (2) Fin 3 grouped normal form in AndersonTowerGroupedNormalForm.lean: groupedFin3 (k : Fin 3→ℕ) is the canonical grouped word (counts vector to word expansion); groupedFin3_count preserves per-letter counts (ensuring permutation equivalence); ofFn_swapChain_groupedFin3 : List.ofFn f → groupedFin3 (count) connects an arbitrary Cartesian word to its normal form by a swap chain of length ≤ M² (where M = (List.ofFn f).length). Pinch-equation implementations (eq. 4.2.58–4.2.59) are PR-3.3b proper. | Quantum/SpinS/OrderOperatorAlgebra.lean / Quantum/SpinS/AndersonTowerGroupedNormalForm.lean |
| card_ofFn_count_eq | Multinomial fiber cardinality (Tasaki §4.2.2, Prop 4.10 arc PR-3.3b-β; PROVED axiom-free, Issue #4974, PR #5022, p. 108): purely combinatorial prefix to the pinch estimate — for any finite alphabet ι : Fintype and length vector (k : ι → ℕ) with ∑ i, k i = n, the number of functions f : Fin n → ι whose word List.ofFn f contains each letter exactly k i times equals the multinomial coefficient Nat.multinomial univ k = n! / ∏ i, (k i)!. Generalizes the binary special case card_ofFn_count_true_eq (Bool alphabet / binomial coefficient) to arbitrary finite alphabets, enabling the multiplicity conversion in Prop 4.10’s grouped-word pinch equation (eqs. 4.2.58–4.2.59 RHS). Pure combinatorics; the pinch-equation main identification and real-part O(1/V) bound are PR-3.3b proper. | Math/Combinatorics/MultinomialFiber.lean |
| count_ofFn_eq_card_filter | Letter count bridge (Tasaki §4.2.2, Prop 4.10 arc PR-3.3b-γ; PROVED axiom-free, Issue #4974, PR #5024, p. 108): for f : Fin n → ι the letter count form (List.ofFn f).count a equals the fibre cardinality (univ.filter (fun j => f j = a)).card, bridging the list-count representation (sphere-moment/order-word estimates) and the set-filter cardinality form (position-selection counting). Generalizes the two-letter helper count_true_ofFn (Bool alphabet) to arbitrary finite alphabets. Arithmetic capstone; feeds the pinch coefficient match. | Math/Combinatorics/MultinomialFiber.lean |
| two_mul_factorial_eq | Even factorial split (Tasaki §4.2.2, Prop 4.10 arc PR-3.3b-γ; PROVED axiom-free, Issue #4974, PR #5024, p. 108): (2a)! = 2^a · a! · (2a-1)‼ splits an even factorial into even and odd double-factorial parts. Thin corollary of Nat.doubleFactorial_two_mul and Nat.factorial_eq_mul_doubleFactorial, converting the per-configuration even factorials (2 h_i)! into the odd double factorials (2 h_i - 1)‼ appearing in the sphere-moment closed form. Pure arithmetic; ingredient of the pinch coefficient match. | Math/DoubleFactorial.lean |
| pinch_coeff_match | Pinch coefficient match (Tasaki §4.2.2, Prop 4.10 arc PR-3.3b-γ; PROVED axiom-free, Issue #4974, PR #5024, p. 108, eqs. (4.2.58)/(4.2.59)): the doubled-count multinomial times the odd double-factorial sphere moment equals the multinomial coefficient up to the universal 4π / (2M+1) factor: multinomial(2h) · ∏(2h_i-1)‼ · (2M+1) = multinomial(h) · (2M+1)‼. The natural-number identity (cleared via Nat.multinomial_spec, two_mul_factorial_eq, Nat.doubleFactorial_two_mul, Nat.factorial_eq_mul_doubleFactorial) underpins the real-arithmetic pinch estimate. Arithmetic capstone of Prop 4.10’s index/cardinality layer. | Math/Combinatorics/PinchCoeff.lean |
| cartWord_sphereAverage_pinch / orderSqOp_pow_eq_sum_cartWord / sqWord / cartPinchPoly | Pinch scalar band identity (Tasaki §4.2.2, Prop 4.10 capstone PR-3.3b; PROVED axiom-free, Issue #4974, PR #5025, p. 108, eqs. (4.2.58)/(4.2.59)): the capstone theorem of Proposition 4.10’s pinch arc combining all prior steps. Three infrastructure lemmas: square word sqWord (g : Fin m → Fin 3) : List (Fin 3) — the length-2m doubled configuration (g₀,g₀,g₁,g₁,…), yielding (ô²)^m = Σ_g ô^{sqWord g} (orderSqOp_pow_eq_sum_cartWord), closure of the squared order operator as Cartesian words; pinch polynomial cartPinchPoly m — explicit m-dependent constant bundling sphere-moment weight, 4π/(2m+1) factor, and swap-chain/branching scales ((2m)² · 9(2m)). Main theorem cartWord_sphereAverage_pinch: for a total-spin singlet Φ, the sphere average of (Ô_L^n)^{2m} equals the rotationally invariant main part (4π/(2m+1))⟨Φ,(ô²)^m Φ⟩.re up to an O((V·N)^{2m−2}) error bound: |⟨Φ, (∫_{S²} (Ô_L^n)^{2m} dσ) Φ⟩.re − (4π/(2m+1))⟨Φ,(ô²)^m Φ⟩.re| ≤ cartPinchPoly(m)·(V·N)^{2m−2}·⟨Φ,Φ⟩.re. Route: (1) ordered-word expectations (sphere monomial moments, PR-2) contracted to grouped form via PR-3.3a real band; (2) squared-word expectations (sq-config sum, orderSqOp_pow_eq_sum_cartWord) contracted via same band; (3) main parts equated through grouped-normal-form multinomial match (pinch_coeff_match, PR-3.3b-γ); (4) remainder aggregated from self-contained operator-norm band. Self-contained reference: ô²-moment symbolic only; Conjecture 4.12 (mStar lower bound) and ratio limit (PR-4/5) deferred. | Quantum/SpinS/AndersonTowerPinch.lean |
| orderSqMoment / orderSqMoment_ge / orderSqMoment_sq_le / orderSqMoment_one_ge / orderSqOp_torus_posSemidef | Squared-order-operator moment lower bound (Tasaki §4.2.2, Prop 4.10 arc PR-4a; PROVED axiom-free, Issue #4974, PR #5026, p. 108, eqs. (4.2.31)/(4.2.35)–(4.2.37)): the ô²-moment lower bound R_m ≥ (q₀ · (L^d)²)^m · R_0 (where R_k = ⟨Φ, (ô²)^k Φ⟩) driving the sphere-average relative-close estimate of Proposition 4.10. The derivation is the verbatim ô²-lift of the Theorem 4.9 p̂-moment machinery in three source-independent steps: (1) Log-convexity (orderSqMoment_sq_le): ô² = orderSqOp is Hermitian and positive-semidefinite (orderSqOp_torus_isHermitian, orderSqOp_torus_posSemidef), so moments obey positive-semidefinite Cauchy–Schwarz R_{k+1}² ≤ R_k · R_{k+2} via hermitian_pow_dotProduct_split + posSemidef_re_dotProduct_mulVec_sq_le. (2) Base ratio (orderSqMoment_one_ge): from the split ô² = (L^d)² · p̂ + (ô^{(3)})² and the long-range-order hypothesis q₀ ≤ ⟨(ô^{(3)})²⟩ / (‖Φ‖² (L^d)²) (no isotropy required), we have R_1 ≥ q₀ · (L^d)² · R_0. (3) Telescoping (orderSqMoment_ge): abstract real_logConvex_geometric_lower (from Math/Analysis/RealLogConvexSequence.lean) iterates the log-convexity to geometric lower bound R_m ≥ (q₀ · (L^d)²)^m · R_0. Scope: only the q₀ one-sided lower bound; sphere-average relative-close and its L→∞ limit are sequel PR-4b; Tanaka-state infrastructure and Conjecture 4.12 (isotropy mStar = √(3q₀)) remain deferred. | Quantum/SpinS/AndersonTowerOrderSqMoment.lean / Math/Analysis/RealLogConvexSequence.lean |
| sphereAverage_orderSqMoment_relative_close | Sphere-average relative-close estimate (Tasaki §4.2.2, Prop 4.10 arc PR-4b; PROVED axiom-free, Issue #4974, PR #5027, p. 108, eqs. (4.2.58)–(4.2.59)): convert the pinch scalar band identity (cartWord_sphereAverage_pinch, PR-3.3b) from an absolute remainder into a relative one by dividing through the ô²-moment lower bound (orderSqMoment_ge, PR-4a). The volume exponent cancels as V^{2m−2} / V^{2m} = 1/V², giving the finite relative inequality |⟨Φ, (∫_{S²} (Ô_L^n)^{2m} dσ) Φ⟩.re − (4π/(2m+1)) R_m| ≤ (cartPinchPoly m · N^{2m−2} / (q₀^m · V²)) · R_m where R_m = orderSqMoment d L N Φ m. Finite relative inequality only; the L ↑ ∞ limit (Tendsto), isotropy factor 3, Φ-collapse, and Conjecture 4.12 are sequel PR-5/6. | Quantum/SpinS/AndersonTowerSphereMomentRatio.lean |
| orderSqOp_expectation_eq_three_mul_axis3 | Factor-3 diagonal isotropy of ô² (Tasaki §4.2.2, Prop 4.10 arc L4a; PROVED axiom-free, Issue #4974, PR #5028, p. 108, eqs. (4.2.57)–(4.2.58)): wrapper combining the singlet equalities staggeredOrder_sq_expectation_eq_12 and staggeredOrder_sq_expectation_eq_23 to collapse the squared-order diagonal expectation: ⟨Φ, ô² Φ⟩ = 3 · ⟨Φ, (ô^{(3)})² Φ⟩ on a total-Ŝ³/Ŝ¹-singlet. The factor 3 is load-bearing for the later collapse identification to q₀ = (mStar)². Scope: factor-3 diagonal isotropy only; per-direction generalization and Φ-collapse are L4b/L5 sequels. | Quantum/SpinS/AndersonTowerOrderSqIsotropy.lean |
| directionMoment_rotationPath_hasDerivAt_zero | Rotation-derivative vanishing in direction-moment Ward (Tasaki §4.2.2, Prop 4.10 arc L4b-ii; PROVED axiom-free, Issue #4974, PR #5032, p. 108): so(3) generator vanishes the direction moment. For rotation path t ↦ rotationPath γ n₀ t (parametrizing rotations around axis n₀ by angle γ(t)), the direction-moment scalar directionMoment A Φ M n = ⟨Φ, (ô·n)^{2M} Φ⟩ satisfies HasDerivAt (fun t => directionMoment A Φ M (rotationPath γ n₀ t)) 0 t₀ — the derivative vanishes at t₀ (critical point in n-space). Route B scalar-polynomial analysis: master Ward identity consumption (per-direction sub-arc), stepping to n-independent globalization. Scope: rotation-derivative vanishing only; n-independent generalization (L4b-iii) and Φ-collapse are L5 sequels. | Quantum/SpinS/AndersonTowerRotationDeriv.lean |
| directionTanakaTowerTerm_vecNormSqRe_indep / sphere_reachable_from_e3 / directionMoment_indep / directionStaggeredOp_isHermitian | Per-direction n-independence via arc-constancy + sphere reachability (Tasaki §4.2.2, Prop 4.10 arc L4b-iii; PROVED axiom-free, Issue #4974, PR #5033, p. 108): completes the L4b singlet-isotropy arc. The directional moment g(n)=⟨Φ,(Ô_L^n)^{2M}Φ⟩ is constant along rotation circles (arc constancy directionMoment_rotationPath_const). Every unit vector n∈S² is reachable from the north pole e₃=(0,0,1) via two rotation arcs (spherical-coordinate parametrization sphere_reachable_from_e3), so chaining arc constancy gives global isotropy g(n)=g(e₃) (directionMoment_indep). The direction order operator Ô_L^n is Hermitian (directionStaggeredOp_isHermitian), so the per-direction tower-term squared norm ‖(Ô_L^n)^M Φ‖²=Re g(n) is n-independent (directionTanakaTowerTerm_vecNormSqRe_indep), consumed by the sphere-average assembly (vector assembly/c_M fixed = PR-6). Scope: per-direction n-independence only; Φ-collapse and vector assembly are PR-6 sequels. | Quantum/SpinS/AndersonTowerDirectionIsotropy.lean |
| sphereAverage_directionStaggeredOp_pow_mulVec | Bochner mulVec interchange for sphere-average operator polynomials (Tasaki §4.2.2, Prop 4.10 arc L3; PROVED axiom-free, Issue #4974, PR #5029, p. 108): the crucial linear step enabling the sphere-average decomposition — for any operator polynomial (A_n)^k and state vector Φ, the Bochner integral over the sphere commutes with right multiplication by Φ: ∫_{S²}((A_n)^k.mulVec Φ) dσ(n) = (∫_{S²}(A_n)^k dσ(n)).mulVec Φ. Proved via ContinuousLinearMap.integral_comp_comm (CLM pushforward + ℂ-linearity of mulVec in finite dimension). Scope: interchange only; per-direction n-independent generalization (L4b-iii) and Φ-collapse are L5 sequels. | Quantum/SpinS/AndersonTowerSphereMoment.lean |
| orderSq_collapse_vecNormSqRe | Collapse identity (4.2.60) (Tasaki §4.2.2, Prop 4.10 arc L5-a; PROVED axiom-free, Issue #4974, PR #5030, p. 108, eq. (4.2.60)): pure algebraic collapse identity for the squared-order operator: vecNormSqRe(unitNormalize(B^j Φ)−Φ̂) = 2(1−R_j/(√(R_{2j}·R_0))) where B = orderSqOp, R_k = ⟨Φ, (ô²)^k Φ⟩. Scope: collapse identity only; the RHS limit toward 1 (Φ-collapse, L5-b) and per-direction generalizations (L4b) are sequel steps. Unconditionally pure algebraic; no isotropy or moment hypothesis. | Quantum/SpinS/AndersonTowerOrderSqCollapse.lean |
| solidAngleAverageTanaka_unitNormalize_eq_orderPow | Sphere-average normalisation reduction (Tasaki §4.2.2, Prop 4.10 arc PR-6a; PROVED axiom-free, Issue #4974, PR #5037, pp. 108–109, eqs. (4.2.57)–(4.2.61)): for a total-spin singlet Φ the normalised solid-angle average equals the normalisation of the single even-power sphere-integral applied to Φ: unitNormalize(solidAngleAverageTanaka Φ) = unitNormalize((∫_{S²} (Ô_L^n)^{2j} dσ(n)) Φ), where 2j = if Even M then M else M+1. The odd power of {M, M+1} integrates to zero (sphereAverageDirectionPow_odd_eq_zero); the even power survives with normalisation absorbing the fixed positive-real constant (unitNormalize_sqrt2Inv_directionOrder_eq). This is the tip consumed by the vector-remainder bridge (PR-6b) and final assembly (PR-6c). Scope: sphere-average reduction only; vector-remainder assembly and L→∞ limit are PR-6b/6c sequels. | Quantum/SpinS/AndersonTowerSphereReduce.lean |
| sphereMoment_grouped_eq_orderSq_grouped / cartPinchVecPoly / sphereAverage_orderSq_manyBodyOperatorNormS_diff_le / sphereAverage_orderSq_vecRemainder_le | Vector pinch bridge for sphere-average remainder bound (Tasaki §4.2.2, Prop 4.10 arc PR-6b-ii; PROVED axiom-free, Issue #4974, PR #5041, p. 108, eqs. (4.2.58)–(4.2.59)): the L² vector-norm remainder bound, converting operator-norm swap-band bounds (cartWord_swapChain_manyBodyOperatorNormS_diff_le, PR-6b-i) into vector pinch via solid-angle average. Tip B capstone sphereAverage_orderSq_vecRemainder_le: the solid-angle-average vector distance from the main part (4π/(2j+1))(ô²)^j Φ is bounded by √(cartPinchVecPoly m · N^{2m−2} / (q₀^m · V²)) · √R_0 (Tasaki eqs. (4.2.58)–(4.2.59), p. 108). Helper lemmas sphereMoment_grouped_eq_orderSq_grouped (grouped-word moment identity) and sphereAverage_orderSq_manyBodyOperatorNormS_diff_le (single-swap vector bound); both consume the PR-6b-i operator-norm infrastructure (sqrt_vecNormSqRe_mulVec_le, cartWord_swapChain_manyBodyOperatorNormS_diff_le) and the PR-6a sphere-reduce tip. Feeds the final sphere-average assembly (PR-6c, Prop 4.10 capstone). Scope: vector pinch bound only; ratio collapse & L→∞ limit are PR-6c sequels. | Quantum/SpinS/AndersonTowerSphereVecRemainder.lean |
| diagonal_tendsto_zero | Lemma 4.16 (§4.2.2, DISCHARGED axiom-free; p. 108): diagonal extraction from an iterated limit. If f : ℕ→ℕ→ℝ has lim_M lim_L f L M = 0 (each column → g M, g M → 0), then ∃ nondecreasing m : ℕ→ℕ with m(L)→∞ and lim_L f L (m L) = 0. Pure real analysis (threshold construction + Nat.findGreatest); used for the suitable M(L) in Prop 4.10 | Math/DoubleSequenceDiagonal.lean |
| InfiniteSpinSystem / IsInfiniteVolumeGroundState | Definition 4.17 (§4.3.1; eqs. (4.3.1)–(4.3.4)): ground state of the infinite-volume AFM Heisenberg model on ℤᵈ. structure InfiniteSpinSystem d A bundles the C-algebra A, spin ops Ŝ_x^(α), translation automorphisms τ_x (with action laws τ_0=id, τ_x∘τ_y=τ_{x+y} and spin covariance τ_x(Ŝ_y^(α))=Ŝ_{y+x}^(α), eq. 4.3.3); helpers evenSite/bond/spinDot/TranslationInvariant. A state ρ is a ground state iff it is translation-invariant with ρ(Ŝ_x·Ŝ_y)=ε_GS for all bonds. bond is now a wrapper over the graph-centric Lattice.hypercubicLatticeGraph d adjacency (bond_iff_adj). Reuses IsState/WeakDual (Appendix A) | Quantum/SpinS/InfiniteVolumeGroundState.lean |
| IsErgodic / IsPhysicalGroundState | Definitions 4.18 + 4.19 (§4.3.1; eqs. (4.3.5)–(4.3.6)): ergodic & physical ground states. Bulk op Â_n = Σ_{x∈Λ_n∩even} τ_x  over the centered even box Λ_n={−n<x_i≤n} (side 2n). A TI state is ergodic (IsErgodic) iff for every self-adjoint local Â∈A_loc (localAlg field) the density fluctuation ρ(Â_n²)/((2n)^d)² − (ρ(Â_n)/(2n)^d)² → 0 (LLN). A TI ground state is a physical ground state (IsPhysicalGroundState) iff it is ergodic | Quantum/SpinS/InfiniteVolumeGroundState.lean |
| theorem_4_20_omega0 / theorem_4_20_omegaN | Theorem 4.20 (§4.3.1, AXIOM; eqs. (4.3.7)–(4.3.10)): the concrete infinite-volume ground states exist. Conditional on IsGroundStateEnergyDensity S εGS (εGS = S’s genuine energy density, eq. 4.3.4), ω_0 (L→∞ limit of ⟨Φ_GS|·|Φ_GS⟩) is a TI ground state with ω_0(Ŝ_x)=0 (LRO, no SSB). For each unit n∈ℝ³, assuming HasStaggeredLRO S m* (m>0), ω_n (L→∞ limit of ⟨Ξ_n|·|Ξ_n⟩) is a TI ground state with ω_n(Ŝ_x^(α))=(−1)^x m* n_α (LRO + full SSB). Helpers staggeredSign, IsUnitVector | Quantum/SpinS/InfiniteVolumeGroundState.lean |
| conjecture_4_21 | Conjecture 4.21 (§4.3.1, AXIOM-FREE Prop STATEMENT; eq. after (4.3.10)): the symmetry-breaking ground states are physical. def conjecture_4_21 (S) (εGS) : Prop — every infinite-volume ground state ω with the Néel magnetization ω(Ŝ_x^(α))=(−1)^x m* n_α (the ω_n of Thm 4.20) is ergodic (hence a physical ground state, Def 4.19). Never asserted true (no axiom/theorem derives it) | Quantum/SpinS/InfiniteVolumeGroundState.lean |
| evenSite_iff_mem_hypercubicEvenSublattice / mem_hypercubicOddSublattice_iff_not_evenSite / staggeredSign_eq_one_iff_mem_hypercubicEvenSublattice / staggeredSign_eq_neg_one_iff_mem_hypercubicOddSublattice | parity bridge (§4.3, Issue #4557): the §4.3 quantum helpers evenSite / staggeredSign agree with the graph-centric bipartition Lattice.hypercubicEvenSublattice / hypercubicOddSublattice — evenSite x ↔ x ∈ ℤᵈ_even, staggeredSign x = ±1 iff x is in the even/odd sublattice. Axiom-free | Quantum/SpinS/InfiniteVolumeGroundState.lean |
| LocalSupportData / LocalSupportData.localSubalgebra / boxLocalSubalgebra / boxLocalSubalgebra_mono / spin_mem_boxLocalSubalgebra_of_mem | local-support interface of the quasi-local algebra (§4.3.1 / §A.7, Defs A.23/A.25/A.27, Issue #4644; AXIOM-FREE): the graph-centric layer between the finite boxes Λ_n = hypercubicBox d n and the abstract quasi-local C-algebra A. structure LocalSupportData S carries a support predicate Supports Λ a (a acts only on sites of Λ) closed under the *-algebra ops and monotone in Λ, with each spin op Ŝ_x^(α) supported on {x}. localSubalgebra Λ : StarSubalgebra ℂ A is the *-subalgebra A_Λ cut out by Supports Λ; localSubalgebra_mono (Λ⊆Γ → A_Λ≤A_Γ) and localSubalgebra_le_localAlg (A_Λ≤A_loc). boxLocalSubalgebra n = A_{Λ_n} with monotone increasing tower boxLocalSubalgebra_mono (nested boxes) and spin_mem_boxLocalSubalgebra_of_mem (x∈Λ_n → Ŝ_x^(α)∈A_{Λ_n}). No inductive-limit existence asserted | Quantum/SpinS/QuasiLocalSupport.lean |
| LocalSupportData.boxLocalTowerSup / boxLocalTowerClosure / boxLocalTowerSup_le_localAlg / boxLocalSubalgebra_directed / BoxTowerExhaustsLocalAlg / BoxTowerClosureIsQuasiLocalAlgebra | inductive-limit interface of the box-local tower (Appendix A.7 / §4.3.1, Issue #4644; AXIOM-FREE): boxLocalTowerSup = ⨆ₙ A_{Λ_n} and its norm closure boxLocalTowerClosure, with the axiom-free order facts (boxLocalSubalgebra_le_boxLocalTowerSup, boxLocalTowerSup_le_localAlg, directedness boxLocalSubalgebra_directed, …_le_boxLocalTowerClosure). The two operator-algebraic identifications — the tower exhausts A_loc (BoxTowerExhaustsLocalAlg) and A is the norm closure of the tower (BoxTowerClosureIsQuasiLocalAlgebra) — are def : Prop hypotheses, NOT asserted (LocalSupportData only gives the easy inclusion); boxLocalTowerSup_eq_localAlg_of_exhausts is the conditional consequence. No new axiom | Quantum/SpinS/QuasiLocalInductiveLimit.lean |
| boxOrderedBondPairs / boxLocalHamiltonian / LocalSupportData.spinDot_mem_localSubalgebra_of_mem / boxLocalHamiltonian_mem_boxLocalSubalgebra / boxLocalHamiltonian_mem_localAlg | finite-box partial Hamiltonian in the quasi-local algebra (§4.3.1 eq. (4.3.4) / §A.7, Issue #4644; AXIOM-FREE): the finite-box AFM Heisenberg Hamiltonian Ĥ_{Λ_n} = ½ Σ_{(x,y) bond in Λ_n} Ŝ_x·Ŝ_y of an InfiniteSpinSystem, as an element of the abstract quasi-local C-algebra A. boxOrderedBondPairs d n is the ordered adjacent vertex pairs of the induced box graph (mem_boxOrderedBondPairs, swap_mem_boxOrderedBondPairs); the ½ compensates the ordered double sum (no Ŝ_x·Ŝ_y=Ŝ_y·Ŝ_x symmetry is assumed). spinDot_mem_localSubalgebra_of_mem (both endpoints in Λ ⟹ bond op in A_Λ) gives boxLocalHamiltonian_mem_boxLocalSubalgebra (Ĥ_{Λ_n}∈A_{Λ_n}) and boxLocalHamiltonian_mem_localAlg (Ĥ_{Λ_n}∈A_loc). No self-adjointness/commutativity claimed; abstract A not identified with the finite-matrix model | Quantum/SpinS/BoxLocalHamiltonian.lean |
| InfiniteSpinSystem.bond_add_right_iff / transl_spinDot / transl_bulkOp / translatedBoxLocalHamiltonian / transl_boxLocalHamiltonian | translation covariance of the local finite-box observables (§4.3.1 eqs. (4.3.3)–(4.3.6) / §A.7, Issue #4644; AXIOM-FREE): how the local observables transform under the translation automorphisms τ_x. bond_add_right_iff (bond (y+x) (z+x) ↔ bond y z); transl_spinDot (τ_x(Ŝ_y·Ŝ_z) = Ŝ_{y+x}·Ŝ_{z+x}, from transl_spin + StarAlgEquiv multiplicativity); transl_bulkOp (τ_x Â_n = (τ_x Â)_n); the translated box translatedLatticeBox d x n = Λ_n + x (mem_translatedLatticeBox); translatedBoxLocalHamiltonian Ĥ_{Λ_n+x} with transl_boxLocalHamiltonian (τ_x Ĥ_{Λ_n} = Ĥ_{Λ_n+x}) and the shifted-box locality lemmas translatedBoxLocalHamiltonian_mem_localSubalgebra/_mem_localAlg + transl_boxLocalHamiltonian_mem_localSubalgebra/_mem_localAlg. No self-adjointness/commutativity used | Quantum/SpinS/BoxLocalTranslation.lean |
| boxOrderedBondPairs_card_eq_two_mul_boxBondCount / boxLocalHamiltonianEnergyDensity / HasBoxLocalHamiltonianEnergyDensity / IsInfiniteVolumeGroundState.boxLocalHamiltonian_apply / boxLocalHamiltonianEnergyDensity_eq / hasBoxLocalHamiltonianEnergyDensity | box-local energy density of the abstract partial Hamiltonian (§4.3.1 eq. (4.3.4), Issue #4644; AXIOM-FREE, no new axiom): connects boxLocalHamiltonian to Tasaki’s per-bond ground-state energy density ε_GS (Def 4.17). The ordered box bonds number 2·|B_n| (boxOrderedBondPairs_card_eq_two_mul_boxBondCount, via the graph dart count). In any infinite-volume ground state ω the ½-scaled ordered bond sum collapses: ω(Ĥ_{Λ_n}) = |B_n|·ε_GS (boxLocalHamiltonian_apply), so the normalized density boxLocalHamiltonianEnergyDensity = ω(Ĥ_{Λ_n}).re/|B_n| equals ε_GS for nonempty boxes (boxLocalHamiltonianEnergyDensity_eq) and converges to it (hasBoxLocalHamiltonianEnergyDensity; HasBoxLocalHamiltonianEnergyDensity is a named convergence Prop). Genuine existence of ε_GS/limit states stays in the existing documented axioms | Quantum/SpinS/BoxLocalEnergyDensity.lean |
| TranslationInvariant.spinDot_add_right_apply / transl_boxLocalHamiltonian_apply / translatedBoxLocalHamiltonian_apply_eq / translatedBoxLocalHamiltonianEnergyDensity / IsInfiniteVolumeGroundState.translatedBoxLocalHamiltonian_apply / hasTranslatedBoxLocalHamiltonianEnergyDensity | translation-invariant expectations of the local finite-box observables (§4.3.1 eqs. (4.3.3)–(4.3.6), Issue #4644; AXIOM-FREE): state-level consequences of the translation covariance. For a translation-invariant state ω and an even shift x, ω(Ŝ_{y+x}·Ŝ_{z+x}) = ω(Ŝ_y·Ŝ_z) (spinDot_add_right_apply), ω((τ_x Â)_n)=ω(Â_n) (bulkOp_transl_apply), ω(Ĥ_{Λ_n+x})=ω(Ĥ_{Λ_n}) (translatedBoxLocalHamiltonian_apply_eq), and the shifted-box energy density translatedBoxLocalHamiltonianEnergyDensity agrees with the centered one. For an infinite-volume ground state the bond condition is uniform, so for every shift ω(Ĥ_{Λ_n+x})=|B_n|·ε_GS=ω(Ĥ_{Λ_n}) (IsInfiniteVolumeGroundState.translatedBoxLocalHamiltonian_apply/_eq_boxLocal) and the shifted-box density equals/converges to ε_GS (translatedBoxLocalHamiltonianEnergyDensity_eq, hasTranslatedBoxLocalHamiltonianEnergyDensity). No new axiom | Quantum/SpinS/BoxLocalTranslationInvariant.lean |
| InfiniteSpinSystem.evenLatticeBox / bulkOp_add / bulkOp_smul / bulkOp_finset_sum / bulkOp_spin_eq_sum / bulkOp_spinDot_eq_sum / LocalSupportData.bulkOp_spin_mem_localAlg / bulkOp_spinDot_mem_localAlg / TranslationInvariant.bulkOp_apply_eq_card_mul | algebra of the bulk operator Â_n (§4.3.1 eqs. (4.3.5)–(4.3.6), Issue #4644; AXIOM-FREE): the constructive algebra of  ↦ Â_n = Σ_{x∈Λ_n∩ℤᵈ_even} τ_x  (evenLatticeBox = the index set). It is ℂ-linear (bulkOp_zero/bulkOp_add/bulkOp_smul/bulkOp_finset_sum); the bulk of a spin/bond operator expands over shifted even sites (bulkOp_spin_eq_sum, bulkOp_spinDot_eq_sum); these bulk observables are local (bulkOp_spin_mem_localSubalgebra/_mem_localAlg, bulkOp_spinDot_mem_localSubalgebra/_mem_localAlg, supported in the translated box / union); and for a translation-invariant state ω(Â_n) = \|Λ_n∩ℤᵈ_even\|·ω(Â) (bulkOp_apply_eq_card_mul). No new axiom | Quantum/SpinS/BulkOperator.lean |
| InfiniteSpinSystem.bulkVolume / latticeBox_card_real / bulkDensity / bulkDensityMean / bulkDensitySecondMoment / bulkDensityFluctuation / isErgodic_iff_tendsto_bulkDensityFluctuation / IsErgodic.tendsto_bulkDensityFluctuation | bulk density Â_n / Lᵈ and the ergodic fluctuation (§4.3.1 eqs. (4.3.5)–(4.3.6), Issue #4644; AXIOM-FREE): the macroscopic density observable and the fluctuation of Definition 4.18. bulkVolume d n = (2n)ᵈ (latticeBox_card_real: =|Λ_n|); bulkDensity = (Lᵈ)⁻¹ • Â_n is ℂ-linear (bulkDensity_zero/_add/_smul) with ω(Â_n/Lᵈ)=(Lᵈ)⁻¹·ω(Â_n) (bulkDensity_apply) and the TI value (TranslationInvariant.bulkDensity_apply_eq_card_mul/bulkDensityMean_eq_card_mul); the real moments bulkDensityMean/bulkDensitySecondMoment and the fluctuation bulkDensityFluctuation give a named restatement of ergodicity (isErgodic_iff_tendsto_bulkDensityFluctuation) plus the ergodic-state accessors. No closed form for \|Λ_n∩ℤᵈ_even\| asserted; no new axiom | Quantum/SpinS/BulkDensity.lean |
| InfiniteSpinSystem.paritySign / paritySign_add / paritySign_sum / sum_paritySign_Ioc_neg_nat / two_mul_evenLatticeBox_card / evenLatticeBox_card_real / TranslationInvariant.bulkDensity_apply_eq_half_mul / bulkDensityMean_eq_half_mul | even-sublattice cardinality \|Λ_n∩ℤᵈ_even\| = (2n)ᵈ/2 (§4.3.1, Issue #4644; AXIOM-FREE): completes the bulk-density coefficient. The parity sign ε(m)=(−1)^m is multiplicative (paritySign_add/paritySign_sum) and cancels over the symmetric interval (sum_paritySign_Ioc_neg_nat), so the box has equal even/odd counts: 2·\|Λ_n∩ℤᵈ_even\| = (2n)ᵈ (two_mul_evenLatticeBox_card, d≥1), real form evenLatticeBox_card_real (= bulkVolume/2). Hence for a translation-invariant state and n≥1, ω(Â_n/Lᵈ)=½ω(Â) (bulkDensity_apply_eq_half_mul) and Re ω(Â_n)/Lᵈ=½ Re ω(Â) (bulkDensityMean_eq_half_mul). No new axiom | Quantum/SpinS/EvenLatticeBoxCard.lean |
| InfiniteSpinSystem.IsPhysicalGroundState.* (isInfiniteVolumeGroundState / isErgodic / isState / translationInvariant / spinDot_apply / tendsto_bulkDensityFluctuation / iff_isInfiniteVolumeGroundState_and_tendsto_bulkDensityFluctuation / boxLocalHamiltonian_apply / hasBoxLocalHamiltonianEnergyDensity / translatedBoxLocalHamiltonian_apply / bulkDensity_apply_eq_half_mul) | physical-ground-state consequences (§4.3.1 Def 4.19, Issue #4644; AXIOM-FREE): capstone of the §4.3.1 constructive layer. A physical ground state (IsPhysicalGroundState = IV ground state ∧ ergodic) gets structural accessors, the bond energy condition ω(Ŝ_x·Ŝ_y)=ε_GS, vanishing bulk-density fluctuation, box/shifted-box energy density =ε_GS (and convergence), and even-sublattice half-filling ω(Â_n/Lᵈ)=½ω(Â) — all derived axiom-free from #4645–#4652. iff_… characterizes a physical ground state as an IV ground state with vanishing bulk-density fluctuations. No new axiom | Quantum/SpinS/PhysicalGroundStateConsequences.lean |
| InfiniteSpinSystem.staggeredCellSpin / staggeredBulkSpin / staggeredBulkSpinDensity / staggeredBulkSpinDensity_apply_of_zero_magnetization / staggeredBulkSpinDensity_apply_of_staggered_magnetization / IsPhysicalGroundState.tendsto_staggeredCellSpin_bulkDensityFluctuation | staggered (Néel) bulk observable (§4.3.1 eqs. (4.3.5)/(4.3.9)/(4.3.10), Issue #4644; AXIOM-FREE): the Néel order-parameter cell Ŝ_0^(α)−Ŝ_u^(α) (staggeredCellSpin, support {0,u}), its even-sublattice bulk average/density (staggeredBulkSpin/staggeredBulkSpinDensity, expansion Σ_{x∈Λ_n∩even}(Ŝ_x−Ŝ_{u+x})), with TI half-value ½ω(cell). Magnetization-conditional values (taken as hypotheses, not asserted): on a zero-magnetization state the staggered bulk density is 0 (eq. 4.3.9), on a Néel state (staggeredSign u=−1, ω(Ŝ_x)=(−1)^x m∗ n) it equals m∗ n_α (eq. 4.3.10). Locality staggeredCellSpin_mem_localAlg; physical-state fluctuation corollary. No new axiom | Quantum/SpinS/StaggeredBulkSpin.lean |
| QuasiLocalRealization / boxLocalTowerSup_eq_localAlg / boxLocalTowerClosure_eq_top / localAlg_topologicalClosure_eq_top / spin_mem_boxLocalTowerClosure / staggeredBulkSpinDensity_mem_localAlg | quasi-local realization bundle (Appendix A.7, Issue #4644; AXIOM-FREE): the sound capstone of the constructive infinite-volume layer. structure QuasiLocalRealization bundles an InfiniteSpinSystem, a LocalSupportData, and the two operator-algebraic hypotheses (BoxTowerExhaustsLocalAlg, BoxTowerClosureIsQuasiLocalAlgebra) as fields (since localAlg is a free field, these cannot be asserted globally). For any realization: boxLocalTowerSup = A_loc, boxLocalTowerClosure = ⊤, A_loc is dense (localAlg_topologicalClosure_eq_top = ⊤), and the spins / finite-box Hamiltonians / staggered bulk observables are local and lie in the realized closure. All consequences conditional + axiom-free; no global assertion | Quantum/SpinS/QuasiLocalRealization.lean |
| tasaki_4_22_magnetization_vanishes / tasaki_4_22_exponential_clustering | Theorem 4.22 (§4.4.1, AXIOMS; eqs. (4.4.1)–(4.4.6)): the 1D Heisenberg model is disordered at any nonzero temperature. New finite-temperature framework: Gibbs operator thermalGibbsOpS β H = e^{−βH}, partition thermalPartitionFnS, real canonical average thermalAverageReS β H A = Re Tr[A e^{−βH}]/Re Tr[e^{−βH}] (eq. 4.4.3); field Hamiltonians heisenbergFieldHamiltonianS ferro covering ferro (4.4.1, uniform field) and AFM (4.4.2, staggered field); torus embedding torusEmbed, ℓ¹ distance intL1Dist, even-side sequence evenSide n=2(n+1). (4.4.5) tasaki_4_22_magnetization_vanishes: lim_{h↓0} lim_{L↑∞} ⟨Ŝ_x^(3)⟩_{β,h}^L=0 (no SSB; order of limits essential), stated soundly per footnote 41 (ε–δ with inner liminf-subsequence ∃n₀ ∀n≥n₀ ∃m≥n, |mag|<ε). (4.4.6) tasaki_4_22_exponential_clustering: ∃ ξ(β),C(β)∈(0,∞) with |⟨Ŝ_x^(α)Ŝ_y^(α)⟩_{β,0}^∞| ≤ C exp(−|x−y|/ξ), bounding the concrete liminf correlation infiniteVolSpinCorrLiminf | Quantum/SpinS/HeisenbergEquilibrium.lean |
| tasaki_4_23_high_temperature_disorder | Theorem 4.23 (§4.4.1, AXIOM; eqs. (4.4.7)–(4.4.8)): the Heisenberg model in d ≥ 2 is disordered at sufficiently high temperature. Reuses the Theorem 4.22 finite-temperature framework at general d (hd : 2 ≤ d): there exists β₀ ∈ (0,∞) (depending only on d and S, not on the ferro/AFM flag — ferro is universally quantified under ∃ β₀) such that for every β ∈ [0, β₀], (4.4.7) the magnetization vanishes lim_{h↓0} lim_{L↑∞} ⟨Ŝ_x^(3)⟩_{β,h}^L = 0 (same ε–δ / liminf-subsequence form) and (4.4.8) ∃ ξ(β),C(β)∈(0,∞) with |⟨Ŝ_x^(α)Ŝ_y^(α)⟩_{β,0}^∞| ≤ C exp(−|x−y|/ξ). The shared high-temperature threshold β₀ binds both statements and both models under one outer existential (cluster-expansion technique, Tasaki [21,50,61]) | Quantum/SpinS/HeisenbergEquilibrium.lean |
| improved_hohenberg_mermin_wagner | Theorem 4.24 (§4.4.3, AXIOM; eqs. (4.4.21)–(4.4.22)): the improved Hohenberg–Mermin–Wagner theorem — the 2D Heisenberg model exhibits no magnetic ordering of any type at any nonzero temperature. New generalizedFieldHamiltonianS J ξ (eq. 4.4.21): J Σ Ŝ·Ŝ − h Σ_x Σ_α (ξ_x^α) Ŝ_x^(α) (field h_x = h ξ_x) with J ∈ {−1,+1} and an arbitrary fixed field-direction family ξ (\|ξ_x\| ≤ 1), generalizing the uniform/staggered fields; finiteVolMagnetizationGenS is its finite-volume Gibbs magnetization ⟨Ŝ_x^(α)⟩_{β,h}^L. For d=2, any β ∈ [0,∞), every J=±1, every bounded ξ, every component α=1,2,3, and every x ∈ ℤ²: lim_{h↓0} lim_{L↑∞} ⟨Ŝ_x^(α)⟩_{β,h}^L = 0 (4.4.22). Per footnote 48 the inner limit is a limsup, so the sound form is eventual (∃n₀ ∀n≥n₀, all large even volumes) — stronger than the liminf-subsequence form of 4.22/4.23. Proof: McBryan–Spencer complex-translation method (no translation invariance needed) | Quantum/SpinS/HeisenbergEquilibrium.lean |
| mcbryan_spencer_koma_tasaki | Theorem 4.25 (§4.4.3, AXIOM; eqs. (4.4.23)–(4.4.24)): the McBryan–Spencer / Koma–Tasaki power-law bound — in d=2 at h=0 the finite-volume two-point correlation finiteVolSpinCorrS decays at least as a power law: there is an L-independent positive decreasing exponent η(β) with \|⟨Ŝ_x^(α)Ŝ_y^(α)⟩_{β,0}^L\| ≤ 2S² \|x−y\|^{−η(β)} (Real.rpow) for every α=1,2,3, β∈[0,∞), and every pair of distinct sites with 0 < \|x−y\| < L/2. The distinctness 0<\|x−y\| is required for soundness (Real.rpow 0 (−η)=0 in Lean, so the bound would be false at x=y where the self-correlation is positive). η(β) ≃ (16CS²β)^{−1} for large β; the same η is bound before ferro (works for both signs). Weaker than the conjectured exponential decay but already excludes 2D long-range order | Quantum/SpinS/HeisenbergEquilibrium.lean |
| theorem_4_26_staggered_lro | Theorem 4.26 (§4.4.4, AXIOM; eq. (4.4.52)): the Dyson–Lieb–Simon theorem — genuine Néel long-range order at sufficiently low temperature in d ≥ 3. New per-axis staggered order operator staggeredOrderOpAxisS α A N (α=0/1/2 → Ô^(1)/Ô^(2)/Ô^(3)). For the AFM Heisenberg model with d ≥ 3 (hd : 3 ≤ d) and any S = N/2 with N ≥ 1 ([NeZero N]): there exist β₀ ∈ (0,∞) and q(β) with q(β) > 0 for β > β₀ such that ⟨(Ô_L^(α)/L^d)²⟩_{β,0}^L = ⟨(Ô_L^(α))²⟩_{β,0}^L / (L^d)² ≥ q(β) for every α=1,2,3, every β > β₀, and all sufficiently large even volumes (the squared operator Ô_L^(α)/L^d gives the (L^d)² normalization — the intensive LRO density, as in §4.1/§4.2). [NeZero N] is essential for soundness (at N=0 the order operator vanishes, contradicting q(β)>0). Proof: reflection positivity (DLS; d=3,S=1/2 via Kennedy–Lieb–Shastry). The ferromagnetic LRO is only conjectured (RP fails) | Quantum/SpinS/HeisenbergEquilibrium.lean |
| theorem_4_27_griffiths_koma_tasaki_ssb | Theorem 4.27 (§4.4.4, AXIOM; eq. (4.4.53)): the Griffiths / Koma–Tasaki theorem — under the same conditions as Theorem 4.26 (AFM, d ≥ 3, N ≥ 1 [NeZero N]), low-temperature LRO is accompanied by genuine SSB. With the staggered field (eq. 4.4.2), lim_{h↓0} lim_{L↑∞} ⟨Ô_L^(3)⟩_{β,h}^L / L^d ≥ √(3 q(β)) for β > β₀. The axiom bundles the Theorem 4.26 LRO bound (4.4.52) and the SSB bound (4.4.53) under one shared ∃β₀ ∃q, making the “same q” dependence explicit; the √3 has the same origin as Theorem 4.11. Double limit in ε–δ form (outer h↓0, inner liminf as eventual lower bound). Proof: Koma–Tasaki (extending Griffiths) | Quantum/SpinS/HeisenbergEquilibrium.lean |
← Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1) · Catalogue · Bose–Einstein condensation of hard-core bosons (Tasaki §5.1–§5.2) →