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
Start of the Chapters 3–10 backfill (Issue #4485; book order, infinite systems in scope). Tasaki §3.4, Theorem 3.1, eqs. (3.4.7)–(3.4.12), pp. 66–67.
| Lean name | Statement | File |
|—|—|—|
| horsch_vonderLinden_lowLying | for Hermitian H with min eigenvalue E₀ = eigenvalues i₀, a unit state Γ orthogonal to the ground eigenvector with ⟨Γ,HΓ⟩ ≤ E₀+δ yields an energy eigenstate j ≠ i₀ with E₀ ≤ E_j ≤ E₀+δ (a low-lying state; possibly another ground state if degenerate, as Tasaki notes) | Quantum/HorschVonderLinden.lean |
| kaplan_horsch_vonderLinden_order_lower_bound | Theorem 3.2, finite-volume core (§3.4; the thermodynamic double limit 3.4.22 is not formalized): for the field-perturbed ground state Ψ of H − h·O (h>0) and any trial Ξ, the order parameter obeys ⟨Ξ,OΞ⟩ + (E₀−⟨Ξ,HΞ⟩)/h ≤ ⟨Ψ,OΨ⟩ (eq. (3.4.21), the variational core; the double limit L↑∞,h↓0 gives the √q₀ SSB bound) | Quantum/KaplanHorschVonderLinden.lean |
| staggeredOrderOpS / staggeredOrderOpS_isHermitian | Theorem 4.1 (§4.1, Dyson–Lieb–Simon, toward; eq. (4.1.7)): the staggered (Néel) order operator Ô = Σ_x ε_x Ŝ_x^(3) (ε_x = ±1 sublattice sign) and its Hermiticity (real ±1 combination of Hermitian Ŝ_x^(3)), so ⟨Φ,Ô²Φ⟩ is a real order parameter. The Néel-LRO statement needs the actual hypercubic torus + reflection positivity (false for arbitrary bipartite graphs); deferred pending that infrastructure (infinite-volume in scope) | Quantum/SpinS/DysonLiebSimon.lean |
| shastry_no_symmetry_breaking_1d | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/ShastryNoSSB.lean, Quantum/SpinS/RingBondReflection.lean, Quantum/SpinS/RingReflectionTheta.lean, Quantum/SpinS/RingReflectionHamiltonian.lean, Quantum/SpinS/RingReflectionPositivity.lean, Quantum/SpinS/RingReflectionTraceCone.lean, Quantum/SpinS/RingReflectionWeightedCone.lean, Quantum/SpinS/RingReflectionGibbsCone.lean, Quantum/SpinS/RingReflectionGibbsExp.lean, Quantum/SpinS/RingReflectionExpSupport.lean, Quantum/SpinS/RingReflectionTwoFieldPairing.lean, Quantum/SpinS/RingReflectionRPDecomposition.lean |
| refLeftSum | RP infra layer 4b (RingReflectionTraceCone.lean, §4.1, Shastry base / PR #4977): the left-diagonal coordinate S(A) = ∑_ℓ A_{(ℓ,ℓ),(ℓ,ℓ)}, the scalar “square root” of a left-supported operator entering the reflection-positive factorization Tr(θ(A)·B) = conj(S A)·S B; fundamental to the genuine bilinear generalization of trace positivity | Quantum/SpinS/RingReflectionTraceCone.lean |
| trace_theta_mul_eq_refLeftSum_mul | RP infra layer 4b (RingReflectionTraceCone.lean, §4.1, Shastry base / PR #4977): the bilinear reflection base identity Tr(θ(A)·B) = conj(S A)·S B for left-supported operators, the genuine bilinear generalization (and proof engine) of trace reflection positivity; the foundation on which the Gibbs / doubled Cauchy–Schwarz layer of the Dyson–Lieb–Simon / Shastry argument is built (Tasaki §4.1, Theorem 4.2, as infrastructure toward its proof) | Quantum/SpinS/RingReflectionTraceCone.lean |
| twoField_product_pairing | RP infra layer 7b (RingReflectionTwoFieldPairing.lean, Tasaki §4.1, toward Theorem 4.2 / PR #4990): the two-field SWEEP operator identity — the doubled Dyson–Lieb–Simon approximant (g(x)·θ(g(y))·∑ᵢ wᵢ·(θ(Cᵢ(y))·Cᵢ(x)))^m (with left-supported kinetic family g, nonnegative weights wᵢ ≥ 0, and FIELD-DEPENDENT left-supported cone generators Cᵢ(z) — the reflected pile carrying the y-field factor Cᵢ(y), the non-reflected pile the x-field factor Cᵢ(x)) collapses into a nonnegative reflection pairing ∑ₖ vₖ·(θ(𝓛ₖ(y))·𝓛ₖ(x)) over the crossing family κ = ιᵐ, where vₖ = ∏ w ≥ 0 and the pattern-shared family 𝓛ₖ(z) (left-supported, depending on the field only through z) carries the SAME crossing sequence in both piles — proved by induction via sweep_operator_identity (the single SWEEP step) with the disjoint-support commutation and θ’s multiplicativity. The field-free pairing is the constant specialization Cᵢ(z) := Cᵢ (Tasaki §4.1 Theorem 4.2, crossing identity (4.1.65)–(4.1.69), p. 90). | Quantum/SpinS/RingReflectionTwoFieldPairing.lean |
| twoField_product_pairing_trace | RP infra layer 7b (RingReflectionTwoFieldPairing.lean, Tasaki §4.1, toward Theorem 4.2 / PR #4990): taking the trace of the SWEEP identity twoField_product_pairing and applying the bilinear reflection base identity trace_theta_mul_eq_refLeftSum_mul termwise yields the weighted ℓ² Gram form Tr(U) = ∑ₖ vₖ · conj(refLeftSum 𝓛ₖ(y)) · refLeftSum 𝓛ₖ(x) (the doubled reflection Cauchy–Schwarz pairing consumed by the next PR7b-iii-b/c layer) — field-dependent crossing generators (Tasaki §4.1 Theorem 4.2, (4.1.65)–(4.1.69), p. 90). | Quantum/SpinS/RingReflectionTwoFieldPairing.lean |
| falkBruch_double_commutator | Cor 4.3 / Falk–Bruch (FalkBruchDoubleCommutator.lean, Tasaki §4.1, toward Corollary 4.3): the concrete ground-state Falk–Bruch inequality — for a ground state Φ, Hermitian A and a potential y for AΦ ((H−E₀)y = AΦ), 2(Re⟨Φ,A²Φ⟩)² ≤ Re⟨Φ,[A,[H,A]]Φ⟩·Re⟨y,AΦ⟩; combines the abstract Falk–Bruch (K = H−E₀ PSD) with the double-commutator = variational-energy identity | Quantum/SpinS/FalkBruchDoubleCommutator.lean |
| hermitianSubMin_posSemidef | Cor 4.3 / Falk–Bruch (HermitianSubMinPosSemidef.lean, Tasaki §4.1, toward Corollary 4.3): the Hamiltonian shifted to its ground energy H − E₀ (E₀ = hermitianMinEigenvalue) is positive-semidefinite — the quadratic form is real (Hermiticity, isHermitian_dotProduct_mulVec_im_zero) with nonnegative real part (the variational lower bound); this is the PSD K fed into the Falk–Bruch inequality | Quantum/SpinS/HermitianSubMinPosSemidef.lean |
| falkBruch_of_mulVec_eq | Cor 4.3 / Falk–Bruch (FalkBruch.lean, Tasaki §4.1, toward Corollary 4.3): the abstract ground-state Falk–Bruch inequality — for PSD K and w in the range of K (K y = w), (Re⟨w,w⟩)² ≤ Re⟨w,K w⟩·Re⟨y,w⟩, an immediate instance of the PSD Cauchy–Schwarz (posSemidef_re_dotProduct_mulVec_sq_le) with second argument y; no spectral theory / pseudo-inverse needed | Quantum/SpinS/FalkBruch.lean |
| double_commutator_ground_state_nonneg | Cor 4.3 / Falk–Bruch (DoubleCommutatorNonneg.lean, Tasaki §4.1, toward Corollary 4.3): the ground-state double commutator Re⟨Φ, [A,[H,A]] Φ⟩ ≥ 0 for Hermitian A and a minimal-eigenvalue eigenvector Φ — it equals twice the variational energy of AΦ, nonnegative since the ground energy is the Rayleigh minimum (hermitianMinEigenvalue_mul_dotProduct_re_le_rayleighOnVec); the sign of the Falk–Bruch numerator | Quantum/SpinS/DoubleCommutatorNonneg.lean |
| double_commutator_ground_state_eq | Cor 4.3 / Falk–Bruch (DoubleCommutatorVariational.lean, Tasaki §4.1, toward Corollary 4.3): for Hermitian H, A and a ground state HΦ = E₀Φ (E₀ real), the f-sum-rule oscillator strength equals twice the variational energy of AΦ — ⟨Φ, [A,[H,A]] Φ⟩ = 2⟨AΦ, H AΦ⟩ − 2E₀⟨AΦ, AΦ⟩ (Hermitian-shift); the denominator of the ground-state Falk–Bruch inequality | Quantum/SpinS/DoubleCommutatorVariational.lean |
| spinSDot_double_commutator_onSiteS_spinSOp3 | Cor 4.3 / f-sum-rule (SingleBondDoubleCommutator.lean, Tasaki §4.1, toward Corollary 4.3): the per-bond double commutator is the negated transverse bond energy [Ŝ_a^{(3)}, [Ŝ_a·Ŝ_b, Ŝ_a^{(3)}]] = −(Ŝ_a^{(1)}Ŝ_b^{(1)} + Ŝ_a^{(2)}Ŝ_b^{(2)}) (the f-sum-rule integrand / oscillator strength of the staggered mode), bounded by the bond energy | Quantum/SpinS/SingleBondDoubleCommutator.lean |
| heisenbergHamiltonianS_commutator_onSiteS | Cor 4.3 / IR bound (HeisenbergSpinSOp3Commutator.lean, Tasaki §4.1, toward Corollary 4.3): the Heisenberg Hamiltonian commutator distributes over bonds [Ĥ_J, Ŝ_z^{(3)}] = Σ_x Σ_y J_{xy} [Ŝ_x·Ŝ_y, Ŝ_z^{(3)}]; with the per-bond case analysis this reduces the spin-current divergence [Ĥ, Ŝ_z^{(3)}] to the two bonds incident to z | Quantum/SpinS/HeisenbergSpinSOp3Commutator.lean |
| spinSDot_commutator_onSiteS_spinSOp3 / _right | Cor 4.3 / IR bound (SingleBondSpinSOp3Commutator.lean, Tasaki §4.1, toward Corollary 4.3): the single-bond spin current [Ŝ_a·Ŝ_b, Ŝ_a^{(3)}] = i(Ŝ_a^{(1)} Ŝ_b^{(2)} − Ŝ_a^{(2)} Ŝ_b^{(1)}) for a ≠ b (only the transverse bond components fail to commute with Ŝ_a^{(3)}, via the cyclic SU(2) commutators; _right is the symmetric right-endpoint companion [Ŝ_a·Ŝ_b, Ŝ_b^{(3)}], and _eq_zero_of_ne is the off-bond vanishing [Ŝ_x·Ŝ_y, Ŝ_z^{(3)}] = 0 for z ∉ {x,y}); the building block of [Ĥ, Ŝ_z^{(3)}] and the double commutator in the infrared / f-sum-rule bound | Quantum/SpinS/SingleBondSpinSOp3Commutator.lean |
| expectation_abs_le_manyBodyOperatorNormS | Cor 4.3 / f-sum-rule (ExpectationNormBound.lean, Tasaki §4.1, toward Corollary 4.3): the general norm-to-expectation bound — for any M and a normalized state Φ (star Φ ⬝ᵥ Φ = 1), |⟨Φ, M Φ⟩.re| ≤ ‖M‖ (normalized-state form of abs_re_dotProduct_mulVec_le_norm_mul); converts operator-norm bounds into expectation bounds in the Falk–Bruch argument | Quantum/SpinS/ExpectationNormBound.lean |
| transverseBondEnergy_expectation_abs_le | Cor 4.3 / f-sum-rule (TransverseBondEnergyExpectation.lean, Tasaki §4.1, toward Corollary 4.3): in a normalized state Φ, the transverse bond energy expectation |⟨Φ, (Ŝ_a^{(1)}Ŝ_b^{(1)} + Ŝ_a^{(2)}Ŝ_b^{(2)}) Φ⟩.re| ≤ 2N² (the operator-norm bound + the norm→expectation bridge abs_re_dotProduct_mulVec_le_norm_mul + ‖Φ‖ = 1); summed over the O(L) adjacent bonds bounds the oscillator strength by O(L) | Quantum/SpinS/TransverseBondEnergyExpectation.lean |
| spinSDot_commutator_onSiteS_spinSOp3_norm_le | Cor 4.3 / f-sum-rule (SingleBondCommutatorNorm.lean, Tasaki §4.1, toward Corollary 4.3): the single-bond spin current [Ŝ_a·Ŝ_b, Ŝ_a^{(3)}] has operator norm ≤ 2N² (‖i‖ = 1 + per-site norm bounds + submultiplicativity); the O(1) bound per bond, summed over z’s two incident bonds, bounds ‖[Ĥ, Ŝ_z^{(3)}]‖ by O(1) | Quantum/SpinS/SingleBondCommutatorNorm.lean |
| transverseBondEnergy_manyBodyOperatorNormS_le | Cor 4.3 / f-sum-rule (TransverseBondEnergyNorm.lean, Tasaki §4.1, toward Corollary 4.3): the transverse bond energy (per-bond oscillator strength = −[Ŝ_a^{(3)},[Ŝ_a·Ŝ_b,Ŝ_a^{(3)}]]) has operator norm ‖Ŝ_a^{(1)}Ŝ_b^{(1)} + Ŝ_a^{(2)}Ŝ_b^{(2)}‖ ≤ 2N² (per-site norm bound ‖Ŝ^{(α)}‖ ≤ N + submultiplicativity); summed over the O(L) adjacent bonds this bounds the oscillator strength by O(L) | Quantum/SpinS/TransverseBondEnergyNorm.lean |
| pair_double_commutator_eq_zero_of_ne | Cor 4.3 / f-sum-rule (PairCommutatorVanish.lean, Tasaki §4.1, toward Corollary 4.3): off-pair vanishing [Ŝ_x^{(3)}, [Ĥ, Ŝ_z^{(3)}]] = 0 for x ∉ {z−1, z, z+1} — since [Ĥ, Ŝ_z^{(3)}] is supported on z’s two incident bonds, Ŝ_x^{(3)} commutes with it (Commute lemmas); hence the oscillator-strength double sum has only O(L) nonzero terms (three per z) | Quantum/SpinS/PairCommutatorVanish.lean |
| no_long_range_order_1d_of_susceptibility | Cor 4.3 / conditional reduction (NoLongRangeOrderConditional.lean, Tasaki §4.1, toward Corollary 4.3): the exact ε–δ statement of Corollary 4.3 modulo the susceptibility bound — if there is C ≥ 0 such that every normalized ground state of an even zero-field ring (L≥2, Even L) has a potential y for ÔΦ with Re⟨y,ÔΦ⟩ ≤ C·L, then for every ε > 0 there is L₀ beyond which every normalized ground state has \|⟨Φ,Ô²Φ⟩.re/L²\| < ε (assembling the O(L) oscillator bound + susceptibility reduction + ground-state bridge + an Archimedean ε–δ). This isolates the unconditional Cor 4.3 to the susceptibility bound Re⟨y,ÔΦ⟩ ≤ C·L; that bound is now supplied by the documented Shastry axiom shastry_staggered_susceptibility_bound, discharging no_long_range_order_1d into a theorem (PR #5003) | Quantum/SpinS/NoLongRangeOrderConditional.lean |
| groundState_mulVec_eq_hermitianMinEigenvalue | Cor 4.3 / ground-state bridge (HermitianGroundStateEigenvalue.lean, Tasaki §4.1, toward Corollary 4.3): a ground-state eigenvalue equals the minimum eigenvalue — for a Hermitian H and a normalized eigenvector Φ (HΦ = E₀•Φ) whose E₀ has minimal real part over all eigenpairs, HΦ = (hermitianMinEigenvalue H)•Φ (E₀.im = 0 by Hermiticity; E₀.re squeezed between the variational lower bound and the minimizing eigenvector); bridges the “energy-minimizing eigenpair” axiom hypothesis to the Falk–Bruch hermitianMinEigenvalue interface (PR #4847) | Quantum/SpinS/HermitianGroundStateEigenvalue.lean |
| staggeredOrder_sq_le_susceptibility | Cor 4.3 / Falk–Bruch (StaggeredOrderSusceptibility.lean, Tasaki §4.1, toward Corollary 4.3): the squared staggered order parameter is bounded by O(L) times the susceptibility — for a ground state Φ of the zero-field ring (eigenvalue hermitianMinEigenvalue) and a potential y for ÔΦ ((Ĥ−E₀)y = ÔΦ), 2(Re⟨Φ,Ô²Φ⟩)² ≤ 12N³·L·Re⟨y,ÔΦ⟩ (Falk–Bruch 2⟨Ô²⟩²≤osc·χ with the O(L) oscillator bound osc≤12N³L and χ=Re⟨y,ÔΦ⟩≥0 PSD); reduces Cor 4.3 to the susceptibility bound χ ≤ C·L (PR #4846) | Quantum/SpinS/StaggeredOrderSusceptibility.lean |
| oscillatorStrength_abs_le | Cor 4.3 / f-sum-rule (OscillatorStrengthBound.lean, Tasaki §4.1, toward Corollary 4.3): the f-sum-rule oscillator strength is O(L) — in a normalized state Φ, |⟨Φ, [Ô, [Ĥ, Ô]] Φ⟩.re| ≤ 12N³·L (assembling the double-sum form, the off-pair vanishing restricting to three nonzero z per x, the uniform per-pair norm ≤ 4N³, and the norm→expectation bridge); the O(L) numerator of the ground-state Falk–Bruch bound (PR #4845) | Quantum/SpinS/OscillatorStrengthBound.lean |
| pair_double_commutator_norm_le | Cor 4.3 / f-sum-rule (PairCommutatorNorm.lean, Tasaki §4.1, toward Corollary 4.3): each summand of the oscillator strength is bounded uniformly in L — ‖[Ŝ_x^{(3)}, [Ĥ, Ŝ_z^{(3)}]]‖ ≤ 4N³ (commutator norm ≤ 2‖Ŝ^{(3)}‖·‖[Ĥ, Ŝ_z^{(3)}]‖ with ‖Ŝ^{(3)}‖ ≤ N/2 and ‖[Ĥ, Ŝ_z^{(3)}]‖ ≤ 4N²); combined with off-pair vanishing gives O(L) | Quantum/SpinS/PairCommutatorNorm.lean |
| heisenbergHamiltonianS_ringCoupling_commutator_onSiteS_spinSOp3_norm_le | Cor 4.3 / f-sum-rule (RingHamiltonianCommutatorNorm.lean, Tasaki §4.1, toward Corollary 4.3): since [Ĥ, Ŝ_z^{(3)}] localizes to z’s two incident bonds, its operator norm is O(1) — ‖[Ĥ, Ŝ_z^{(3)}]‖ ≤ 4N² (sum of the two single-bond spin-current norms ≤ 2N² each); the length-independent locality making the oscillator strength O(L) | Quantum/SpinS/RingHamiltonianCommutatorNorm.lean |
| heisenbergHamiltonianS_ringCoupling_commutator_onSiteS_spinSOp3_closed | Cor 4.3 / f-sum-rule (RingHamiltonianCommutatorClosed.lean, Tasaki §4.1, toward Corollary 4.3): closed form of the spin-current divergence on a ring L ≥ 2 — [Ĥ, Ŝ_z^{(3)}] = [Ŝ_z·Ŝ_{z+1}, Ŝ_z^{(3)}] + [Ŝ_{z−1}·Ŝ_z, Ŝ_z^{(3)}] (the bond sum collapses to z’s two incident bonds via Finset.sum_pair, every other bond commuting); plus finRotate_ne_self | Quantum/SpinS/RingHamiltonianCommutatorClosed.lean |
| heisenbergHamiltonianS_ringCoupling_commutator_onSiteS_spinSOp3 | Cor 4.3 / f-sum-rule (RingHamiltonianCommutatorBondSum.lean, Tasaki §4.1, toward Corollary 4.3): the ring Hamiltonian commutator with Ŝ_z^{(3)} as a bond sum [Ĥ, Ŝ_z^{(3)}] = Σ_x [Ŝ_x·Ŝ_{x+1}, Ŝ_z^{(3)}] (bond-sum form + commutator distribution); since each bond commutator vanishes off z, this localizes the spin-current divergence to z’s two incident bonds | Quantum/SpinS/RingHamiltonianCommutatorBondSum.lean |
| heisenbergHamiltonianS_ringCoupling_eq_bondSum_general | Cor 4.3 / f-sum-rule (RingBondSumGeneral.lean, Tasaki §4.1, toward Corollary 4.3): the ring Heisenberg Hamiltonian on Fin L of any length as a bond sum Ĥ = Σ_x Ŝ_x·Ŝ_{finRotate L x} (directed coupling collapses the defining double sum); the form used to localize [Ĥ, Ŝ_z^{(3)}] to the two bonds incident to z | Quantum/SpinS/RingBondSumGeneral.lean |
| staggeredOrderOpS_double_commutator_dotProduct | Cor 4.3 / f-sum-rule (OscillatorStrengthForm.lean, Tasaki §4.1, toward Corollary 4.3): the oscillator strength as a double sum of two-site expectations ⟨Φ,[Ô,[Ĥ,Ô]]Φ⟩ = Σ_x Σ_z ε_x ε_z ⟨Φ,[Ŝ_x^{(3)},[Ĥ,Ŝ_z^{(3)}]]Φ⟩ (mulVec/dotProduct linearity over the operator double sum), whose summands vanish off adjacent sites — the O(L) oscillator strength | Quantum/SpinS/OscillatorStrengthForm.lean |
| staggeredOrderOpS_double_commutator | Cor 4.3 / f-sum-rule (StaggeredOrderDoubleCommutator.lean, Tasaki §4.1, toward Corollary 4.3): the f-sum-rule double commutator as a double site sum [Ô,[Ĥ,Ô]] = Σ_x Σ_z ε_x ε_z [Ŝ_x^{(3)},[Ĥ,Ŝ_z^{(3)}]] (order-operator commutator distribution applied twice; _commutator' reversed variant), whose summands vanish off adjacent sites so the apparent O(L²) collapses to O(L) | Quantum/SpinS/StaggeredOrderDoubleCommutator.lean |
| staggeredOrderOpS_commutator | Cor 4.3 / f-sum-rule (StaggeredOrderCommutator.lean, Tasaki §4.1, toward Corollary 4.3): the staggered order operator commutator distributes over sites [Ô, C] = Σ_x ε_x [Ŝ_x^{(3)}, C]; applied twice it expands the f-sum-rule double commutator [Ô,[Ĥ,Ô]] into a double site sum, whose terms vanish off adjacent sites (reducing the naive O(L²) count to O(L)) | Quantum/SpinS/StaggeredOrderCommutator.lean |
| staggeredOrderOpS_sq_dotProduct | Cor 4.3 bridge (StaggeredOrderSquareForm.lean, Tasaki §4.1, toward Corollary 4.3): the ground-state quadratic-form expansion ⟨Φ, Ô² Φ⟩ = Σ_x Σ_y ε_x ε_y ⟨Φ, Ŝ_x^{(3)} Ŝ_y^{(3)} Φ⟩, rewriting the order parameter in the exact form star Φ ⬝ᵥ (Ô²).mulVec Φ of the Corollary through the two-point functions the RP machinery bounds | Quantum/SpinS/StaggeredOrderSquareForm.lean |
| staggeredOrderOpS_sq_eq_sum | Cor 4.3 bridge (StaggeredOrderSquare.lean, Tasaki §4.1, toward Corollary 4.3): the staggered order operator squared expands as the two-point double sum Ô² = Σ_x Σ_y ε_x ε_y Ŝ_x^{(3)} Ŝ_y^{(3)} — the bridge from the order parameter to the two-point functions bounded by the reflection-positivity / infrared machinery (the squared order parameter per L² is controlled by the total two-point sum, only O(L) in one dimension) | Quantum/SpinS/StaggeredOrderSquare.lean |
| rpTraceWeight_cauchySchwarz_abs | RP infra layer 40 (RingReflectionCauchySchwarzSqrt.lean, Tasaki §4.1, toward Theorem 4.2): the square-root (usable) form of the RP Cauchy–Schwarz — |Re Tr(M·θA·B)| ≤ √(Re Tr(M·θA·A))·√(Re Tr(M·θB·B)) for a reflection-invariant RP trace weight M and left-supported A,B, by taking roots in the chessboard inequality (diagonals nonnegative); the form iterated in the DLS spreading argument | Quantum/SpinS/RingReflectionCauchySchwarzSqrt.lean |
| ringTranslateConj / chessboard_ringTranslateConj_of | RP infra layer 39 (RingReflectionChessboardTransport.lean, Tasaki §4.1, toward Theorem 4.2): conjugation by the ring translation τ(X) = T†·X·T is a trace-preserving *-homomorphism (ringTranslateConj_mul/_trace), so any chessboard estimate transports unchanged to the translation-conjugated data (τM, τ(θA), τB) (chessboard_ringTranslateConj_of) — the weight τM is the Marshall gauge relative to the shifted reflection plane; carries the single-axis chessboard to every bond toward Gaussian domination | Quantum/SpinS/RingReflectionChessboardTransport.lean |
| chainTranslation_conj_gibbs / thermalAverageReS_chainTranslation | RP infra layer 38 (RingTranslationGibbs.lean, Tasaki §4.1, toward Theorem 4.2): unlike the half-system gauge, the physical ring Heisenberg Hamiltonian is translation invariant (chainTranslation_conj_heisenbergHamiltonianS), so the physical Gibbs operator exp(−β·Ĥ) is translation invariant (chainTranslation_conj_gibbs) and every physical thermal average is translation covariant ⟨T†AT⟩ = ⟨A⟩ (thermalAverageReS_chainTranslation); the thermal-state translation symmetry for the momentum-space infrared analysis | Quantum/SpinS/RingTranslationGibbs.lean |
| chainTranslation_conj_ringReflectionThetaS_onSiteS / _spinSDot | RP infra layer 37 (RingReflectionTranslation.lean, Tasaki §4.1, toward Theorem 4.2): translation covariance of the fixed-axis reflection map θ — conjugating θ(onSiteS x A) (resp. θ(Ŝ_x·Ŝ_y)) by the ring translation chainTranslationOp shifts the reflection axis, sending the sites to finRotate (ringReflect x) (resp. both endpoints); the foundation for reflections across every bond, needed to spread the single-axis chessboard toward DLS Gaussian domination | Quantum/SpinS/RingReflectionTranslation.lean |
| ringDLSGibbs_reflection_step | RP infra layer 36 (RingReflectionGibbsChessboard.lean, Tasaki §4.1, toward Theorem 4.2): the concrete chessboard inequality for the gauged ring Gibbs weight — combining its reflection positivity (Gibbs capstone) and reflection invariance (θM=M), for β ≥ 0 and left-supported A,B, (Re Tr(M·θA·B))² ≤ Re Tr(M·θA·A)·Re Tr(M·θB·B) with M = exp(−β·toHamiltonian); the DLS factorization estimate for the thermal state of the physical ring antiferromagnet | Quantum/SpinS/RingReflectionGibbsChessboard.lean |
| ringReflectionThetaS_toHamiltonian / _ringDLSGibbs | RP infra layer 35 (RingReflectionThetaInvariance.lean, Tasaki §4.1, toward Theorem 4.2): the gauged DLS Hamiltonian is reflection-invariant θ(toHamiltonian) = toHamiltonian (the H_L + θ(H_L) part is swapped to itself; each crossing bond θ(crossBondInteractionS x) = crossBondInteractionS x since Ŝ_x^α commutes with its right-half reflection θ(Ŝ_x^α)), hence the gauged ring Gibbs weight exp(−β·toHamiltonian) is reflection-invariant — supplying the θM = M hypothesis for the chessboard/real-diagonal lemmas | Quantum/SpinS/RingReflectionThetaInvariance.lean |
| rpForm_re_symm / rpTraceWeight_reflection_step | RP infra layer 34 (RingReflectionChessboard.lean, Tasaki §4.1, toward Theorem 4.2): for a reflection-invariant RP trace weight M (θM=M) and left-supported A,B, the off-diagonal form value is symmetric Re Tr(M·θA·B) = Re Tr(M·θB·A) (since A commutes with the right-half θB); feeding this into the Cauchy–Schwarz discriminant collapses the cross term, giving the chessboard bound (Re Tr(M·θA·B))² ≤ Re Tr(M·θA·A)·Re Tr(M·θB·B) — the DLS factorization step underlying Gaussian domination | Quantum/SpinS/RingReflectionChessboard.lean |
| ringReflectionThetaS_trace / rpForm_diag_im_zero | RP infra layer 33 (RingReflectionTraceReality.lean, Tasaki §4.1, toward Theorem 4.2): the reflection map conjugates the trace Tr(θX) = conj(Tr X) (reindex the diagonal by the involutive site reflection), so for a reflection-invariant weight M (θM = M) and left-supported A the RP-form diagonal Tr(M·θA·A) is real (θ²=id, *-homomorphism, A commutes with θA); together with the Cauchy–Schwarz this makes (A,B)↦Tr(M·θA·B) a genuine positive-semidefinite form with real diagonal | Quantum/SpinS/RingReflectionTraceReality.lean |
| rpTraceWeight_cauchySchwarz | RP infra layer 32 (RingReflectionCauchySchwarz.lean, Tasaki §4.1, toward Theorem 4.2): a reflection-positive trace weight M makes (A,B) ↦ Tr(M·θA·B) a positive-semidefinite sesquilinear form on the left subalgebra; expanding 0 ≤ Re Tr(M·θ(A−tB)·(A−tB)) as a nonnegative real quadratic in t and taking its discriminant (discrim_le_zero) gives (Re Tr(M·θA·B) + Re Tr(M·θB·A))² ≤ 4·Re Tr(M·θA·A)·Re Tr(M·θB·B) — the workhorse for the DLS infrared bound | Quantum/SpinS/RingReflectionCauchySchwarz.lean |
| thermalAverageReS_toHamiltonian_eq | RP infra layer 31 (RingReflectionThermalTransfer.lean, Tasaki §4.1, toward Theorem 4.2): the right-half gauge is a similarity transform, so it leaves the partition function invariant (thermalPartitionFnS_toHamiltonian_eq) and transports thermal averages — the physical ring Heisenberg canonical average of A equals the reflection-positive DLS canonical average of rightGauge · A · rightGaugeInv; the bridge carrying RP bounds back to the physical ring antiferromagnet | Quantum/SpinS/RingReflectionThermalTransfer.lean |
| exp_neg_smul_toHamiltonian_eq | RP infra layer 30 (RingReflectionGibbsGauge.lean, Tasaki §4.1, toward Theorem 4.2): conjugation by the right-half gauge commutes with the matrix exponential (Matrix.exp_units_conj), so the physical ring Heisenberg Gibbs operator exp(−β Ĥ) and the reflection-positive DLS Gibbs operator exp(−β · ringDLSDecomposition.toHamiltonian) are unitarily equivalent — physical thermal averages become DLS thermal averages of gauge-transformed observables | Quantum/SpinS/RingReflectionGibbsGauge.lean |
| rightGauge_conj_ringHamiltonian | RP infra layer 29 (RingReflectionGaugeAssembly.lean, Tasaki §4.1, toward Theorem 4.2): the right-half DLS/Marshall gauge conjugates the ring Heisenberg Hamiltonian into the reflection-positive DLS Hamiltonian — rightGauge · heisenbergHamiltonianS (ringCoupling (2n)) · rightGaugeInv = ringDLSDecomposition.toHamiltonian (bond Hamiltonians fixed, the two crossing bonds become the negated gauged crossing interactions); the unitary equivalence bridging the physical ring antiferromagnet to its reflection-positive form | Quantum/SpinS/RingReflectionGaugeAssembly.lean |
| rightGauge_conj_ringLeftHamiltonian / rightGauge_conj_theta_ringLeftHamiltonian | RP infra layer 28 (RingReflectionNonCrossConj.lean, Tasaki §4.1, toward Theorem 4.2): summing the bond-invariance lemmas, the right-half gauge fixes both the left bond Hamiltonian (rightGauge_conj_ringLeftHamiltonian) and the reflected right bond Hamiltonian θ(ringLeftHamiltonian) (rightGauge_conj_theta_ringLeftHamiltonian) — only the two crossing bonds are affected | Quantum/SpinS/RingReflectionNonCrossConj.lean |
| rightGauge_conj_crossBond | RP infra layer 27 (RingReflectionCrossConj.lean, Tasaki §4.1, toward Theorem 4.2): the gauge image of a crossing bond is the negated gauged crossing interaction. For a left site x < n (reflection r x a right site), rightGauge · (Ŝ_x · Ŝ_{r x}) · rightGaugeInv = −crossBondInteractionS x — the left endpoint untouched, the right endpoint gauged (flipping Ŝ^1/Ŝ^3 signs), matching crossBondInteractionS_eq. Both ring crossing bonds (n−1,n) and (2n−1,0) are of this form | Quantum/SpinS/RingReflectionCrossConj.lean |
| rightGauge_conj_spinSDot_left/_right | RP infra layer 26 (RingReflectionBondConj.lean, Tasaki §4.1, toward Theorem 4.2): the right-half gauge fixes every non-crossing bond. rightGauge_conj_spinSDot_left (left bond, both sites < n: untouched) and rightGauge_conj_spinSDot_right (right bond, both sites gauged: the Ŝ^1/Ŝ^3 sign flips cancel in the product, Ŝ^2 unchanged). Only the two crossing bonds acquire the DLS sign flip. Helpers rightGauge_conj_onSiteS_left/_right | Quantum/SpinS/RingReflectionBondConj.lean |
| rightGauge_conj_mul (gauge homomorphism) | RP infra layer 25 (RingReflectionGaugeConj.lean, Tasaki §4.1, toward Theorem 4.2): conjugation X ↦ rightGauge·X·rightGaugeInv by the right-half DLS/Marshall gauge is an algebra homomorphism — rightGauge_conj_mul (over products, via rightGaugeInv_mul_rightGauge), rightGauge_conj_add, rightGauge_conj_smul, rightGauge_conj_sum. With rightGauge_conj_onSiteS these compute the gauge image of any operator built from single-site operators (the ring Hamiltonian in particular) | Quantum/SpinS/RingReflectionGaugeConj.lean |
| AxisTwoPiRotS / rightGauge_conj_onSiteS | RP infra layer 24 (RingReflectionGauge.lean, Tasaki §4.1, toward Theorem 4.2): the right-half DLS/Marshall gauge. manyBodyTensorS_conj_onSiteS_dep — site-dependent tensor conjugation (⊗_i W_i)(onSiteS z A)(⊗_i Winv_i) = onSiteS z (W_z·A·Winv_z) (for W_i·Winv_i = 1). AxisTwoPiRotS — the single-site π-rotation around axis 2 as an interface (following AxisSwapUnitaryS; fields U Ŝ^1 U⁻¹ = −Ŝ^1, U Ŝ^2 U⁻¹ = Ŝ^2, U Ŝ^3 U⁻¹ = −Ŝ^3, non-vacuous at spin-1/2). rightGauge/rightGaugeInv — the gauge unitary applying U on the right sites only; rightGaugeInv_mul_rightGauge (invertible) and rightGauge_conj_onSiteS (conjugation acts as U·A·U⁻¹ on right sites, trivially on left). The interface is made non-vacuous at spin-1/2 by axisTwoPiRotSpinHalf (the explicit spinHalfRot2 π). The gauge bridging the ungauged ring Hamiltonian to its reflection-positive form | Quantum/SpinS/RingReflectionGauge.lean |
| heisenbergHamiltonianS_ringCoupling_ungauged_dls | RP infra layer 23 (RingReflectionUngaugedDLS.lean, Tasaki §4.1, toward Theorem 4.2): the ungauged DLS split of the ring Heisenberg Hamiltonian. Combining the bond split (#4798) with ringRightBondSum = θ(ringLeftHamiltonian) (#4799): heisenbergHamiltonianS (ringCoupling (2n)) = ringLeftHamiltonian + θ(ringLeftHamiltonian) + (Ŝ_{n−1}·Ŝ_n + Ŝ_{2n−1}·Ŝ_0). The crossing term is the ungauged AFM crossing bond, differing from the gauged crossBondInteractionS (with Ŝ² sign flipped) by the DLS/Marshall gauge; bridging the two via the gauge unitary is the next step | Quantum/SpinS/RingReflectionUngaugedDLS.lean |
| ringRightBondSum_eq_theta | RP infra layer 22 (RingReflectionRightEqTheta.lean, Tasaki §4.1, toward Theorem 4.2): the right bond Hamiltonian equals the reflection of the left bond Hamiltonian. Reindexing by the bijection x ↦ r(x+1) (reflection of the cyclic successor ringBondSucc, shown bijective = ·+1 via Equiv.addRight) and using spinSDot symmetry, ringRightBondSum = θ(ringLeftHamiltonian) (Fintype.sum_bijective). This identifies the right part of the bond split with the θ(H_L) term of the DLS decomposition; combined with the bond split (#4798), heisenbergHamiltonianS (ringCoupling (2n)) = ringLeftHamiltonian + θ(ringLeftHamiltonian) + (ungauged crossing bonds) | Quantum/SpinS/RingReflectionRightEqTheta.lean |
| heisenbergHamiltonianS_ringCoupling_bond_split | RP infra layer 21 (RingReflectionBondSplit.lean, Tasaki §4.1, toward Theorem 4.2): the ring Heisenberg Hamiltonian split into left, right, and crossing bonds. The bonds (x, x+1) of Fin (2n) fall into four disjoint classes by x.val (left x ≤ n−2, crossing x = n−1, right n ≤ x ≤ 2n−2, crossing x = 2n−1); summing the bond form over this partition (bondTerm_four_way per-bond decomposition + Finset.sum_add_distrib + sum_ite_val_eq) gives heisenbergHamiltonianS (ringCoupling (2n)) = ringLeftHamiltonian + ringRightBondSum + Ŝ_{n−1}·Ŝ_n + Ŝ_{2n−1}·Ŝ_0. Identifying ringRightBondSum with θ(ringLeftHamiltonian) and the crossing bonds with the gauged interaction is the next step | Quantum/SpinS/RingReflectionBondSplit.lean |
| ringDLSDecomposition_gibbs_rpTraceWeight | RP infra layer 20 (RingReflectionConcreteGibbs.lean, Tasaki §4.1, toward Theorem 4.2): the concrete gauged ring antiferromagnet has a reflection-positive Gibbs weight. Instantiating the ring DLS decomposition with the concrete left part H_L = ringLeftHamiltonian (ringDLSDecomposition), ringDLSDecomposition_toHamiltonian gives the gauged ring Hamiltonian H = ringLeftHamiltonian + θ(ringLeftHamiltonian) − (crossBondInteractionS 0 + crossBondInteractionS (n−1)), and ringDLSDecomposition_gibbs_rpTraceWeight concludes (via the Gibbs capstone) that exp(−β·H) is a reflection-positive trace weight (β ≥ 0). Identification of H with the physical ungauged Hamiltonian (bond-split assembly + gauge unitary) is the next step | Quantum/SpinS/RingReflectionConcreteGibbs.lean |
| ringBondSquareFieldHamiltonian / ringBondSquareLinField / ringBondSquareConst / ringBondSquareFieldHamiltonian_eq / ringBondSquareFieldHamiltonian_isHermitian | Bond-square field Hamiltonian foundation (RingReflectionBondSquareField.lean, Tasaki §4.1 (4.1.48), book p.86, bond-square field Hamiltonian / PR #4987): the faithful quadratic bond-square field Hamiltonian and its reduction to the linear-core form. Tasaki’s field Hamiltonian couples the staggered field f_x = (−1)ˣ h_x quadratically inside the bond-square ½{Ŝ³ₓ + Ŝ³_y − f_x − f_y}²; this square form is the faithful object. The equivalent linear-core form ringFieldHamiltonian n N (ringBondSquareLinField n h) + (ringBondSquareConst n h : ℂ) • 1 is a proved identity (★) ringBondSquareFieldHamiltonian_eq, obtained by expanding the square, completing the isotropic dot product with the Ŝ³ₓŜ³_y cross term, cancelling the single-ion terms via successor reindexing, and regrouping into linear and scalar parts. The staggered-field per-site coefficient ringBondSquareLinField n h z = −(f_z + f_{z+1}) − (f_{z−1} + f_z) (the two incident ring-bond field sums, Tasaki b̃-field (4.1.38), book p.84). The scalar constant ringBondSquareConst n h = ½ Σ_bonds (f_x + f_{x+1})² is nonnegative (deferred; C(h)≥0 is consumed in later PR-BS3+ where the collapse inequality and uniform-field bound are applied) and repairs the reflection-bound inequality direction. The bond-square Hamiltonian is Hermitian (ringBondSquareFieldHamiltonian_isHermitian) as the sum of the Hermitian linear-core part and the real scalar constant. This is PR-BS1 (bond-square route) toward the reflection-positivity infrastructure for Theorem 4.2. | Quantum/SpinS/RingReflectionBondSquareField.lean |
| ringBondSquareFieldPartitionRe / ringBondSquareFieldPartitionRe_eq_scaled | Bond-square field partition function and scaled reduction (RingReflectionBondSquareFieldPartition.lean, Tasaki §4.1 (4.1.49), book p.86, bond-square partition function / PR #4988): the canonical partition function Z^{BS}_β(h) = Re Tr exp(−β·Ĥ_h) of the bond-square field Hamiltonian ringBondSquareFieldHamiltonian (Tasaki (4.1.48), book p.86). The crux is the scalar-shift reduction (★★) ringBondSquareFieldPartitionRe_eq_scaled: since the reduction identity (★) (ringBondSquareFieldHamiltonian_eq, PR-BS1) decomposes Ĥ_h = Ĥ(kOf h) + C(h)·1 where C(h)·1 is a real scalar central element commuting with Ĥ(kOf h), the matrix exponential splits: exp(−β·Ĥ_h) = exp(−β·Ĥ(kOf h)) · exp(−βC(h)·1), and the scalar exponential exp(−βC(h)·1) evaluates to e^{−βC(h)}·1 (via Matrix.exp_diagonal). The real scalar e^{−βC(h)} pulls out of both the trace (Matrix.trace_smul) and the real part (Complex.re_ofReal_mul), yielding Z^{BS}_β(h) = e^{−βC(h)} · Z^{repo}_β(kOf h) (Tasaki §4.1 (4.1.49), book p.86), the finite-β form of the uniform-field bound. This equation lets later PR-BS3+ reuse the single-field symmetries of ringFieldPartitionRe for the bond-square partition function without redefining Z on a field map. This is PR-BS2 of the bond-square route toward the reflection-positivity infrastructure for Theorem 4.2. | Quantum/SpinS/RingReflectionBondSquareFieldPartition.lean |
| ringBondSquareConst_const / ringBondSquareLinField_const / ringBondSquareFieldHamiltonian_const / ringBondSquareFieldPartitionRe_const | Constant-field collapse (RingReflectionBondSquareField.lean / RingReflectionBondSquareFieldPartition.lean, Tasaki §4.1 footnote 10 (4.1.49), book pp. 84–86, constant-field collapse / PR #4989): at a constant field h_x ≡ c, the staggered field on any ring bond sums to zero f_x + f_{x+1} = (−1)^x c + (−1)^{x+1} c = 0 via the even-ring staggered sign relation (−1)^{x+1} = −(−1)^x (private lemma: neg_one_pow_ringBondSucc); consequently both the bond-square constant C(h^const) = 0 (ringBondSquareConst_const) and the bond-square linear field kOf(h^const) = 0 (ringBondSquareLinField_const) vanish (each per-site coefficient is the sum of two incident bond cancellations, proven via private ringBondSquareStagField_const_bond_cancel). The operator collapse Ĥ(h^const) = ringFieldHamiltonian n N 0 (ringBondSquareFieldHamiltonian_const) follows from the reduction identity (★) and the two vanishings: the bond-square Hamiltonian at a constant field collapses to the field-free linear-core form Ĥ₀ (Tasaki §4.1 (4.1.49), book p.86, finite-N form of E_GS(h^const) = E_GS(0,…,0)). The partition-function collapse Z^{BS}_β(h^const) = Z^{repo}_β(0) (ringBondSquareFieldPartitionRe_const) is immediate from the operator collapse: both partition functions are the real part of the Gibbs trace of the same Hamiltonian ringFieldHamiltonian n N 0, and the scalar exponential e^{−βC(h^const)} = e^0 = 1 vanishes from the (★★) reduction (finite-β form of E_GS(h^const) = E_GS(0,…,0), consumed by the uniform-field Gaussian-domination bound PR-BS10+). This is PR-BS3 of the bond-square route toward the reflection-positivity infrastructure for Theorem 4.2. | Quantum/SpinS/RingReflectionBondSquareField.lean, Quantum/SpinS/RingReflectionBondSquareFieldPartition.lean |
| ringBondSquareLeftFieldHamiltonian / ringBondSquareLeftFieldHamiltonian_supportedOnLeft / ringBondSquareCrossingGen / ringBondSquareCrossingGen_supportedOnLeft / ringBondSquareFieldCrossing / ringBondSquareFieldCrossing_twoFieldConeRep / ringBondSquareTwoFieldWeight / ringBondSquareTwoFieldWeight_self / ringBondSquareTwoFieldWeight_isLimit | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/RingReflectionBondSquareTwoFieldWeight.lean |
| ringBondSquareTwoFieldWeight_reflection_cauchySchwarz | Bond-square reflection Cauchy–Schwarz capstone (RingReflectionTwoFieldCauchySchwarz.lean, Tasaki §4.1 (4.1.51), book p. 86, bond-square finite-β reflection Cauchy–Schwarz / PR #4993): the bond-square variant of Tasaki’s reflection Cauchy–Schwarz inequality — (Re Tr W^{BS}(a,b))² ≤ Re Tr W^{BS}(a,a) · Re Tr W^{BS}(b,b) where W^{BS}(a,b) = ringBondSquareTwoFieldWeight n N β a b. The proof proceeds via a nested double limit (DLS Trotter), with the finite (m,r) Cauchy–Schwarz upgraded by the inner limit r → ∞ (exponential cone closure) and outer limit m → ∞ (Trotter convergence); both limits preserve the inequality via cauchySchwarz_of_tendsto. The bond-square crossing is genuinely field-dependent (via the crossing generators instantiating RPTwoFieldConeRepS), so the (b,b) slot in the Trotter representation directly carries the correct field-dependent crossing from the isLimit statement — no field-free-crossing rewrite or new sign lemma is required. The 0 ≤ β hypothesis ensures cone positivity of (β/m)D where D is the bond-square crossing interaction. This capstone completes the bond-square reflection Cauchy–Schwarz layer toward Theorem 4.2 (the bond-square Gaussian-domination sub-arc). | Quantum/SpinS/RingReflectionTwoFieldCauchySchwarz.lean |
| ringBondSquareBondTermOf / ringBondSquareLeftBondSum / ringBondSquareRightBondSum / ringBondSquareFieldHamiltonian_eq_bondTermOf_sum / ringBondSquareFieldHamiltonian_ungauged_dls / ringBondSquareLeftBondSum_eq_leftCouplingBulk | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/RingReflectionBondSquareUngaugedDLS.lean |
| physBondSquareFieldOf / ringBondSquareStagField_physBondSquareFieldOf / rightGauge_conj_ringBondSquareFieldHamiltonian / rightGauge_conj_sub / rightGauge_conj_ringBondSquareBondTermOf_left / rightGauge_conj_ringBondSquareLeftBondSum / rightGauge_conj_ringBondSquareSingleIon / rightGauge_conj_ringBondSquareRightBondSum | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/RingReflectionBondSquareGaugeCrux.lean |
| ringBondSquareFieldPartitionRe_physFieldOf / physBondSquareFieldOf_self / ringBondSquareFieldPartitionRe_reflection_step | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/RingReflectionBondSquarePhysId.lean |
| ringBondSquareConst_reindexCyclic / ringBondSquareLinField_reindexCyclic / ringBondSquareFieldPartitionRe_pos / ringBondSquareFieldPartitionRe_reindexCyclic / ringBondSquareFieldPartition_gaussianDomination | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/RingReflectionBondSquareGaussianDomination.lean |
| ringBondSquareFieldPartitionRe_uniform_bound | Bond-square uniform-field capstone (RingReflectionBondSquareUniformBound.lean, Tasaki §4.1 Theorem 4.2 (4.1.49)/(4.1.52), book pp. 85–86, bond-square uniform-field bound / PR #4999): the terminal capstone of the bond-square reflection-positivity route: the bound Z^{BS}_β(h) ≤ Z^{BS}_β(0) (Tasaki §4.1 Theorem 4.2, uniform-field bound (4.1.49)/(4.1.52), pp. 85–86). Pure algebraic glue atop the chessboard Gaussian-domination capstone (PR-BS9, ringBondSquareFieldPartition_gaussianDomination) and the constant-field collapse (PR-BS3, ringBondSquareFieldPartitionRe_const). The chessboard bound gives Z^{BS}_β(h)^{2n} ≤ ∏_j Z^{BS}_β(fun _ => h j); each constant-field factor collapses exactly (without e^{−βC} ≤ 1 estimate — the constant field cancels at the operator level via ringBondSquareFieldHamiltonian_const, PR-BS3) to Z^{repo}_β(0) = Z^{BS}_β(0), so the product is Z^{BS}_β(0)^{2n}. The 2n-th root monotonicity le_of_pow_le_pow_left₀ (with strict positivity from ringBondSquareFieldPartitionRe_pos, PR-BS9) then yields the bound. This completes the bond-square route toward Theorem 4.2 (Tasaki pp. 85–90; DLS 1978; FILS). | Quantum/SpinS/RingReflectionBondSquareUniformBound.lean |
| trace_exp_smul_neg_re_eq_sum_exp / tendsto_neg_inv_mul_log_trace_exp_re_atTop_hermitianMinEigenvalue | (SUM) & (χ1-a) — Free-energy T → 0 limit: eigenvalue-sum spectral form and ground-energy limit (FreeEnergyGroundEnergyLimit.lean, Tasaki §4.1 (4.1.40)/(4.1.49), book pp. 85–86, free-energy T→0 limit / PR #5000): the real-analysis engine for the susceptibility phase. Two lemmas: (SUM) trace_exp_smul_neg_re_eq_sum_exp — for a Hermitian matrix H, the real part of the Gibbs trace Re Tr e^{−βH} = ∑_i e^{−β λ_i} (spectral theorem: the scalar −β folds into the eigenvalue diagonal, exponentiates entrywise, and the trace drops unitary conjugation). (χ1-a) tendsto_neg_inv_mul_log_trace_exp_re_atTop_hermitianMinEigenvalue — for a Hermitian H, −(1/β) log (Re Tr e^{−βH}) → hermitianMinEigenvalue H as β → ∞ (the ground-state energy is the zero-temperature limit of the free energy), via the two-sided Boltzmann squeeze e^{−βE} ≤ Z(β) ≤ card·e^{−βE} (with degeneracy subleading: (log card)/β → 0). The dual limit tendsto_neg_inv_mul_log_trace_exp_re_atTop_hermitianMinEigenvalue is applied in PR-χ1 to both Ĥ(h) and Ĥ(0) to yield the ground-state inequality E_GS(0) ≤ E_GS(h) from the finite-β partition bound Z^{BS}_β(h) ≤ Z^{BS}_β(0) by limit-preservation. This is PR-χ1 (free-energy layer) toward the susceptibility phase. | Quantum/SpinS/FreeEnergyGroundEnergyLimit.lean |
| ringBondSquareFieldHamiltonian_hermitianMinEigenvalue_ge_field_zero | (χ1-b) — Ground-state energy uniform-field bound E_GS(h) ≥ E_GS(0) (RingReflectionBondSquareGroundEnergy.lean, Tasaki §4.1 (4.1.40)/(4.1.49), book pp. 85–86, ground-state energy bound / PR #5000): TEMPORARY capstone of the χ1 (susceptibility free-energy) opening: the ground-state energy of the bond-square field Hamiltonian at field h is at least that at zero field, E_GS(0) ≤ E_GS(h), on the even ring Fin (2n) (n ≥ 1). The T → 0 limit of the finite-β partition bound Z^{BS}_β(h) ≤ Z^{BS}_β(0) (PR-BS10): both partition functions are strictly positive (BS9), so Real.log is monotone; multiplying the log inequality by −(1/β) < 0 reverses it into the free-energy inequality −(1/β) log Z^{BS}_β(0) ≤ −(1/β) log Z^{BS}_β(h) for every β > 0; applying (χ1-a) to both sides yields the ground-state inequality in the limit β → ∞ via le_of_tendsto_of_tendsto. This bound is the entry point for the next PR-χ2 (susceptibility sum rule) and the long-range order theorems that follow. This is PR-χ1b of the susceptibility phase toward Theorem 4.2. | Quantum/SpinS/RingReflectionBondSquareGroundEnergy.lean |
| hermitian_posSemidef_exists_orthogonal_potential | (χ2a-i) — Pseudoinverse existence for Hermitian matrices (HermitianPseudoinverse.lean, generic finite-dimensional linear algebra, Tasaki §4.1 eq. (4.1.39), book p. 84, susceptibility sum rule infrastructure / PR #5001): for a positive-semidefinite (hence Hermitian) matrix A, if v ⊥ ker A, then ∃y: A y = v ∧ y ⊥ ker A (the Moore–Penrose pseudoinverse image). Since range A = (ker A)ᗮ for self-adjoint A (proof: LinearMap.orthogonal_ker + adjoint identity), v lies in the range; projecting any preimage onto (ker A)ᗮ yields y orthogonal to the kernel while preserving the image. Load-bearing for the resolvent identity and susceptibility finite-order perturbation (Tasaki (4.1.39)/(4.1.41), pp. 84–86). | Math/MatrixAnalysis/HermitianPseudoinverse.lean |
| exists_smul_of_mem_finrank_le_one | (χ2a-ii) — Scalar-multiple extraction from one-dimensional eigenspace (UniqueEigenspaceInvolution.lean, generic finite-dimensional linear algebra shared with Theorem 2.4, issue #4777, PR #5001): if a submodule E has finrank ≤ 1, and Φ ≠ 0 and w both lie in E, then ∃c: w = c • Φ (any element is a scalar multiple of any non-zero member). This is the uniqueness engine used by the involution eigenvalue lemma below. | Math/MatrixAnalysis/UniqueEigenspaceInvolution.lean |
| exists_involution_eigenvalue_of_unique_eigenspace | (χ2a-iii) — Involution eigenvalue on unique ground state (UniqueEigenspaceInvolution.lean, Tasaki §2.5 Theorem 2.4 (p. 43–44) and §4.1 Theorem 4.2 (pp. 84–86), shared proof infrastructure, issue #4777, PR #5001): if a Hermitian matrix H has a μ-eigenspace of finrank ≤ 1 (unique ground state), Φ is a non-zero μ-eigenvector, and Θ commutes with H and is an involution (Θ² = 1), then ∃δ: Θ Φ = δ • Φ ∧ δ² = 1 (Θ acts as ±1 on the unique eigenstate). The mechanism: Θ Φ lies in the eigenspace (commutation), so equals δ • Φ (uniqueness via exists_smul_of_mem_finrank_le_one), and Θ² Φ = Φ forces δ² = 1. Used in both Theorem 2.4 (no-magnetization) and χ2a (first-order vanishing). | Math/MatrixAnalysis/UniqueEigenspaceInvolution.lean |
| dotProduct_mulVec_eq_zero_of_conj_anti | (χ2a-iv) — Vanishing under symmetric anti-involution (AndersonTowerTanakaMoments.lean, generalized to issue #4777, PR #5001): shared lemma for Theorem 4.9 transverse-moment vanishing (§4.2.2) and χ2a first-order vanishing (§4.1 Theorem 4.2). If Θᴴ = Θ (real symmetric), Θ Ξ = δ • Ξ with δ · δ̄ = 1 (unit modulus), and Θ O Θ = −O (anti-invariance), then ⟨Ξ| O |Ξ⟩ = 0. Proof: conjugating by Θ yields ⟨Ξ| (Θ O Θ) |Ξ⟩ = (δ δ̄) · ⟨Ξ| O |Ξ⟩ = ⟨Ξ| O |Ξ⟩ (by unit-modulus identity), but also = −⟨Ξ| O |Ξ⟩ (by anti-invariance), so vanishing. At δ = ±1 (unique eigenspace case), this is the crux of first-order vanishing in the susceptibility perturbation (Tasaki (4.1.39), p. 84). Made public; signature generalized from δ = 1 to δ * star δ = 1. | Quantum/SpinS/AndersonTowerTanakaMoments.lean |
| ringBondSquareLinFieldOp_groundState_expectation_zero | (χ2a-v) — First-order susceptibility vanishing (RingReflectionBondSquareSusceptibility.lean, Tasaki §4.1 eq. (4.1.39), book p. 84, susceptibility sum rule / PR #5001): the Zeeman perturbation V = Σ_z (kOf h)_z · Ŝ³_z (the 1st-order term in the susceptibility expansion ringBondSquareFieldHamiltonian_eq, reduction (★)) vanishes in expectation on any unique ground state Φ of the field-free ring Hamiltonian H₀ = ringFieldHamiltonian n N 0. The axis-1 spin reversal Θ = manyBodyReversalS is a real symmetric involution commuting with H₀ and reversing each Ŝ³_z (Θ Ŝ³_z Θ = −Ŝ³_z), hence reversing V (Θ V Θ = −V). On the unique ground state, Θ Φ = δ Φ with δ = ±1 (via exists_involution_eigenvalue_of_unique_eigenspace), so ⟨Φ|V|Φ⟩ = 0 (via dotProduct_mulVec_eq_zero_of_conj_anti). This ensures the second-order perturbation formula (4.1.41) has no first-order correction, enabling the sum-rule capstone χ2b to close the susceptibility. | Quantum/SpinS/RingReflectionBondSquareSusceptibility.lean |
| ringBondSquareStagField_smul | (χ2b-0) — Staggered-field scaling (RingReflectionBondSquareSusceptibilitySumRule.lean, Tasaki §4.1 (4.1.37)–(4.1.38), book p. 84, susceptibility sum rule / PR #5002): foundational scaling lemma — the staggered field f_x(h) = (−1)ˣ h_x is linear in the input field h, so f_x(λh) = λ·f_x(h). This base linearity of the staggered field underpins the higher-order field-scaling lemmas (χ2b-i/ii/iii) which derive quadratic and composite scalings by composition. | Quantum/SpinS/RingReflectionBondSquareSusceptibilitySumRule.lean |
| ringBondSquareLinField_smul / ringBondSquareConst_smul / ringFieldHamiltonian_smul_field | (χ2b-i/ii/iii) — Field scaling laws (RingReflectionBondSquareSusceptibilitySumRule.lean, Tasaki §4.1 (4.1.37)–(4.1.38), book p. 84, susceptibility sum rule / PR #5002): three linear-scaling lemmas for the variational expansion of the susceptibility sum rule. (i) Linear-field scaling ringBondSquareLinField_smul: kOf(λh) = λ·kOf(h) (each per-site linear field coefficient scales by λ). (ii) Quadratic-constant scaling ringBondSquareConst_smul: C(λh) = λ²·C(h), where C(h) = ½Σ(f_x+f_{x+1})² is a sum of squared bond sums (f the staggered field); quadratic scaling ensures the λ-polynomial in the variational bound is exactly quadratic. (iii) Field-Hamiltonian scaling ringFieldHamiltonian_smul_field: Ĥ_field(λk) = H₀ + λ·(Σ_z k_z·Ŝ³_z) — the Zeeman sum is linear in the field-coefficient vector k, with the field-free part H₀ = ringFieldHamiltonian n N 0 isolated. Load-bearing for the operator identity that combines all three to produce the λ-parametrised Hamiltonian form consumed by the variational bound (Tasaki (4.1.37), p. 84). | Quantum/SpinS/RingReflectionBondSquareSusceptibilitySumRule.lean |
| ringBondSquareFieldHamiltonian_smulField_eq | (χ2b-iv) — λ-parametrised operator identity (RingReflectionBondSquareSusceptibilitySumRule.lean, Tasaki §4.1 (4.1.37)–(4.1.38), book p. 84, susceptibility sum rule / PR #5002): the bond-square field Hamiltonian at the scaled field λh decomposes as Ĥ_λ = H₀ + λ·V + (λ²·C(h))·1, where H₀ = ringFieldHamiltonian n N 0 is the field-free ring Heisenberg Hamiltonian, V = Σ_z (ringBondSquareLinField n h)_z·Ŝ³_z is the Zeeman perturbation (Tasaki’s −Ô_b, eq. (4.1.38)), and C(h) = ringBondSquareConst n h is the scalar constant. Combines the three scaling lemmas (χ2b-i/ii/iii) with the reduction ringBondSquareFieldHamiltonian_eq (Tasaki (4.1.37)) to yield the polynomial form essential for the variational expansion (Tasaki eq. (4.1.41), pp. 84–86). | Quantum/SpinS/RingReflectionBondSquareSusceptibilitySumRule.lean |
| ringBondSquareField_susceptibility_sum_rule | (χ2b-v — CAPSTONE) — Susceptibility sum rule (RingReflectionBondSquareSusceptibilitySumRule.lean, Tasaki §4.1 Theorem 4.2, eq. (4.1.41), book p. 84, susceptibility sum rule / PR #5002): CAPSTONE of χ2 (second-order perturbation phase): for a unique ground state Φ of the field-free ring Heisenberg Hamiltonian H₀ = ringFieldHamiltonian n N 0, there is a pseudoinverse potential y (orthogonal to Φ) satisfying (H₀−E₀)y = VΦ for the Zeeman perturbation V, whose susceptibility is bounded by the scalar constant, Re⟨y, VΦ⟩ ≤ C(h) = ½Σ(f_x+f_{x+1})². Proved by expanding χ1’s ground-energy bound E_GS(λh) ≥ E_GS(0) to second order at the trial state ψ_λ = Φ − λ·y: the variational lower bound combined with the operator identity ringBondSquareFieldHamiltonian_smulField_eq makes E_GS(λh) ≤ ⟨ψ_λ|Ĥ_λ|ψ_λ⟩/⟨ψ_λ|ψ_λ⟩ a quadratic λ-polynomial with vanishing first-order term (⟨Φ|V|Φ⟩ = 0, χ2a-v), whose λ → 0⁺ limit yields the sum rule (Tasaki (4.1.39)–(4.1.41), pp. 84–86, eqs. (4.1.38) / proof lines 1–11). Phrased in hsusc shape (the hypothetical-susceptibility carrier from no_long_range_order_1d_of_susceptibility) for general field h; staggered specialisation and the Green-function ≤ C·L bound belong to χ3 (next stage). This is the second-order perturbation gate toward Theorem 4.2 long-range order. | Quantum/SpinS/RingReflectionBondSquareSusceptibilitySumRule.lean |
| ringLeftFieldHamiltonian / ringLeftFieldHamiltonian_supportedOnLeft | Gaussian-domination layer 1 (RingReflectionFieldWeight.lean, Tasaki §4.1, toward Theorem 4.2): the field-augmented left Hamiltonian. For the Dyson–Lieb–Simon Gaussian-domination bound, the first infrastructure piece augments the left-half DLS part H_L with a diagonal single-site field Σ_{x < n} (a x) · Ŝ_x^{(3)}, yielding ringLeftFieldHamiltonian n N a = ringLeftHamiltonian + ∑_{x<n} (a x : ℂ) • onSiteS x (spinSOp3 N) (still left-supported); ringLeftFieldHamiltonian_supportedOnLeft proves left-supportedness (sum of left-supported terms) — the field-shifted left part Lfield(a) of Tasaki eq. (4.1.9). This is the foundation for the symmetric-field Gibbs weight and the Gaussian-domination RP cone. | Quantum/SpinS/RingReflectionFieldWeight.lean |
| ringFieldDLSDecomposition | Gaussian-domination layer 2 (RingReflectionFieldWeight.lean, Tasaki §4.1, toward Theorem 4.2): field-augmented DLS decomposition. The ring crossing reflection-positive decomposition instantiated with the field-augmented left part ringLeftFieldHamiltonian: ringFieldDLSDecomposition n N a = ringCrossingRPDecomposition (ringLeftFieldHamiltonian n N a) (ringLeftFieldHamiltonian_supportedOnLeft n N a). Its reconstructed Hamiltonian is the symmetric-field ring Hamiltonian Lfield(a) + θ(Lfield(a)) − crossing, the DLS form for the uniform-field Gaussian-domination bound Z_β(h) ≤ Z_β(0) (Tasaki §4.1, eqs. (4.1.49)–(4.1.51), p. 86). | Quantum/SpinS/RingReflectionFieldWeight.lean |
| ringReflectionThetaS_exp_mul_theta_exp | Gaussian-domination layer 5b (RingReflectionKineticConeRep.lean, Tasaki §4.1, PR #4976, toward Theorem 4.2): asymmetric kinetic merge for the two-field weight. For left-supported X and Y, the product exp X · θ(exp Y) merges into exp(X + θ Y) (the left-supported exp X and right-supported θ(exp Y) commute by disjoint supports). This is the two-field analogue of ringReflectionThetaS_exp_add_eq with independent left and right generators; placed in its own RingReflectionKineticConeRep.lean module to avoid importing MatrixExponential and creating a norm-instance diamond. Consumed by ringBondSquareTwoFieldWeight_isLimit as the kinetic-factor building block of the Lie-product convergence. | Quantum/SpinS/RingReflectionKineticConeRep.lean |
| ringFieldPartitionRe | RP capstone layer 7c (RingReflectionFieldPartition.lean, Tasaki §4.1 eqs. (4.1.47)–(4.1.51), pp. 85–86, physical field partition function / PR #4983): the physical per-site field partition function Z_β(h) := Re Tr exp(−β·Ĥ_field(h)), together with the field-splitting bookkeeping. The crux: the field-splitting map physFieldOf n a b : Fin (2n) → ℝ, defined as if z < n then a_z else −b(r z), realizes h as the physical field whose right-half Marshall gauge transform gives L_field(a) + θ(L_field(b)) − D (crux lemma AxisTwoPiRotS.rightGauge_conj_ringFieldHamiltonian), so the two sources of sign — the gauge’s −Ŝ³ on the right and physFieldOf’s −b(r z) — cancel (no new sign lemma needed, purely definitional from the split). Staggered-field sanity check (physFieldOf_self): the uniform staggered field h_x = (−1)ˣ h₀ decomposes as b_x = a_x. This field-splitting bridge is consumed by the bond-square reflection-positivity route toward Theorem 4.2. | Quantum/SpinS/RingReflectionFieldPartition.lean |
| ringFieldPartitionRe_translate / ringFieldPartitionRe_neg / ringFieldPartitionRe_pos | RP capstone layer 7d-i (RingReflectionFieldPartitionSymmetry.lean, Tasaki §4.1 eqs. (4.1.49)–(4.1.52), pp. 85–86, field partition symmetries / PR #4984): the three structural symmetries of the physical field partition function Z_β(h) = ringFieldPartitionRe n N β h consumed by the −log Z symmetrisation step (PR7d-ii/iii). (A) Translation invariance ringFieldPartitionRe_translate: Z_β(h) = Z_β(h ∘ finRotate) — the ring Hamiltonian is translation invariant (chainTranslation_conj_heisenbergHamiltonianS), so conjugation by the unitary ring translation carries Ĥ_field(h∘finRotate) to Ĥ_field(h) and the trace is invariant. (B) Spin-flip invariance ringFieldPartitionRe_neg: Z_β(−h) = Z_β(h) — a global axis-2 π-rotation fullGauge (the AxisTwoPiRotS.U on every site) preserves the Heisenberg dot product (fullGauge_conj_spinSDot) while flipping the field Σ_z h_z Ŝ³_z ↦ Σ_z (−h_z) Ŝ³_z, so Z_β(−h) = Z_β(h) by trace invariance. (C) Strict positivity ringFieldPartitionRe_pos: 0 < Z_β(h) — the field Hamiltonian is Hermitian (ringFieldHamiltonian_isHermitian), so exp(−β·Ĥ_field(h)) is positive definite (Matrix.posDef_exp_of_isHermitian), hence its trace is strictly positive; this is the genuine domain condition of the −log Z step. The period-2 staggered relabel P h z = (−1)^z h z (PR7d-ii) has period 2, so a single one-step shift produces a global sign: both A and B are required for cyclicity of the averaged potential in the classical chessboard lemma (Lemma 4.5, Tasaki pp. 87–88). | Quantum/SpinS/RingReflectionFieldPartitionSymmetry.lean |
| Matrix.posDef_exp_of_isHermitian | Math helper (generic finite-dim linear algebra, Math/PosSemidef/ExpPosDef.lean): the exponential of a Hermitian complex matrix is positive definite. For Hermitian A, exp A is positive definite: writing M = exp(A/2) (Hermitian + invertible), the split exp A = Mᴴ · M (via the commuting-exponent addition law exp(A/2 + A/2) = M·M) is positive definite by Matrix.PosDef.conjTranspose_mul_self. This avoids the continuous-functional-calculus route (which causes deterministic typeclass-resolution timeouts). Load-bearing strict positivity behind Z_β(h) = Tr exp(−βH) > 0 for Hermitian Hamiltonians (consumed by ringFieldPartitionRe_pos in the −log Z step) | Math/PosSemidef/ExpPosDef.lean |
| ringReflectionThetaS_ringLeftHamiltonian | RP infra layer 19 (RingReflectionRightBondSum.lean, Tasaki §4.1, toward Theorem 4.2): the reflected left bond Hamiltonian is the right bond Hamiltonian. Applying θ to the left bond sum reflects each left bond (x,x+1) to a right bond (r x, r(x+1)) = (2n−1−x, 2n−2−x): θ(ringLeftHamiltonian) = ∑_x [if x+1 < n then Ŝ_{r x}·Ŝ_{r(x+1)} else 0] (via ringReflectionThetaS_sum + ringReflectionThetaS_spinSDot). This is the right part θ(H_L) of the ring DLS decomposition | Quantum/SpinS/RingReflectionRightBondSum.lean |
| ringLeftHamiltonian_eq_leftBondSum | RP infra layer 18 (RingReflectionLeftBondSum.lean, Tasaki §4.1, toward Theorem 4.2): the left-half bond Hamiltonian as a sum over left bonds. Collapsing the left coupling’s double sum, ringLeftHamiltonian n N = ∑_x [if x+1 < n then Ŝ_x · Ŝ_{x+1} else 0] — only the bonds (x, x+1) entirely inside {0,…,n−1} survive (helpers ringLeftCoupling_succ_of_lt, ringLeftCoupling_eq_zero_of_ne, ringLeftCoupling_eq_zero_of_not_lt). The left part of the ring DLS decomposition over its actual bonds | Quantum/SpinS/RingReflectionLeftBondSum.lean |
| heisenbergHamiltonianS_ringCoupling_eq_bondSum | RP infra layer 17 (RingReflectionBondSum.lean, Tasaki §4.1, toward Theorem 4.2): the ring Heisenberg Hamiltonian as a sum over nearest-neighbor bonds. The directed coupling ringCoupling (2n) is 1 exactly on successor pairs (x, x+1 mod 2n), so the double sum collapses (Finset.sum_eq_single) to heisenbergHamiltonianS (ringCoupling (2n)) N = ∑_x Ŝ_x · Ŝ_{ringBondSucc x} (ringBondSucc x = x+1 mod 2n). This bond form is the starting point for the left/right/crossing bond split | Quantum/SpinS/RingReflectionBondSum.lean |
| ringLeftHamiltonian_supportedOnLeft | RP infra layer 16 (RingReflectionLeftHamiltonian.lean, Tasaki §4.1, toward Theorem 4.2): the left part H_L of the ring DLS decomposition is left-supported. SupportedOnLeftS.sum (left-supportedness closed under finite sums); heisenbergHamiltonianS_supportedOnLeft (a Heisenberg Hamiltonian whose coupling J x y vanishes unless both sites are in the left half is left-supported, being ∑_{x,y} J x y · Ŝ_x·Ŝ_y with each surviving term left-supported); ringLeftCoupling (the ring nearest-neighbor coupling restricted to left-half sites); and ringLeftHamiltonian = heisenbergHamiltonianS (ringLeftCoupling n) N, the concrete H_L that feeds ringCrossingRPDecomposition. The remaining bond-split match to the gauged ring Hamiltonian and the unitary ungauge are the next step | Quantum/SpinS/RingReflectionLeftHamiltonian.lean |
| ring_gibbs_rpTraceWeight (ring instance) | RP infra layer 15 (RingReflectionRingInstance.lean, Tasaki §4.1, toward Theorem 4.2): the DLS decomposition of the gauged ring antiferromagnet. The two crossing bonds of Fin (2n) are (n−1,n) and (2n−1,0), reflected from left sites n−1 and 0; ringCrossingRPDecomposition packages (for an arbitrary left-supported H_L) the RPDecomposition whose crossing bonds are the single-site spin operators at sites 0 and n−1, with ringCrossingRPDecomposition_interaction identifying its interaction as crossBondInteractionS 0 + crossBondInteractionS (n−1) and ringCrossingRPDecomposition_toHamiltonian giving toHamiltonian = H_L + θ(H_L) − (crossing). Then ring_gibbs_rpTraceWeight concludes (via the Gibbs capstone) that the gauged ring Gibbs weight exp(−β·(H_L+θ(H_L)−crossing)) is a reflection-positive trace weight (β ≥ 0). Also spinSDot_supportedOnLeft (a left-half bond is left-supported). The concrete left-bond H_L and the unitary equivalence to heisenbergHamiltonianS (ringCoupling (2n)) are the next step | Quantum/SpinS/RingReflectionRingInstance.lean |
| RPDecomposition.gibbs_rpTraceWeight (Gibbs RP capstone) | RP infra layer 14 (RingReflectionGibbsCapstone.lean, Tasaki §4.1, toward Theorem 4.2): full Gibbs reflection positivity — for a reflection-positive decomposition H = H_L + θ(H_L) − D (RPDecomposition) and β ≥ 0, the Gibbs weight exp(−β·H) is a reflection-positive trace weight. The Dyson–Lieb–Simon Trotter assembly: e^{−βH} = e^{A+B} (A = −β·(H_L+θH_L), B = β·D), via the Lie product formula e^{A+B} = lim_m (e^{A/m}·e^{B/m})^m (LieProduct.lieProductFormula); each factor is consumed by an accumulating RP trace weight — the kinetic factor e^{A/m} = exp(Y+θY) is cone-representable (coneRep_exp_add + mul_coneRep_right) and the interaction factor e^{B/m} is the exp of a cone-representable operator (mul_exp_coneRep_right) — then induction over the power and RPTraceWeightS.tendsto. Helpers: realSmul_add_theta, RPDecomposition.interaction_coneRep. This is the reflection positivity at the heart of the DLS / Shastry argument | Quantum/SpinS/RingReflectionGibbsCapstone.lean |
| RPTraceWeightS.mul_exp_coneRep_right | RP infra layer 13 (RingReflectionMulExpConeRep.lean, Tasaki §4.1, toward Theorem 4.2): an RP trace weight absorbs the exponential of a cone-representable operator. If M is RP and P is RPTraceConeRepS, then M · exp P is RP — the partial sums ∑_{k<m}(k!)⁻¹Pᵏ are cone-representable (pow/smul_nonneg/add), so each M·(partial sum) is RP (mul_coneRep_right), and M·exp P is their limit (continuity of left multiplication + RPTraceWeightS.tendsto). This consumes the interaction Gibbs factor e^{βD/m} in the Trotter expansion | Quantum/SpinS/RingReflectionMulExpConeRep.lean |
| coneRep_exp_add (kinetic factor) | RP infra layer 12 (RingReflectionKineticConeRep.lean, Tasaki §4.1, toward Theorem 4.2): the kinetic Gibbs factor is cone-representable. For left-supported X, exp(X + θ X) = exp X · θ(exp X) = θ(exp X) · exp X (ringReflectionThetaS_exp_add_eq, via exp_add_of_commute since X and θ(X) commute, θ(exp X) = exp(θ X), and mul_theta_comm); the right-hand side is a single cone generator θ(L)·L (L = exp X left-supported), so coneRep_exp_add gives RPTraceConeRepS (exp(X + θ X)). This is the kinetic building block (e^{−βH₀/m}) the Trotter expansion of e^{−βH} consumes | Quantum/SpinS/RingReflectionKineticConeRep.lean |
| RPTraceWeightS.mul_coneRep_right (cone closure) | RP infra layer 11 (RingReflectionRPWeightCone.lean, Tasaki §4.1, toward Theorem 4.2): the reflection-positive trace weights form a convex cone — RPTraceWeightS.zero/one (the identity is RP, the β=0 trace cone), add, smul_nonneg, sum (closed under finite sums) — and RPTraceWeightS.mul_coneRep_right: an RP trace weight times a cone-representable operator (RPTraceConeRepS) is again RP (since M·∑cᵢθ(Cᵢ)Cᵢ = ∑cᵢ(M·θ(Cᵢ)Cᵢ), each RP by the cone-generator closure, summed). This is the algebraic engine that accumulates reflection positivity factor-by-factor in the Trotter expansion of e^{−βH} | Quantum/SpinS/RingReflectionRPWeightCone.lean |
| RPTraceWeightS.mul_weightGen_right / RPTraceWeightS.weightGen_mul_left | RP infra layer 10 (RingReflectionGibbsRP.lean, Tasaki §4.1, toward Theorem 4.2): closure of reflection-positive trace weights under cone generators θ(L)·L (L left-supported). The naive “conjugation” closure M ↦ L·M·θ(L) is false (the homomorphism order θ(LA)=θ(L)θ(A) clashes with the test operator B=AL, and left-supported operators do not commute); the correct closure multiplies by a cone generator: M·(θ(L)·L) is RP (substitute the test operator A ↦ L·A, using L·θ(A)=θ(A)·L and θ(L)·θ(A)=θ(L·A)) and (θ(L)·L)·M is RP (substitute A ↦ A·L, via trace cyclicity). These are the kinetic-factor building blocks of the full Dyson–Lieb–Simon Gibbs reflection positivity | Quantum/SpinS/RingReflectionGibbsRP.lean |
| crossBondInteractionS / RPDecomposition | RP infra layer 9 (RingReflectionRPDecomposition.lean, Tasaki §4.1, toward Theorem 4.2): the DLS decomposition data and the crossing-bond interaction. crossBondInteractionS x = Σ_α Ŝ_x^α·θ(Ŝ_x^α) (left site x), with the gauge identity crossBondInteractionS x = Ŝ_x^1 Ŝ_{r x}^1 − Ŝ_x^2 Ŝ_{r x}^2 + Ŝ_x^3 Ŝ_{r x}^3 (the lone − on the Ŝ^2 term is the sign flipped by the DLS/Marshall gauge — a π-rotation around axis 2 on the right half — making all three components contribute the same negative reflection-positive sign). Each onSiteS x Ŝ^α (x<n) is left-supported; crossBondInteractionS_exp_rpTraceWeight shows exp(t·crossBondInteractionS x) (t≥0) is a reflection-positive trace weight (via mul_theta_comm + the interaction-exponential cone). The abstract RPDecomposition structure (H_L + θ(H_L) − Σ_b C_b·θ(C_b), all C_b left-supported) packages the DLS form, with interaction_exp_rpTraceWeight giving the Gibbs interaction factor’s reflection positivity | Quantum/SpinS/RingReflectionRPDecomposition.lean |
| no_long_range_order_1d | Corollary 4.3 (§4.1, THEOREM; eq. (4.1.11)): absence of LRO in 1D on even rings. For the zero-field 1D AFM Heisenberg ring on even L sites (Even L, bipartite — faithful to Tasaki §3.1/§4.1.1 which define the lattice for even L only), the squared staggered order parameter per site vanishes in the thermodynamic limit lim_{L↑∞} ⟨Φ_GS\|(Ô_L^(3)/L)²\|Φ_GS⟩ = 0 (ε–δ form). Discharged (PR #5003) by feeding the documented Shastry susceptibility axiom shastry_staggered_susceptibility_bound (χ(k*)≤C·L) into the conditional reduction no_long_range_order_1d_of_susceptibility for N ≥ 1; the degenerate spin-0 case N = 0 is unconditional (the staggered order operator vanishes). #print axioms = [propext, Classical.choice, Quot.sound, shastry_staggered_susceptibility_bound] | Quantum/SpinS/NoLongRangeOrder1D.lean |
| shastry_staggered_susceptibility_bound | Shastry susceptibility bound χ(k*)≤C·L (§4.1, DOCUMENTED AXIOM; toward Corollary 4.3): for the zero-field 1D AFM Heisenberg ring on even L ≥ 2 sites (Even L, bipartite) there is a size-uniform C ≥ 0 with every normalized ground state admitting a potential y for ÔΦ ((Ĥ−E₀)y=ÔΦ) of O(L) static staggered susceptibility Re⟨y,ÔΦ⟩ ≤ C·L (physically χ(k*)=L·f_L^(-1)(k*)). Tasaki does not prove this in the book — footnote 3 (p. 76) cites Shastry [58] / the rigorous formulation of Tanaka–Takeda–Idogaki [63], and footnote 9 (p. 83) singles out the f_L^(-1)(k*) bound as the only “nontrivial part that requires some hard analysis”. Per the project’s explicit instruction this genuinely external hard-analysis estimate (massive-Green / inverse-Fourier k*=π control) based on Shastry J.Phys.A 25 L249 (1992) [58] and Tanaka–Takeda–Idogaki JMMM 272–276 908 (2004) [63] is a documented axiom; it discharges no_long_range_order_1d (PR #5003) | Quantum/SpinS/NoLongRangeOrder1D.lean |
← Generic matrix-analysis helpers (Math/MatrixAnalysis/) · Catalogue · Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1) →