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 foundations and Tasaki Chapter 2
| Lean name | Statement | File |
|—|—|—|
| magSumS_neelConfigOfS / totalSpinSOp3_mulVec_neelStateOfS | spin-S Néel state magnetization: magSumS (neelConfigOfS A N) = \|¬A\| · N, hence Ŝ_tot^(3) · \|Φ_Néel⟩ = ((\|A\| − \|¬A\|)·N/2) · \|Φ_Néel⟩. For \|A\| ≠ \|¬A\| the absolute value \|\|A\| − \|¬A\|\|·N/2 matches the conjectured Tasaki §2.5 Theorem 2.3 ground-state total spin (γ-4 step 27) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1068) |
| bipartiteImbalanceWeight / magEigenvalueS_neelConfigOfS_eq_bipartiteImbalanceWeight / neelStateOfS_mem_magSubspaceS_bipartiteImbalanceWeight / bipartiteImbalanceWeight_eq_zero_of_card_eq / bipartiteImbalanceWeight_eq_mMax_of_cardNotA_zero / bipartiteImbalanceWeight_re_nonneg_of_cardA_ge_cardNotA | bipartite imbalance weight foundation for Tasaki §2.5 Theorem 2.3 (γ-4 / \|A\| ≠ \|¬A\| case): definition bipartiteImbalanceWeight A N := (\|A\| − \|¬A\|) · N / 2 — the signed Ŝ_tot^(3) magnetization weight of the Néel orientation neelStateOfS A N. (In the \|A\| ≥ \|¬A\| orientation, this signed weight equals the predicted Theorem 2.3 total spin \|\|A\| − \|¬A\|\|·S; in the opposite orientation it is its negative.) Packages: bridge magEigenvalueS (neelConfigOfS A N) = bipartiteImbalanceWeight A N; membership neelStateOfS A N ∈ magSubspaceS Λ N (bipartiteImbalanceWeight A N); two edge cases (balanced bipartite → weight 0; saturated bipartite → weight m_max); non-negativity of the real part when \|A\| ≥ \|¬A\|. First foundational step toward formalising Theorem 2.3’s prediction at the magnetization-sector level (PR #2773, file Quantum/SpinS/NeelBipartiteWeight.lean) |
| sublatticeSpinSDot_apply_diag_neel / heisenbergToyHamiltonianS_apply_diag_neel | spin-S toy Hamiltonian Néel-state expectation value: ⟨Φ_Néel \| Ĥ_toy_S \| Φ_Néel⟩ = -\|A\|·\|¬A\|·N²/2. Negative of the all-up state eigenvalue (PR #1061), demonstrating the Néel state has strictly lower energy. Proof via PR #1055’s Ĥ_toy_S = 2 • (Ŝ_A · Ŝ_¬A) and per-pair diagonal (spinSDot x y) (neel) (neel) = m_x · m_y = -N²/4 for x ∈ A, y ∈ ¬A (γ-4 step 28) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1070) |
| heisenbergToyHamiltonian_apply_diag_neel | spin-1/2 toy Hamiltonian Néel-state expectation value: ⟨Φ_Néel \| Ĥ_toy \| Φ_Néel⟩ = -\|A\|·\|¬A\|/2. Spin-1/2 (N=1) specialisation of PR #1070; negative of the all-up state eigenvalue. Variational separation underpinning the spin-1/2 AFM ground-state argument (γ-4 step 29) | Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean (PR #1071) |
| magnetization_neelConfigOf / totalSpinHalfOp3_mulVec_neelStateOf | spin-1/2 Néel state magnetization: magnetization Λ (neelConfigOf A) = \|A\| − \|¬A\|, hence Ŝ_tot^(3) · \|Φ_Néel⟩ = ((\|A\| − \|¬A\|)/2) · \|Φ_Néel⟩. Spin-1/2 (N=1) specialisation of PR #1068 (γ-4 step 31) | Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean (PR #1073) |
| bipartiteCompleteGraphOf_preconnected | spin-S mirror of bipartiteGraphFromA_preconnected: (bipartiteCompleteGraphOf A).Preconnected when both sublattices are non-empty (any two vertices joined by a walk of length ≤ 2) (γ-4 step 32) | Quantum/SpinS/BipartiteCompleteGraph.lean (PR #1074) |
| heisenbergToyHamiltonianS_commutator_totalSpinSOp{1,2,3} / _commute_totalSpinSOp{1,2,3} | spin-S toy Hamiltonian SU(2) invariance at the axis level: [Ĥ_toy_S, Ŝ_tot^(α)] = 0 for α ∈ {1, 2, 3}, equivalently Commute Ĥ_toy_S Ŝ_tot^(α). Direct specialisation of the spin-S Heisenberg Hamiltonian SU(2) invariance to J = bipartiteCoupling A. The axis-3 form gives magnetisation-sector preservation [Ĥ_toy_S, Ŝ_tot^z] = 0 (γ-4 step 33) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1075) |
| heisenbergToyHamiltonianS_commute_totalSpinSOpPlus / _OpMinus | spin-S toy Hamiltonian commutes with the SU(2) raising/lowering ladder operators: Commute Ĥ_toy_S Ŝ^±_tot. Direct specialisation of the spin-S Heisenberg Hamiltonian ladder commutators to J = bipartiteCoupling A. Completes the full SU(2) algebra commutator set (γ-4 step 34) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1076) |
| heisenbergToyHamiltonianS_mulVec_mem_magSubspaceS | spin-S toy Hamiltonian preserves each magnetization subspace: v ∈ magSubspaceS Λ N M ⇒ (Ĥ_toy_S · v) ∈ magSubspaceS Λ N M. Direct corollary of [Ĥ_toy_S, Ŝ_tot^(3)] = 0 (PR #1075). Operator-level magnetisation conservation under toy AFM dynamics (γ-4 step 35) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1077) |
| totalSpinSSquared_commute_totalSpinSOp3 / totalSpinSSquared_mulVec_mem_magSubspaceS / sublatticeSpinSquaredS_mulVec_mem_magSubspaceS / _complement_mulVec_mem_magSubspaceS | spin-S Casimir operators preserve each magnetization subspace magSubspaceS Λ N M: (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² each commute with Ŝ_tot^(3) and so map magSubspaceS into itself. Foundation for the joint eigenbasis analysis (γ-4 step 36) | Quantum/SpinS/TotalSquared.lean, Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1078) |
| totalSpinSOpMinus_mulVec_mem_magSubspaceS_of_mem / totalSpinSOpPlus_mulVec_mem_magSubspaceS_of_mem | spin-S SU(2) raising/lowering ladder operators shift the magnetization subspace by ±1: Ŝ^∓_tot maps magSubspaceS Λ N M to magSubspaceS Λ N (M ∓ 1). Spin-S mirror of the spin-1/2 versions. Uses Cartan relations [Ŝ_tot^(3), Ŝ^∓_tot] = ∓ Ŝ^∓_tot (γ-4 step 37) | Quantum/SpinS/AllAlignedStateMagShift.lean (PR #1079) |
| heisenbergToyHamiltonian_commutator_totalSpinHalfOp{1,2,3} / _commute_totalSpinHalfOp{1,2,3} / _mulVec_mem_magnetizationSubspace_of_mem | spin-1/2 mirror back of γ-4 step 33 / 35: toy Hamiltonian SU(2) axis-α commutators + magnetisation subspace preservation. Direct specialisation of spin-1/2 Heisenberg infrastructure to J = bipartiteCoupling A (γ-4 step 38) | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean (PR #1080) |
| heisenbergToyHamiltonian_apply_im_eq_zero / heisenbergToyHamiltonianS_apply_im_zero | toy Hamiltonian matrix element realness (both spin-1/2 and spin-S): (Ĥ_toy A) σ' σ and (Ĥ_toy_S A N) σ' σ have zero imaginary part. Direct specialisation of Heisenberg-level realness lemmas to J = bipartiteCoupling A using bipartiteCoupling_im (γ-4 step 39) | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean, Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1081) |
| heisenbergHamiltonian_commute_totalSpinHalfOpPlus / _OpMinus / heisenbergToyHamiltonian_commute_totalSpinHalfOp{Plus,Minus} | spin-1/2 Heisenberg Hamiltonian and toy Hamiltonian commute with Ŝ^±_tot (Commute-form of existing commutator lemmas). Spin-1/2 mirror back of γ-4 step 34 (γ-4 step 40) | Quantum/SpinDot/HamiltonianCore.lean, Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean (PR #1082) |
| sublatticeSpinHalfSquared_mulVec_mem_magnetizationSubspace_of_mem / _complement_mulVec_mem_magnetizationSubspace_of_mem | spin-1/2 sublattice Casimir preserves each magnetisation subspace H_M. Direct corollary of sublatticeSpinHalfSquared_commute_totalSpinHalfOp3 (existing). Spin-1/2 mirror back of γ-4 step 36 (γ-4 step 41) | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean (PR #1083) |
| heisenbergHamiltonian_isSymm_of_real_symm / heisenbergHamiltonianS_isSymm_of_real / heisenbergToyHamiltonian_isSymm / heisenbergToyHamiltonianS_isSymm | matrix symmetry (IsSymm) for Heisenberg-type Hamiltonians and toy Hamiltonians (both spin-1/2 and spin-S) under real (and symmetric, where required) coupling. Direct corollary of Hermiticity plus realness of matrix entries: for a Hermitian complex matrix with real entries, conjTranspose = transpose (γ-4 step 42) | Quantum/MarshallLiebMattis/Realness.lean, Quantum/SpinS/Heisenberg.lean, Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean, Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1084) |
| sublatticeSpinSOpPlus / sublatticeSpinSOpMinus / _eq_add / _eq_sub | spin-S sublattice raising / lowering ladder operators Ŝ_A^± := Σ_{x : A x} onSiteS x (spinSOpPlus/Minus N) with definitional unfoldings Ŝ_A^± = Ŝ_A^(1) ± i Ŝ_A^(2). Foundation for sublattice-level SU(2) representation theory analysis; mirror of totalSpinSOpPlus/Minus restricted to A (γ-4 step 43) | Quantum/SpinS/SublatticeSpinLadderDefCore.lean (PR #1085) |
| totalSpinSOpPlus_eq_sublattice_sum / totalSpinSOpMinus_eq_sublattice_sum | spin-S total raising/lowering operators decompose across the bipartition: Ŝ^±_tot = Ŝ_A^± + Ŝ_¬A^±. Mirror of axis decompositions (γ-4 step 44) | Quantum/SpinS/SublatticeSpinLadderDefCore.lean (PR #1086) |
| sublatticeSpinSOpPlus_mulVec_allAlignedStateS_zero / sublatticeSpinSOpMinus_mulVec_allAlignedStateS_last | spin-S sublattice ladder operators annihilate the appropriate extremal all-aligned state: Ŝ_A^+ · \|σ_⊤⟩ = 0 and Ŝ_A^- · \|σ_⊥⟩ = 0. Direct from on-site annihilations summed over A (γ-4 step 45) | Quantum/SpinS/SublatticeSpinLadderDefCore.lean (PR #1087) |
| sublatticeSpinSOp3_commutator_sublatticeSpinSOpPlus / _OpMinus | spin-S sublattice Cartan relations [Ŝ_A^(3), Ŝ_A^±] = ±Ŝ_A^±. Derived from the sublattice SU(2) algebra (PR #1048) and Ŝ_A^± = Ŝ_A^(1) ± i Ŝ_A^(2). Mirror of totalSpinSOp3_commutator_totalSpinSOpPlus/Minus for sublattices (γ-4 step 46) | Quantum/SpinS/SublatticeSpinLadderDefCore.lean (PR #1088) |
| totalSpinSOp3_commutator_sublatticeSpinSOpPlus / _OpMinus | total Cartan relation for sublattice ladders: [Ŝ_tot^(3), Ŝ_A^±] = ±Ŝ_A^±. Combines sublattice Cartan (PR #1088) with cross-sublattice commutativity (PR #1046): [Ŝ_¬A^(3), Ŝ_A^±] = 0. Consequence: Ŝ_A^± shifts the total magnetisation by ±1 (γ-4 step 47) | Quantum/SpinS/SublatticeSpinLadderDefCore.lean (PR #1089) |
| sublatticeSpinSOpMinus_mulVec_mem_magSubspaceS_of_mem / sublatticeSpinSOpPlus_mulVec_mem_magSubspaceS_of_mem | spin-S sublattice ladder operators shift magSubspaceS by ±1: Ŝ_A^± : magSubspaceS Λ N M → magSubspaceS Λ N (M ± 1). Direct corollary of total Cartan relation (PR #1089) (γ-4 step 48) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1090) |
| sublatticeSpinSDot_self_eq_sublatticeSpinSquaredS | sublatticeSpinSDot N A A = sublatticeSpinSquaredS N A. Definitional identity unifying the cross-sublattice dot product API (Ŝ_A · Ŝ_B) with the sublattice Casimir (Ŝ_A)² for the diagonal B = A case (γ-4 step 49) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1092) |
| sublatticeSpinHalfOpPlus / sublatticeSpinHalfOpMinus / _eq_add / _eq_sub / totalSpinHalfOpPlus_eq_sublattice_sum / _OpMinus_eq_sublattice_sum | spin-1/2 sublattice ladder operators (mirror back of γ-4 steps 43, 44): Ŝ_A^± := Σ_{x : A x} onSite x spinHalfOp±, with Ŝ_A^± = Ŝ_A^(1) ± i Ŝ_A^(2) and Ŝ^±_tot = Ŝ_A^± + Ŝ_¬A^±. Brings spin-1/2 to parity with spin-S (γ-4 step 50) | Quantum/MarshallLiebMattis/SublatticeSpin.lean (PR #1093) |
| sublatticeSpinHalfOp3_commutator_sublatticeSpinHalfOpPlus / _OpMinus / totalSpinHalfOp3_commutator_sublatticeSpinHalfOpPlus / _OpMinus | spin-1/2 sublattice + total Cartan relations: [Ŝ_A^(3), Ŝ_A^±] = ±Ŝ_A^± and [Ŝ_tot^(3), Ŝ_A^±] = ±Ŝ_A^±. Mirror back of γ-4 steps 46/47 (γ-4 step 51) | Quantum/MarshallLiebMattis/SublatticeSpin.lean (PR #1094) |
| sublatticeSpinHalfOpMinus_mulVec_mem_magnetizationSubspace_of_mem / sublatticeSpinHalfOpPlus_mulVec_mem_magnetizationSubspace_of_mem | spin-1/2 sublattice ladder operators shift magnetizationSubspace by ±1: Ŝ_A^± : H_M → H_(M ± 1). Direct corollary of total Cartan (PR #1094). Mirror back of γ-4 step 48 (γ-4 step 52) | Quantum/MarshallLiebMattis/SublatticeSpinLadderPropertiesCore.lean (PR #1095) |
| sublatticeSpinHalfOpPlus_mulVec_basisVec_zero / sublatticeSpinHalfOpMinus_mulVec_basisVec_one | spin-1/2 sublattice ladder operators annihilate extremal all-up / all-down basis state: Ŝ_A^+ · \|0...0⟩ = 0 and Ŝ_A^- · \|1...1⟩ = 0. Direct from on-site annihilation summed over A. Mirror back of γ-4 step 45 (γ-4 step 53) | Quantum/MarshallLiebMattis/SublatticeSpinLadderPropertiesCore.lean (PR #1096) |
| sublatticeSpinSOpPlus_conjTranspose / _OpMinus_conjTranspose (spin-S) and sublatticeSpinHalfOpPlus_conjTranspose / _OpMinus_conjTranspose (spin-1/2) | sublattice ladder operators are Hermitian conjugates: (Ŝ_A^+)† = Ŝ_A^- and (Ŝ_A^-)† = Ŝ_A^+. Direct from spinSOpPlus_conjTranspose = spinSOpMinus summed over A. Mirror of totalSpinSOpPlus_conjTranspose for sublattices (γ-4 step 54). Also unprivates onSite_conjTranspose and onSiteS_conjTranspose helpers | Quantum/SpinS/SublatticeSpinLadder.lean, Quantum/MarshallLiebMattis/SublatticeSpinLadderPropertiesCore.lean (PR #1098) |
| sublatticeSpinSOpPlus_apply_im_zero / sublatticeSpinSOpMinus_apply_im_zero | spin-S sublattice ladder operators have real matrix elements: ((Ŝ_A^±) σ' σ).im = 0. Direct from on-site realness summed over A. Useful for downstream realness arguments (γ-4 step 57) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1101) |
| sublatticeSpinDot_self_eq_sublatticeSpinHalfSquared | spin-1/2 definitional identity: sublatticeSpinDot A A = sublatticeSpinHalfSquared A. Mirror back of γ-4 step 49 (γ-4 step 59) | Quantum/MarshallLiebMattis/SublatticeSpinDot.lean (PR #1105) |
| sublatticeSpinHalfOpPlus_apply_im_eq_zero / sublatticeSpinHalfOpMinus_apply_im_eq_zero (and on-site / single-site lemmas) | spin-1/2 sublattice ladder operators have real matrix elements. Mirror back of γ-4 step 57 (γ-4 step 60) | Quantum/MarshallLiebMattis/SublatticeSpinRealness.lean (PR #1106) |
| sublatticeSpinSOp{1,2,3}_sq_eq_conjTranspose_mul (and the spin-1/2 axis-3 mirror sublatticeSpinHalfOp3_sq_eq_conjTranspose_mul) | sublattice axis operators squared equal (Ŝ_A^(α))ᴴ * Ŝ_A^(α). Direct from Hermiticity. The operator identity underlying PSD: Aᴴ A is PSD for any A. Useful for setting up positivity arguments without Matrix.PosSemidef (γ-4 step 61) | Quantum/SpinS/SublatticeSpinLadderDef.lean, Quantum/MarshallLiebMattis/SublatticeSpinRealnessCore.lean (PR #1107) |
| sublatticeSpinSOp1_apply_im_zero / sublatticeSpinSOp3_apply_im_zero | spin-S sublattice axis-1 and axis-3 operators have real matrix elements. Direct from onSiteS_spinSOp{1,3}_apply_im_zero summed over A (γ-4 step 62) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1108) |
| sublatticeSpinHalfOp1_apply_im_eq_zero / sublatticeSpinHalfOp3_apply_im_eq_zero (and on-site / single-site) | spin-1/2 sublattice axis-1 / axis-3 operators have real matrix elements. Mirror back of γ-4 step 62 (γ-4 step 63) | Quantum/MarshallLiebMattis/SublatticeSpinRealnessCore.lean (PR #1109) |
| sublatticeSpinSOpPlus_mulVec_basisVecS_zero_on / sublatticeSpinSOpMinus_mulVec_basisVecS_last_on | spin-S sublattice ladder operators annihilate basis states with extreme A-values: Ŝ_A^+ · \|σ⟩ = 0 if σ|A = 0; Ŝ_A^- · \|σ⟩ = 0 if σ|_A = Fin.last N. Generalises PR #1087 to allow arbitrary σ on ¬A (γ-4 step 64) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1110) |
| sublatticeSpinSOpPlus_mulVec_neelStateOfS / sublatticeSpinSOpMinus_complement_mulVec_neelStateOfS | spin-S Néel state annihilated by sublattice ladders: Ŝ_A^+ · \|Φ_Néel⟩ = 0 (highest weight on A) and Ŝ_¬A^- · \|Φ_Néel⟩ = 0 (lowest weight on ¬A). The Néel state is highest-weight on A and lowest-weight on ¬A, consistent with maximum-spin irreps on each sublattice (γ-4 step 65) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1111) |
| sublatticeSpinHalfOpPlus_mulVec_basisVec_zero_on / sublatticeSpinHalfOpMinus_mulVec_basisVec_one_on / sublatticeSpinHalfOpPlus_mulVec_neelStateOf / sublatticeSpinHalfOpMinus_complement_mulVec_neelStateOf | spin-1/2 mirror back of γ-4 steps 64/65 (γ-4 step 66) | Quantum/MarshallLiebMattis/SublatticeSpinLadderPropertiesCore.lean, Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1112) |
| totalSpinSOpPlus_mulVec_neelStateOfS_eq_complement / totalSpinSOpMinus_mulVec_neelStateOfS_eq_A | spin-S total ladder on Néel reduces to opposite-sublattice ladder via annihilation: Ŝ_tot^+ · \|Φ_Néel⟩ = Ŝ_¬A^+ · \|Φ_Néel⟩ and Ŝ_tot^- · \|Φ_Néel⟩ = Ŝ_A^- · \|Φ_Néel⟩. Direct corollary of decomposition + annihilation (γ-4 step 67) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1113) |
| totalSpinHalfOpPlus_mulVec_neelStateOf_eq_complement / totalSpinHalfOpMinus_mulVec_neelStateOf_eq_A | spin-1/2 mirror of γ-4 step 67 (γ-4 step 68) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1114) |
| spinSDot_apply_diag_neelConfigOfS_of_cross | spin-S per-pair Ŝ_x · Ŝ_y diagonal at the Néel configuration: for x ∈ A, y ∈ ¬A, (Ŝ_x · Ŝ_y) (neel) (neel) = -N²/4. Direct from spinSDot_apply_diag_of_ne with m_x = N/2, m_y = -N/2 (γ-4 step 69) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1115) |
| spinHalfDot_apply_diag_neelConfigOf_of_cross (and unprivates spinHalfDot_apply_diag_of_ne_antiparallel) | spin-1/2 per-pair Ŝ_x · Ŝ_y diagonal at the Néel configuration: for x ∈ A, y ∈ ¬A, (Ŝ_x · Ŝ_y) (neel) (neel) = -1/4. Mirror of γ-4 step 69 (γ-4 step 70) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean (PR #1116) |
| neelConfigOfS_complement | spin-S Néel config under sublattice swap: neelConfigOfS (¬A) N x = if A x then Fin.last N else 0. The natural sublattice-swap dual (γ-4 step 71) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1117) |
| neelConfigOf_complement | spin-1/2 mirror of γ-4 step 71: neelConfigOf (¬A) x = if A x then 1 else 0 (γ-4 step 72) | Quantum/NeelState/Definition.lean (PR #1118) |
| sublatticeSpinSOp3_mulVec_neelStateOfS | Ŝ_A^(3) · \|Φ_Néel⟩ = (\|A\|·N/2) · \|Φ_Néel⟩. Sublattice z-axis acts as |A|·N/2 on Néel state (highest weight on A) (γ-4 step 73) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1119) |
| sublatticeSpinSOp3_complement_mulVec_neelStateOfS | Ŝ_¬A^(3) · \|Φ_Néel⟩ = -(\|¬A\|·N/2) · \|Φ_Néel⟩. Complement sublattice z-axis acts as -|¬A|·N/2 on Néel state (lowest weight on ¬A) (γ-4 step 74) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1120) |
| sublatticeSpinHalfOp3_mulVec_neelStateOf | spin-1/2 mirror of γ-4 step 73: Ŝ_A^(3) · \|Φ_Néel⟩ = (\|A\|/2) · \|Φ_Néel⟩ (γ-4 step 75) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1121) |
| sublatticeSpinHalfOp3_complement_mulVec_neelStateOf | spin-1/2 mirror of γ-4 step 74: Ŝ_¬A^(3) · \|Φ_Néel⟩ = -(\|¬A\|/2) · \|Φ_Néel⟩ (γ-4 step 76) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1122) |
| sublatticeSpinSOp3_sq_mulVec_neelStateOfS / sublatticeSpinSOp3_complement_sq_mulVec_neelStateOfS | (Ŝ_A^(3))² · \|Φ_Néel⟩ = (\|A\|·N/2)² · \|Φ_Néel⟩ and complement: squares of γ-4 steps 73/74 (γ-4 step 77) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1123) |
| sublatticeSpinHalfOp3_sq_mulVec_neelStateOf / sublatticeSpinHalfOp3_complement_sq_mulVec_neelStateOf | spin-1/2 mirror of γ-4 step 77: (Ŝ_A^(3))² · \|Φ_Néel⟩ = (\|A\|/2)² · \|Φ_Néel⟩ and complement (γ-4 step 78) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1124) |
| sublatticeSpinSOp3_cross_complement_mulVec_neelStateOfS | Ŝ_A^(3)·Ŝ_¬A^(3) · \|Φ_Néel⟩ = -\|A\|·\|¬A\|·(N/2)² · \|Φ_Néel⟩. Cross-sublattice product of γ-4 steps 73/74 (γ-4 step 79) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1126) |
| sublatticeSpinHalfOp3_cross_complement_mulVec_neelStateOf | spin-1/2 mirror of γ-4 step 79: Ŝ_A^(3)·Ŝ_¬A^(3) · \|Φ_Néel⟩ = -\|A\|·\|¬A\|/4 · \|Φ_Néel⟩ (γ-4 step 80) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1127) |
| sublatticeSpinSOpPlus_complement_minus_mulVec_neelStateOfS | Ŝ_A^+·Ŝ_¬A^- · \|Φ_Néel⟩ = 0. Cross-ladder annihilation of Néel via Ŝ¬A^- (γ-4 step 81) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1128) |
| sublatticeSpinSOpMinus_complement_minus_mulVec_neelStateOfS | Ŝ_A^-·Ŝ_¬A^- · \|Φ_Néel⟩ = 0. Cross-ladder lowering annihilation via Ŝ_¬A^- (γ-4 step 83) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1130) |
| sublatticeSpinSOpComplementPlus_plus_mulVec_neelStateOfS | Ŝ_¬A^+·Ŝ_A^+ · \|Φ_Néel⟩ = 0. Cross-ladder raising annihilation via Ŝ_A^+ (γ-4 step 85) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1132) |
| sublatticeSpinSOpPlus_cross_commute / sublatticeSpinSOpMinus_cross_commute / sublatticeSpinSOpPlus_cross_commute_minus / sublatticeSpinSOpMinus_cross_commute_plus | spin-S cross-sublattice commute for ladder operators: Ŝ_A^± commutes with Ŝ_¬A^± (all 4 sign combinations). Direct from sublatticeSpinSOpGeneric_cross_commute (γ-4 step 87) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1134) |
| sublatticeSpinHalfOpPlus_cross_commute / sublatticeSpinHalfOpMinus_cross_commute / sublatticeSpinHalfOpPlus_cross_commute_minus / sublatticeSpinHalfOpMinus_cross_commute_plus | spin-1/2 mirror of γ-4 step 87 (γ-4 step 88) | Quantum/MarshallLiebMattis/SublatticeSpinLadderProperties.lean (PR #1135) |
| sublatticeSpinSOpPlus_complement_plus_mulVec_neelStateOfS | Ŝ_A^+·Ŝ_¬A^+ · \|Φ_Néel⟩ = 0 via cross-commute and Ŝ_A^+ annihilation (γ-4 step 89) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1136) |
| sublatticeSpinSOpComplementMinus_plus_mulVec_neelStateOfS | Ŝ_¬A^-·Ŝ_A^+ · \|Φ_Néel⟩ = 0 via Ŝ_A^+ annihilation (γ-4 step 91) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1138) |
| sublatticeSpinSOpMinus_plus_mulVec_neelStateOfS / sublatticeSpinSOpComplementPlus_minus_mulVec_neelStateOfS | same-sublattice annihilations: Ŝ_A^-·Ŝ_A^+ · \|Φ_Néel⟩ = 0 and Ŝ_¬A^+·Ŝ_¬A^- · \|Φ_Néel⟩ = 0 (γ-4 step 93) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1140) |
| sublatticeSpinSOp12sq_mulVec_neelStateOfS | ((Ŝ_A^(1))² + (Ŝ_A^(2))²) · \|Φ_Néel⟩ = (\|A\|·N/2) · \|Φ_Néel⟩. Casimir minus z-axis squared on Néel (γ-4 step 95) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1142) |
| sublatticeSpinSOp12sq_complement_mulVec_neelStateOfS | ((Ŝ_¬A^(1))² + (Ŝ_¬A^(2))²) · \|Φ_Néel⟩ = (\|¬A\|·N/2) · \|Φ_Néel⟩. Complement of γ-4 step 95 (γ-4 step 97) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1144) |
| sublatticeSpinSOpPlus_mul_sublatticeSpinSOpMinus_eq | sublattice Cartan identity: Ŝ_A^+·Ŝ_A^- = (Ŝ_A^(1))² + (Ŝ_A^(2))² + Ŝ_A^(3) (γ-4 step 99) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1146) |
| sublatticeSpinSOpPlus_minus_mulVec_neelStateOfS | Ŝ_A^+·Ŝ_A^- · \|Φ_Néel⟩ = \|A\|·N · \|Φ_Néel⟩. Highest-weight Casimir formula 2s = |A|·N for s = |A|·N/2 (γ-4 step 100) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1147) |
| sublatticeSpinHalfOpPlus_mul_sublatticeSpinHalfOpMinus_eq | spin-1/2 mirror of γ-4 step 99: sublattice Cartan identity (γ-4 step 101) | Quantum/MarshallLiebMattis/SublatticeSpinLadderProperties.lean (PR #1148) |
| sublatticeSpinSOpMinus_mul_sublatticeSpinSOpPlus_eq | dual sublattice Cartan identity: Ŝ_A^-·Ŝ_A^+ = (Ŝ_A^(1))² + (Ŝ_A^(2))² - Ŝ_A^(3) (γ-4 step 103) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1150) |
| sublatticeSpinSOpComplementMinus_complement_plus_mulVec_neelStateOfS | Ŝ_¬A^-·Ŝ_¬A^+ · \|Φ_Néel⟩ = \|¬A\|·N · \|Φ_Néel⟩. Lowest-weight Casimir formula 2s = |¬A|·N for s = |¬A|·N/2 (γ-4 step 104) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1151) |
| sublatticeSpinHalfOpMinus_mul_sublatticeSpinHalfOpPlus_eq / sublatticeSpinHalfOpComplementMinus_complement_plus_mulVec_neelStateOf | spin-1/2 mirrors of γ-4 steps 103/104: dual Cartan and Ŝ_¬A^-·Ŝ_¬A^+ · \|Φ_Néel⟩ = \|¬A\| · \|Φ_Néel⟩ (γ-4 step 105) | Quantum/MarshallLiebMattis/SublatticeSpinLadderProperties.lean (the surviving lemma moved here when this file was split out of Quantum/MarshallLiebMattis/SublatticeSpin.lean in refactor #44, PR #2940) (its companion sublatticeSpinHalfOpComplementMinus_complement_plus_mulVec_neelStateOf lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelExpectations.lean, moved there when refactor #53, PR #3128 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1152) |
| sublatticeSpinSOpPlus_commutator_sublatticeSpinSOpMinus | sublattice Cartan commutator: [Ŝ_A^+, Ŝ_A^-] = 2 · Ŝ_A^(3) (γ-4 step 106) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1153) |
| sublatticeSpinHalfOpPlus_commutator_sublatticeSpinHalfOpMinus | spin-1/2 mirror of γ-4 step 106: [Ŝ_A^+, Ŝ_A^-] = 2 · Ŝ_A^(3) (γ-4 step 107) | Quantum/MarshallLiebMattis/SublatticeSpinLadderProperties.lean (PR #1154) |
| neelStateOfS_ne_zero | spin-S Néel state is non-zero (γ-4 step 108) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1155) |
| neelStateOf_ne_zero | spin-1/2 Néel state is non-zero (γ-4 step 109) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1156) |
| neelStateOfS_inner_self | spin-S Néel state has norm-squared 1: <Φ_Néel \| Φ_Néel> = 1 (γ-4 step 110) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1157) |
| neelStateOf_inner_self | spin-1/2 Néel state norm-squared = 1 (γ-4 step 111) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1158) |
| neelStateOfS_totalSpinSOp3_expectation | <Φ_Néel \| Ŝ_tot^(3) \| Φ_Néel> = (\|A\| - \|¬A\|)·N/2 (γ-4 step 112) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1159) |
| neelStateOfS_sublattice_minus_plus_cross_expectation | <Φ_Néel \| Ŝ_A^- · Ŝ_¬A^+ \| Φ_Néel> = 0. The cross-flip expectation vanishes by Hermitian conjugate of Ŝ_A^+ annihilation (γ-4 step 114) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1161) |
| neelStateOfS_sublattice3_cross_complement3_expectation | <Φ_Néel \| Ŝ_A^(3)·Ŝ_¬A^(3) \| Φ_Néel> = -\|A\|·\|¬A\|·(N/2)² (γ-4 step 116) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1163) |
| neelStateOfS_sublattice_plus_complement_minus_expectation | <Φ_Néel \| Ŝ_A^+·Ŝ_¬A^- \| Φ_Néel> = 0. Trivial via Ŝ_¬A^- annihilation (γ-4 step 118) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1165) |
| neelStateOfS_sublattice_plus_complement_plus_expectation / neelStateOfS_sublattice_minus_complement_minus_expectation | <Φ_Néel \| Ŝ_A^+·Ŝ_¬A^+ \| Φ_Néel> = 0 and <Φ_Néel \| Ŝ_A^-·Ŝ_¬A^- \| Φ_Néel> = 0 (γ-4 step 120) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1167) |
| sublatticeSpinSOp1_mul_op1_add_op2_mul_op2_eq_ladder | cross-axis identity: Ŝ_A^(1)·Ŝ_B^(1) + Ŝ_A^(2)·Ŝ_B^(2) = (1/2)(Ŝ_A^+·Ŝ_B^- + Ŝ_A^-·Ŝ_B^+) (γ-4 step 122) | Quantum/SpinS/SublatticeSpinLadder.lean (PR #1169) |
| sublatticeSpinHalfOp1_mul_op1_add_op2_mul_op2_eq_ladder | spin-1/2 mirror of γ-4 step 122 (γ-4 step 123) | Quantum/MarshallLiebMattis/SublatticeSpinLadderProperties.lean (PR #1170) |
| neelStateOfS_sublatticeSpinSDot_expectation | <Φ_Néel \| Ŝ_A · Ŝ_¬A \| Φ_Néel> = -\|A\|·\|¬A\|·(N/2)². Cross-sublattice spin dot product expectation (γ-4 step 124) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1171) |
| neelStateOfS_totalSpinSSquared_expectation | <Φ_Néel \| (Ŝ_tot)² \| Φ_Néel> = ((\|A\|-\|¬A\|)·N/2)² + (\|A\|+\|¬A\|)·N/2. Full total-spin Casimir expectation (γ-4 step 126) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1173) |
| totalSpinSOp3_sq_mulVec_neelStateOfS | (Ŝ_tot^(3))² · \|Φ_Néel⟩ = ((\|A\|-\|¬A\|)·N/2)² · \|Φ_Néel⟩. Néel is exact (Ŝ_tot^(3))²-eigenvector (γ-4 step 128) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1175) |
| neelStateOfS_totalSpinSSquared_expectation_card_Lambda / neelStateOf_totalSpinHalfSquared_expectation_card_Lambda | reformulation: <Φ_Néel \| (Ŝ_tot)² \| Φ_Néel> = ((\|A\|-\|¬A\|)·N/2)² + \|Λ\|·N/2 (spin-S) and ((\|A\|-\|¬A\|)/2)² + \|Λ\|/2 (spin-1/2) (γ-4 step 130) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelExpectations.lean, moved there when refactor #53, PR #3128 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1177) |
| neelStateOfS_heisenbergToyHamiltonianS_expectation / neelStateOf_heisenbergToyHamiltonian_expectation | <Φ_Néel \| Ĥ_toy \| Φ_Néel> = -\|A\|·\|¬A\|·N²/2 (spin-S) and -\|A\|·\|¬A\|/2 (spin-1/2). Toy-Hamiltonian expectation, equals diagonal element since Néel is a basis vector (γ-4 step 131) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelExpectations.lean, moved there when refactor #53, PR #3128 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1178) |
| basisVecS_expectation_eq_diagonal / basisVec_expectation_eq_diagonal | generic basis-vector expectation = diagonal entry: <σ \| M \| σ> = M σ σ for any matrix M (γ-4 step 132) | Quantum/SpinS/MultiSite.lean and Quantum/ManyBody.lean (PR #1179) |
| neelStateOf_allUp_orthogonal | spin-1/2 mirror: <basisVec (fun _ => 0) \| Φ_Néel> = 0 when \|¬A\| > 0 (γ-4 step 134) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1181) |
| neelMagConfigS | Néel configuration packaged as magConfigS Λ N (\|¬A\|·N). Witness for the magnetization-(\|A\|-\|¬A\|)·N/2 sector (γ-4 step 135) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1182) |
| neelMagConfigS_nonempty | typeclass instance: Nonempty (magConfigS Λ N (\|¬A\|·N)) via neelMagConfigS (γ-4 step 136) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1183) |
| h_intermediate_imp_conditions | migration bridge (Issue #4569): the old h_intermediate hypothesis implies (∃a, A a=true) ∧ (∃b, A b=false) ∧ 1≤N for [Nonempty V], connecting the deprecated h_intermediate-based API to the canonical hA_ne/hB_ne/hN API of the §2.3/§2.4 PF lemmas | Quantum/SpinS/MagConfig.lean (PR #4577) |
| neelConfigOfS_ne_allAlignedConfigS | config-level distinctness: neelConfigOfS A N ≠ allAlignedConfigS Λ N 0 when \|¬A\| > 0 and N > 0 (γ-4 step 144) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1191) |
| allAlignedStateS_last_heisenbergToyHamiltonianS_expectation | <Φ_⊥ \| Ĥ_toy_S \| Φ_⊥> = +\|A\|·\|¬A\|·N²/2. All-down: same eigenvalue as all-up by symmetry (γ-4 step 148) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1195) |
| neelConfigOfS_ne_allAlignedConfigS_last | distinctness: neelConfigOfS A N ≠ allAlignedConfigS Λ N (Fin.last N) when \|A\| > 0 and N > 0 (γ-4 step 152) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1199) |
| neelStateOfS_totalSpinSOp3_sq_expectation / neelStateOf_totalSpinHalfOp3_sq_expectation | <Φ_Néel \| (Ŝ_tot^(3))² \| Φ_Néel> = M² for both spin-S and spin-1/2 (γ-4 step 155) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelExpectations.lean, moved there when refactor #53, PR #3128 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1202) |
| bipartiteCoupling_sum and neelState{OfS,Of}_heisenbergToyHamiltonian{S,}_expectation_via_cross_only | Total bipartite-coupling pair count Σ_{x,y} bipartiteCoupling A x y = 2·\|A\|·\|¬A\|, and toy Hamiltonian Néel expectation via cross-only: chains γ-4 step 164 with the bipartite sum to re-derive <Φ_Néel \| Ĥ_toy \| Φ_Néel> = -\|A\|·\|¬A\|·N²/2 (spin-S) / -\|A\|·\|¬A\|/2 (spin-1/2) by an independent route through the per-pair correlation trio (γ-4 step 165) | Quantum/MarshallLiebMattis/ToyHamiltonian.lean, Quantum/SpinS/SublatticeCasimirNeel.lean, Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1212) |
| LatticeSystem.Lattice.couplingOf_sum and neelState{OfS,Of}_heisenbergHamiltonianOnGraph{S,}_expectation_of_bipartite_closed | Closed-form Heisenberg-on-graph Néel expectation: Σ_{x,y} couplingOf G J x y = J · 2 · #G.edgeFinset (via degree-sum formula); chained with γ-4 step 166, gives <Φ_Néel \| H_G \| Φ_Néel> = -J · #G.edgeFinset · N²/2 (spin-S) / -J · #G.edgeFinset / 2 (spin-1/2) under bipartite alignment. The variational upper bound on the AFM Heisenberg ground-state energy when J > 0 (γ-4 step 167) | LatticeSystem/Lattice/Graph.lean, Quantum/SpinS/SublatticeCasimirNeel.lean, Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1214) |
← Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) · Catalogue · Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) →