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 |
|---|---|---|
akltHamiltonianS / aklt_theorem_7_1 |
§7.1.1 Theorem 7.1 (the AKLT main theorem; PROVED, #print axioms = std3, PR #5131; eqs. (7.1.1)–(7.1.2)): the Affleck–Kennedy–Lieb–Tasaki S=1 chain. akltHamiltonianS L = Σ_x {Ŝ_x·Ŝ_{x+1} + ⅓(Ŝ_x·Ŝ_{x+1})²} (eq. 7.1.1, PBC ring, SU(2)-invariant; the biquadratic term puts it outside Marshall–Lieb–Mattis). aklt_theorem_7_1 is now a theorem (formerly a documented axiom): for all sufficiently large chains (L = n+1, any parity) it gives all four conjuncts — a unique ground state Φ (= the valence-bond-solid VBS state; nonzero eigenvector at E₀, every ground eigenvector ∝ Φ); a spectral gap ≥ ΔE₀ = 1/5 for a positive L-independent ΔE₀ (IsPositiveSpectralGap); and the exact correlation ⟨Φ,Ŝ_x·Ŝ_y Φ⟩/⟨Φ,Φ⟩ → 4(−3)^{−\|x−y\|} (eq. 7.1.2, sign-alternating exponential decay) for fixed sites with \|x−y\| ≥ 1, as L↑∞ (chainSite embedding, eventual-ε form). ΔE₀ and Φ quantified outermost. Proof: pure composition of the three independently discharged conjunct-theorems — existence+eigenvalue+ground-energy+gap aklt_knabe_ring_gap (§7.1.4), uniqueness aklt_ring_ground_state_unique (§7.1.3), correlation decay aklt_correlation_decay (§7.2.2); witnesses ΔE₀=1/5, Φ n = akltVBSState (n+1), E₀ n = −(2/3)(n+1), n₀ = max nK 2. Axiom-free (no operator algebra, no infinite volume) |
Quantum/SpinS/AKLTTheorem71.lean; Quantum/SpinS/AKLT.lean (Hamiltonian def); Quantum/SpinS/AKLTKnabe/KnabeGapD7d.lean; Quantum/SpinS/AKLTUniqueness/GroundStateUnique.lean; Quantum/SpinS/AKLTCorrelationDecay.lean |
IsAKLTChainDynamics / aklt_theorem_7_2 |
§7.1.3 Theorem 7.2 (Matsui; AXIOM, operator-algebraic): the AKLT model on the infinite chain has a unique gapped ground state. On the quasi-local C-algebra, a state ω is a ground state iff IsGroundState ω δ (Def A.25: ω(†[Ĥ,Â])≥0) and has a nonzero gap iff HasNonzeroGap ω δ γ (Def A.27, γ>0). For the 1D InfiniteSpinSystem with the AKLT dynamics δ (tied by the uninterpreted marker IsAKLTChainDynamics), aklt_theorem_7_2 gives ∃ ω, IsState ω, IsGroundState ω δ, unique among states (∀ω', IsState ω' → IsGroundState ω' δ → ω'=ω), and ∃γ, HasNonzeroGap ω δ γ. The unique GS is the L↑∞ limit of the VBS state. Proof: Matsui (uniqueness) on AKLT; documented operator-algebra axiom (per the C-algebra policy) |
Quantum/SpinS/AKLTInfiniteChain.lean |
IsAKLTPerturbation / perturbedAKLTHamiltonianS / aklt_theorem_7_3 |
§7.1.3 Theorem 7.3 (Yarotsky stability; AXIOM; eq. (7.1.4)): the AKLT gap is stable under small local perturbations. perturbedAKLTHamiltonianS L ε v = akltHamiltonianS L + ε Σ_x v̂_x (eq. 7.1.4); IsAKLTPerturbation L r v₀ v bundles: each v̂_x Hermitian, r-local (IsLocalRangeR, now the commutant-form def shared with §6.2 Lemma 6.4 — genuine spatial locality keeps this Theorem 7.3 hypothesis faithful), bounded (manyBodyOperatorNormS ≤ v₀), and translation-covariant (IsTranslationCovariant, an uninterpreted marker for v̂_x = T̂^x v̂_o T̂^{−x}). For range r bounded by v₀, ∃ ε₀>0 such that for |ε|<ε₀ there are ΔE,C,ξ>0 L-independent with: for any L ≥ 3 and any such v, the perturbed AKLT chain has a unique ground state (IsUniqueChainGroundState), a gap ≥ ΔE (IsPositiveSpectralGap), and exponential decay of the connected correlation |connectedChainCorrelation| ≤ C e^{−d(x,y)/ξ} (ringDist). The connected/truncated correlation ⟨Ŝ_x·Ŝ_y⟩ − Σ_α⟨Ŝ_x^(α)⟩⟨Ŝ_y^(α)⟩ is used since a symmetry-breaking perturbation can give nonzero one-point functions (the raw correlation need not decay); L ≥ 3 excludes the degenerate small rings. The gapful AKLT phase is stable. Proof: cluster expansion (Yarotsky) |
Quantum/SpinS/AKLTStability.lean |
bondSpin2ProjectionS / bondLocal_ker_eq_vbsBondSubspace / bondSpin2ProjectionS_mulVec_eq_zero_iff_bondSlice_mem_ker / tasaki_lemma_7_4 |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/AKLTBondProjection.lean |
sum_fin2_fin3 / spinSDot_fin2_apply / spinSDot_fin2_apply' / spinSOpPlus_two_apply / spinSOpMinus_two_apply / spinSOp3_two_apply |
Spin-1 (N = 2) two-site matrix entries (PROVED, #print axioms = std3, PR #5095; model-independent linear algebra; spin-1 conventions per Tasaki, 1st ed. (2020), §2.2, pp. 30–34): the shared entry-level base for every explicit 9×9 computation on ℂ³ ⊗ ℂ³. sum_fin2_fin3 enumerates a sum over the nine configurations Fin 2 → Fin 3. spinSOpPlus_two_apply / spinSOpMinus_two_apply give the spin-1 ladder entries (√2 on the raising resp. lowering pairs, 0 otherwise) and spinSOp3_two_apply the diagonal Ŝ^{(3)} entries 1 − k. spinSDot_fin2_apply discharges the off-bond delta of spinSDot on Λ = Fin 2, exhibiting Ŝ_0 · Ŝ_1 as the plain tensor ∑_α Ŝ^{(α)} ⊗ Ŝ^{(α)}, and spinSDot_fin2_apply' rewrites it in the imaginary-free ladder form ½ (Ŝ⁺ ⊗ Ŝ⁻ + Ŝ⁻ ⊗ Ŝ⁺) + Ŝ^{(3)} ⊗ Ŝ^{(3)}, so downstream kernel computations stay over rational multiples of √2. Previously private helpers of AKLTBondProjection.lean; moved (not copied) here so the AKLT bond spin-2 projection and the Knabe finite-size gap estimates share one copy |
Quantum/SpinS/SpinOneTwoSiteEntries.lean |
aklt_knabe_ring_gap |
§7.1.4 Knabe’s argument for the AKLT gap (PROVED, #print axioms = std3, PR #5122; Tasaki, 1st ed. (2020), §7.1.4, pp. 188–190; S. Knabe, J. Stat. Phys. 52, 627 (1988)): the finite-volume spectral gap of the S=1 AKLT ring. For every ring of length L = n+1 ≥ 5 with no parity restriction, the capstone aklt_knabe_ring_gap proves: the existence of the explicit periodic valence-bond-solid state akltVBSState L as a nonzero eigenvector at ground energy −(2/3)L, and a spectral gap ≥ 1/5 (uniform in L). These are the existence and gap conjuncts (1) and (5) of Tasaki Theorem 7.1; together with the uniqueness (§7.1.3) and correlation (§7.1.2) conjuncts they are composed into the now-theorem aklt_theorem_7_1 (AKLTTheorem71.lean, PR #5131). The proof follows Knabe’s aggregation of bond projectors: (Ĥ′)² ≥ (1/10)Ĥ′ (Gate D6d, §6.2 two-site Knabe inequality), normalized to the ring Hamiltonian by Ĥ_AKLT = 2Ĥ′ − (2/3)L (eq. 7.1.5), giving a gap of 1/5 = 2·(1/10) after normalization transport. Proof: Knabe finite-size spectral bound via bond projector aggregation, frustration-freeness of the VBS, and Courant–Fischer |
Quantum/SpinS/AKLTKnabe/KnabeGapD7d.lean |
finrank_highestWeightE3_window |
§7.1.4 Knabe window: highest-weight dimensions of the four-site spin-1 block (Tasaki, 1st ed. (2020), §7.1.4, pp. 188–190; PR #5149): dim hw_k = 1, 3, 6, 6, 3 for k = 0, …, 4 in (ℂ³)^{⊗4}, i.e. the multiplicities of the total-spin sectors S = 4, 3, 2, 1, 0 (Σ_S (2S+1) k_S = 81). This is the 81 → 1+3+6+6+3 reduction on which the Knabe window bound ĥ² ≥ (2/5) ĥ — the ε_ℓ step of (7.1.37)–(7.1.38) — is checked |
Quantum/SpinS/AKLTKnabe/Sl2LadderSectorsE3.lean |
bondFactor / weylMap / fBond / fBond_dvd_weylMap_of_isVBSGroundForm / weylMap_ground_form_eq_const_smul_prod / ground_eigen_isVBSGroundForm / aklt_ring_ground_state_unique |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/AKLTUniqueness/GroundStateUnique.lean; Quantum/SpinS/AKLTUniqueness/ProductBondDivisibility.lean; Quantum/SpinS/AKLTUniqueness/BondDivisibilityBridge.lean; Quantum/SpinS/AKLTUniqueness/LocalBondDivisibility.lean; Math/MvPolynomial/WeylSpinOneMap.lean; Math/MvPolynomial/BilinearFactorCoprime.lean; Math/MvPolynomial/PairwiseCoprimeProd.lean |
expectationRatioRe_sum / spinSDot_eq_sum_component / aklt_correlation_decay |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/AKLTCorrelationDecay.lean; Quantum/SpinS/AKLTStringOrderTransfer.lean; Quantum/SpinS/AKLTStringOrderCovariance.lean |
akltVBSMatrices / akltVBSState / spinSStringPhaseS1 / stringOperatorS / stringCorrelationS / stringOperatorAxisS / stringCorrelationAxisS / aklt_string_order_7_2_8 |
§7.2.1 hidden antiferromagnetic order / string order parameter (PROVED, Standard 3; Tasaki, 1st ed. (2020), §7.2.1, corrected eqs. (7.2.6)–(7.2.8), pp. 193–194; §7.2.2, eqs. (7.2.12)–(7.2.25), pp. 195–198; Problem 7.2.2.c–d, p. 200, and solutions (S.73)–(S.76), pp. 507–508): akltVBSState is the unnormalized periodic bond-dimension-two, spin-one trace-product MPS built from akltVBSMatrices. Equation (7.2.6) has exactly one leading minus in stringCorrelationAxisS; the official author erratum removes the extra minus on the right of eq. (7.2.7). The strict-window operator stringOperatorS x y uses the concrete phase spinSStringPhaseS1 = diag(−1,1,−1), while stringOperatorAxisS α x y and stringCorrelationAxisS α x y give the same construction for every α : Fin 3. The axis-three transfer calculation proves the exact finite correlation and its uniform thermodynamic estimate; explicit physical rotations and auxiliary gauges prove finite-volume equality with axes one and two. Consequently aklt_string_order_7_2_8 proves the full three-axis value 4/9 in the explicit iterated-ε form, with the inner L↑∞ limit before the separation limit. This direct calculation has no logical dependency on Theorems 7.1, 7.5, or 7.6. |
Quantum/SpinS/AKLTStringOrderDefs.lean; Quantum/SpinS/AKLTStringOrderTransfer.lean; Quantum/SpinS/AKLTStringOrderCovariance.lean; Quantum/SpinS/AKLTStringOrder.lean |
mpsDualTransferMap / HasFaithfulDualEigenmatrix / mps_spans_eventually_iff_spans_for_all_large / mps_spans_for_all_large_iff_has_primitive_transfer_spectrum / mps_theorem_7_5 / GeneratesSameMPS / mps_theorem_7_6 |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/MPSTheorem75Defs.lean; Quantum/SpinS/MPSTheorem75Linear.lean; Quantum/SpinS/MPSTheorem75Choi.lean; Quantum/SpinS/MPSTheorem75Peripheral.lean; Quantum/SpinS/MPSTheorem75.lean; Quantum/SpinS/MPSTheorem76Defs.lean; Quantum/SpinS/MPSTheorem76Algebra.lean; Quantum/SpinS/MPSTheorem76Unitary.lean; Quantum/SpinS/AKLTMatrixProduct.lean |
bondMaxSpinProjectionS / bondMaxSpinProjectionS_comm / regularGraphAKLTHamiltonianS / IsGeneralGraphVBSGroundState / tasaki_theorem_7_7 |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/GeneralAKLT.lean |
spinThreeHalfVBSBondVec / spinThreeHalfVBSBondSubspace / spinThreeHalfBondMaxProjection / spinThreeHalfVBSBondVec_linearIndependent / spinThreeHalfVBSBondVec_annihilated / bondMaxSpinProjectionS_three_local_rank / finrank_spinThreeHalfBondLocal_ker / spinThreeHalfBondLocal_ker_eq_vbsBondSubspace / bondMaxSpinProjectionS_three_local_isHermitian / bondMaxSpinProjectionS_three_local_idempotent / bondMaxSpinProjectionS_three_posSemidef / bondMaxSpinProjectionS_three_eq_onEmbS |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/SpinThreeHalfBondProjection.lean; Quantum/SpinS/SpinThreeHalfBondEmbedding.lean |
HoneycombVertex / HoneycombForwardDart / HoneycombVirtualConfig / honeycombIncidenceSpin / honeycombVirtualDownCount / HoneycombVirtualConfig.Realizes / honeycombSingletWeight / honeycombSymmetrizerWeight / honeycombVBSState / honeycombVBSState_ne_zero |
§7.3.2 finite honeycomb VBS amplitude (PROVED, #print axioms = std3, PR #5133; Tasaki, Physics and Mathematics of Quantum Many-Body Systems, 1st ed. (Springer, 2020), §7.3.2, eq. (7.3.6), p. 210; periodic bipartition in footnote 42, p. 211): as a formal orientation convention, HoneycombForwardDart m chooses the honeycomb darts from sublattice A to B. A virtual bit chooses one of the two normalized singlet terms; honeycombIncidenceSpin uses that bit at the A incidence and Fin.rev at the B incidence. HoneycombVirtualConfig.Realizes matches the three virtual down-spin incidences at each site with its physical Fin 4 basis index. honeycombVBSState m is the literal finite sum of the normalized singlet coefficient 2^{-|E|/2}(-1)^{n_{\downarrow,A}} times the product of normalized on-site symmetric coefficients choose(3,k_x)^{-1/2}. It is not asserted to be globally unit normalized. For m ≥ 2, the basis coefficient with down count 0 on A and 3 on B has the unique all-zero forward virtual configuration and equals (√2⁻¹)^{|E|} ≠ 0; hence honeycombVBSState_ne_zero. The separate bond-annihilation capstone below consumes this amplitude; the following zero-energy capstone assembles it into the full ground-state property. Finite-volume uniqueness, correlation decay, a spectral gap, and infinite-volume uniqueness remain unproved; tasaki_theorem_7_7 remains an axiom. |
Quantum/SpinS/HoneycombAKLTVBS.lean |
glueTwoSitesS / twoSiteSliceS / twoSiteSliceS_onEmbS_mulVec / onEmbS_mulVec_eq_zero_iff_twoSiteSlices / bondMaxSpinProjectionS_three_eq_onEmbS / bondMaxSpinProjectionS_three_mulVec_eq_zero_iff_slices / honeycombVBSState_twoSiteSlice_mem / honeycombVBSState_bond_annihilated |
§7.3.2 honeycomb VBS bond annihilation (PROVED, #print axioms = std3, PR #5133; Tasaki, Physics and Mathematics of Quantum Many-Body Systems, 1st ed. (Springer, 2020), §7.3.2, eq. (7.3.7), p. 210): twoSiteSliceS x y Φ τ freezes every spectator coefficient, and the generic onEmbS bridge proves that an embedded two-site matrix annihilates Φ iff its local matrix annihilates every slice. The spin-three-half specialization transports the local Gate L projector certificate to any distinct pair and rewrites its kernel as spinThreeHalfVBSBondSubspace. For a forward honeycomb dart d in the chosen A → B orientation, the virtual sum is reindexed by the selected bit and all remaining bits. Each fixed-rest fibre is a scalar multiple of one of the nine local VBS generators, so every slice lies in the local kernel and P̂₃[d.fst+d.snd] honeycombVBSState = 0. Since forward darts represent undirected edges bijectively, this is the per-bond ingredient of eq. (7.3.7). It does not define or identify the full Hamiltonian sum and does not prove positive semidefiniteness of that sum, zero energy, uniqueness, correlations, a gap, or any infinite-volume statement. The two configuration-level definitions glueTwoSitesS / twoSiteSliceS live in the leaf module Quantum/SpinS/TwoSiteConfig.lean (PR #5139), shared with the §7.1.3 ring-bond specializations glueBond / bondSlice; the general fixed-point lemma glueTwoSitesS_eq_self is proved there. |
Quantum/SpinS/TwoSiteConfig.lean; Quantum/SpinS/TwoSiteSliceS.lean; Quantum/SpinS/SpinThreeHalfBondEmbedding.lean; Quantum/SpinS/HoneycombAKLTBondAnnihilation.lean |
honeycombVBSState_adj_bond_annihilated / honeycombVBSState_isGeneralGraphVBSGroundState |
§7.3.2 Zero-energy ground state of the finite honeycomb AKLT Hamiltonian (PROVED, #print axioms = std3, PR #5133; Tasaki, Physics and Mathematics of Quantum Many-Body Systems, 1st ed. (Springer, 2020), §7.3.2, Lemma A.9, p. 469): honeycombVBSState_adj_bond_annihilated extends the per-bond annihilation to every ordered adjacent pair (x, y), using the forward-dart and reverse-dart coverage plus the bond-projection symmetry bondMaxSpinProjectionS_comm. The capstone honeycombVBSState_isGeneralGraphVBSGroundState assembles the per-bond ingredients into the full frustration-free zero-energy ground-state property via the ε ≡ 0 specialization of Tasaki’s Lemma A.9 (frustration_free_isGroundState): each local bond term is positive semidefinite (bondMaxSpinProjectionS_three_posSemidef) and annihilates the state, so their sum is positive semidefinite and annihilates the state; the prefactor ½ recovers regularGraphAKLTHamiltonianS. This proves IsGeneralGraphVBSGroundState (honeycombTorusGraph m) 3 (honeycombVBSState m) for m ≥ 2, realizing the ground-state hypothesis of Tasaki Theorem 7.7 on the canonical honeycomb torus. Correlation decay and infinite-volume uniqueness remain unproved; tasaki_theorem_7_7 remains an axiom. |
Quantum/SpinS/HoneycombAKLTZeroEnergy.lean |
graphStateHamiltonianS / brStabilizer / tasaki_theorem_7_8 |
§7.3.3 Briegel–Raussendorf (cluster / graph) state (Theorem 7.8; Tasaki §7.3.3, pp. 217–220, eqs. (7.3.29)–(7.3.40)): the S=1/2 stabilizer state, the qubit analogue of the VBS. pauliXS x = 2Ŝ_x^{(1)} = σ_x^x, pauliZS x = 2Ŝ_x^{(3)} = σ_x^z (qubits, N=1, on Fin L); neighborZProduct G x = the diagonal ∏_{y∼x} σ_y^z (acting by ∏_{y∼x}(−1)^{σ_y}); brStabilizer G x = σ_x^x ∏_{y∼x} σ_y^z = K̂_x (stabilizer, K̂_x²=1, eigenvalues ±1); graphStateHamiltonianS G = −Σ_x K̂_x (eq. 7.3.30). tasaki_theorem_7_8 (PROVED, PR #5136, #print axioms = std3, 0 < L): the cluster state Φ (IsClusterState marker, concrete clusterStateVec G) is the unique ground state with E_GS = −N (N = |Λ| = L, IsGroundEnergy), gap above it exactly 2 (IsPositiveSpectralGap … 2; 0 < L excludes the 1-dim empty lattice), and every ground-energy eigenvector ∝ Φ. Proof: map Ĥ_BR via controlled-Z unitary Û_C (Û_C²=1) to diagonal −Σ σ_x^x; spectral analysis yields E_GS = −L, gap = 2, unique GS. |
Quantum/SpinS/ClusterState.lean |
anisotropicChainHamiltonianS / tasaki_theorem_8_1 |
§8.1.1 Large-D phase of the anisotropic S=1 chain (Theorem 8.1; eqs. (8.1.1)–(8.1.3)): the topological phase transition. anisotropicChainHamiltonianS L D = heisenbergHamiltonianS (ringCoupling L) 2 + D Σ_x (Ŝ_x^{(3)})² (eq. 8.1.1, Ĥ_D = Σ_x[Ŝ_x·Ŝ_{x+1} + D(Ŝ_x^{(3)})²], PBC ring, crystal-field anisotropy); spinSSiteComponentS α x selects Ŝ_x^{(α)} (α : Fin 3). tasaki_theorem_8_1 (AXIOM): ∃ D₀>0 s.t. for D ≥ D₀ there are L-independent ΔE₀,C,ξ>0 with, for every even L≥2, a unique ground state (IsUniqueChainGroundState), a gap ≥ ΔE₀ (IsPositiveSpectralGap), and exponential decay |⟨Ŝ_x^{(α)}Ŝ_y^{(α)}⟩| ≤ C e^{−d(x,y)/ξ} for all three α (d = ringDist) — the large-D phase is unique, disordered, gapped. Raw = connected here (disordered symmetric GS, one-point fns vanish). Proof: cluster-expansion perturbation theory (large D, book D₀≈28; phase to D_c≈1) |
Quantum/SpinS/AnisotropicLargeD.lean |
openAnisotropicChainHamiltonianS / HasStringLRO / tasaki_theorem_8_2 |
§8.1.2–§8.1.3 Hidden order forces edge states (Theorem 8.2, Koma–Tasaki; eqs. (8.1.9)–(8.1.11)): in the anisotropic chain, hidden antiferromagnetic order (positive den Nijs–Rommelse string order O_string^{(α)}(D), §7.2.1) distinguishes the Haldane phase (0≤D<D_c) from the large-D phase, and forces low-lying edge states. openAnisotropicChainHamiltonianS L D is the open-boundary anisotropic chain (openAnisotropicChainCoupling, no wrap-around — the free ends carry the S=1/2 edge spins). HasStringLRO L D Φ q (marker) is the hidden-order bound (8.1.10) ⟨Φ\|(Ô_string^{(α)}/L)²\|Φ⟩ ≥ q_α (q_α>0). tasaki_theorem_8_2 (AXIOM): for fixed D, q there are L-independent C_ν>0 such that for every L>0, whenever Φ is the unique ground state (IsUniqueChainGroundState) of Ĥ_D^open at E₀ with HasStringLRO, there are three linearly independent excited states Ψ_ν (ν:Fin 3, LinearIndependent ℂ Ψ) with Ĥ_D^open Ψ_ν = E_ν Ψ_ν and E₀ < E_ν ≤ E₀ + C_ν/L — hidden order ⟹ near four-fold degeneracy (free S=1/2 edge spins). C_ν quantified outside ∀L (genuinely length-uniform). Proof: Horsch–von der Linden / Koma–Tasaki variational argument (as Theorem 3.1) |
Quantum/SpinS/AnisotropicEdgeStates.lean |
lambdaDChainHamiltonianS / tasaki_theorem_8_3 |
§8.2.1 λ-D model: Néel ≤ string order (Theorem 8.3, Kennedy–Tasaki; eqs. (8.2.1)–(8.2.4)): the two-parameter Haldane-phase model. lambdaDChainHamiltonianS L λ D = Σ_{x,y} [openAnisotropicChainCoupling] · spinSDotXXZ x y λ 2 + D Σ_x (Ŝ_x^{(3)})² (eq. 8.2.1, Ĥ_{λ,D} = open XXZ chain with Ising anisotropy λ + crystal field D; λ=1 ⇒ open-boundary version of the anisotropic model 8.1.1, agreeing in the bulk). neelOrderParameterS/stringOrderParameterS (markers, ℝ→ℝ→Fin 3→ℝ) are the thermodynamic double-limit Néel (8.2.2) and den Nijs–Rommelse string (8.2.3) order parameters of the GS. tasaki_theorem_8_3 (AXIOM, eq. 8.2.4): for λ≥0 and any D, O_Néel^{(α)} ≤ O_string^{(α)} for all α — nonzero Néel order (Ising AF phase) forces nonzero hidden order. tasaki_neel_transverse_eq_nonneg (λ≥0): O_Néel^{(1)} = O_Néel^{(2)} ≥ 0. Proof: path-integral representation (§6.3) |
Quantum/SpinS/LambdaDModel.lean |
ktUnitaryS / piRotationS / IsZ2Z2Invariant / tasaki_prop_8_4 |
§8.2.2–§8.2.3 Kennedy–Tasaki transformation + Proposition 8.4 (Pollmann–Turner–Berg–Oshikawa; eqs. (8.2.5)–(8.2.7)): the nonlocal unitary realizing hidden Z₂×Z₂ symmetry breaking. ktUnitaryS L (marker) is the Kennedy–Tasaki unitary Û_KT = ∏_{u<v} exp(iπ Ŝ_u^{(3)} Ŝ_v^{(1)}) (eq. 8.2.5), with ktUnitaryS_sq (Û_KT²=1) and ktUnitaryS_selfAdjoint (Û_KT=Û_KT†) — a self-adjoint involution. piRotationS L α = ∏_x exp(iπ Ŝ_x^{(α)}) (concrete, on-site matrix exponentials) is the π-rotation about axis α; IsZ2Z2Invariant H = (Û_π^{(α)})† H Û_π^{(α)} = H for all α (commutes with all three π-rotations). HasShortRangeInteraction/HasSomeShortRangeInteraction (markers) capture range-r locality. tasaki_prop_8_4 (AXIOM): for a short-range open-chain Ĥ, Û_KT Ĥ Û_KT is again short-range iff Ĥ is Z₂×Z₂ invariant — the hidden-symmetry-breaking picture is effective exactly when Ĥ has Z₂×Z₂ symmetry |
Quantum/SpinS/KennedyTasakiTransformation.lean |
guWenHamiltonianS / IsSPTPhase / tasaki_oshikawa_8_3_3 |
§8.3.1–§8.3.2 Symmetry protected topological (SPT) phase (Gu–Wen / Pollmann–Turner–Berg–Oshikawa; eqs. (8.3.1)–(8.3.4)): the Haldane phase as an SPT phase. guWenHamiltonianS L D B = anisotropicChainHamiltonianS L D + B Σ_x Ŝ_x^{(1)} (eq. 8.3.4, S=1 chain + magnetic field B in 1-dir, breaks Z₂×Z₂→Z₂; B=0 ⇒ anisotropic 8.1.1). tasaki_oshikawa_8_3_3 (AXIOM, eq. 8.3.3): the spin-S VBS string order O_string^{(α)} is >0 for odd S, =0 for even S (even/odd-S distinction); tasaki_vbs_edge_degeneracy (AXIOM): the spin-S AKLT open chain has (S+1)²-fold edge degeneracy. SPT definition (def : Prop, NOT axiom): HamiltonianPath (continuous ℝ→ Hamiltonian, each short-range gapped-unique via IsShortRangeGappedUniqueGS marker); ContinuouslyConnected/SymmetryConnected sym (path with all Ĥ_s having the symmetry sym); IsTrivialPhase sym H = symmetry-connected to a product state (IsProductStateHamiltonian); IsSPTPhase sym H = short-range gapped-unique + sym H + ¬trivial. The Haldane phase is the prototypical SPT phase protected by Z₂×Z₂ (IsZ2Z2Invariant) |
Quantum/SpinS/SPTPhase.lean |
IsTimeReversalInvariant / IsBondInversionInvariant / vbsInversionParityS / tasaki_spt_classification |
§8.3.2–§8.3.3 Protecting symmetries + topological indices for SPT (Pollmann–Turner–Berg–Oshikawa; eqs. (8.3.6)–(8.3.10)): the Haldane phase is protected by any of three symmetries — (S1) Z₂×Z₂ (IsZ2Z2Invariant), (S2) time-reversal (IsTimeReversalInvariant marker), (S3) bond-centered inversion (IsBondInversionInvariant marker). vbsInversionParityS L S (marker, ℤ) + tasaki_vbs_inversion_parity (AXIOM): Û_inv|Φ_VBS^S⟩ = (−1)^{L·S}|Φ_VBS^S⟩ — odd L·S ⟹ odd parity ⟹ Z₂ obstruction to connecting to the trivial state. IsSpinSVBSNontrivialSPT S (marker) + tasaki_spt_classification (AXIOM): the spin-S VBS is a nontrivial SPT phase iff S is odd (even S ⇒ trivial). entanglementEntropyS (marker, eqs. 8.3.7–8.3.8): the bipartite entanglement entropy −Σ p_j log p_j from the Schmidt decomposition. §8.3.3 is heuristic; precise indices come in §8.3.4 (MPS) / §8.3.6 (Ogata) |
Quantum/SpinS/SPTTopologicalIndex.lean |
IsTrivialProjectiveRep / tasaki_theorem_8_7 / tasaki_corollary_8_5 |
§8.3.4 Matrix-product SPT index (Theorem 8.7 Tachikawa + Corollary 8.5; eqs. (8.3.42)–(8.3.47)): the precise MPS invariant. A protecting symmetry G acts on the bond space by a projective representation with phase function (2-cocycle) φ : G→G→ℝ (IsProjectiveRep marker); it is trivial (IsTrivialProjectiveRep marker) iff φ is a coboundary (eq. 8.3.43) — the cohomology class is the SPT index. SymmetricInjectiveMPSExists G φ (marker): an injective MPS invariant up to phase under V̂(g). tasaki_theorem_8_7 (AXIOM): symmetric injective MPS ⟹ trivial projective rep. For half-odd-integer spin (N odd), z2z2Spin_nontrivial_of_odd (AXIOM, eq. 2.1.31): the Z₂×Z₂ rep is nontrivial. tasaki_corollary_8_5 (PROVED, contrapositive of Thm 8.7): for N odd there is no Z₂×Z₂-invariant injective MPS — the matrix-product Lieb–Schultz–Mattis no-go |
Quantum/SpinS/SPTMatrixProductIndex.lean |
tasaki_theorem_8_6 |
§8.3.5 Discrete-symmetry Lieb–Schultz–Mattis theorem (Theorem 8.6, Ogata–Tasaki): the general no-go without continuous symmetry. For half-odd-integer spin (S=N/2, N odd) with a short-ranged translation-invariant Hamiltonian (HasShortRangeHamiltonianS/IsTranslationInvariantS markers) having either Z₂×Z₂ or time-reversal symmetry (IsZ2Z2SymmetricS ∨ IsTimeReversalSymmetricS), the ground state can never be both unique and gapped: tasaki_theorem_8_6 (AXIOM) ⟹ ¬HasUniqueGappedGroundStateS H. Unlike the original LSM (§6.2, continuous U(1)), this needs only a discrete symmetry; proved rigorously by Ogata–Tasaki via the Cuntz algebra / split property |
Quantum/SpinS/LiebSchultzMattisDiscrete.lean |
sptInterpolatingHamiltonianS / tasaki_theorem_8_8 |
§8.3.6 Rigorous SPT phase transition (Theorem 8.8, Tasaki 2018 index theorem; eq. (8.3.55)): the existence of a topological phase transition. sptInterpolatingHamiltonianS L s = s·akltHamiltonianS L + (1−s)·Σ_x (Ŝ_x^{(3)})² (eq. 8.3.55) linearly connects the trivial Hamiltonian (8.1.2, s=0, large-D phase) to the AKLT/VBS Hamiltonian (7.1.1, s=1, Haldane phase), keeping all three protecting symmetries. tasaki_theorem_8_8 (AXIOM): the model’s infinite-volume limit undergoes a phase transition — ∃ intermediate s∈(0,1) at which the family L↦Ĥ_s is either gapless (IsGaplessInInfiniteVolume), or has multiple ground states (HasMultipleGroundStatesInInfiniteVolume), or has a local-expectation discontinuity (HasLocalExpectationDiscontinuityInInfiniteVolume) — markers on the L↑∞ family. Proving topological phase transitions resists standard methods; Tasaki settled it via an index theorem |
Quantum/SpinS/SPTPhaseTransition.lean |
toricCodeHamiltonianS / tasaki_theorem_8_9 |
§8.4 Topological order: Kitaev’s toric code (Theorem 8.9, Bravyi–Hastings–Michalakis; eqs. (8.4.1), (8.4.19)): a gapped phase whose degeneracy is protected by topology, not symmetry. Qubits live on the edges ToricEdge L = (ZMod L × ZMod L) × Fin 2 of an L×L torus (2L² edges); starEdges/plaquetteEdges are the 4-edge stars A_v/plaquettes B_p; sigmaZS/sigmaXS = σ^z/σ^x. toricCodeHamiltonianS L = −Σ_v ∏_{A_v} σ^z − Σ_p ∏_{B_p} σ^x (eq. 8.4.1, commuting stabilizers, gap ≥ 2, 4-fold degenerate on the torus). perturbedToricHamiltonianS L ε V = Ĥ_tc + ε Σ_x V_x (eq. 8.4.19). tasaki_theorem_8_9 (AXIOM): for range-r perturbations there are L-independent ε₀,Δ>0 such that for |ε|≤ε₀, all L≥2 (nontrivial torus), and any local perturbation (IsToricPerturbation), the perturbed Hamiltonian has four near-degenerate ground states separated by Δ (HasFourNearlyDegenerateGroundStates) — topological 4-fold degeneracy stable under arbitrary perturbation, no symmetry needed. Lattice + stabilizers + both Hamiltonians concrete |
Quantum/SpinS/ToricCode.lean |
← Antiferromagnetic Heisenberg chains and the Haldane conjecture (Tasaki §6.1) · Catalogue · Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) →