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 |
|—|—|—|
| marshallCubicState / _neelCubicConfig | 3D cubic Marshall-rotated checkerboard state; coincides with neelCubicState K L M at the Néel configuration | Quantum/NeelState/MarshallSign.lean |
| marshallSign{Chain,Square,Cubic}Config_flipConfig_neel{Chain,Square,Cubic}Config | Marshall sign on the flipped Néel configuration: (-1)^K (1D), +1 (2D), +1 (3D) — direct compositions of _flipConfig and _neelChainConfig | Quantum/NeelState.lean |
| marshall{Chain,Square,Cubic}State_flipConfig_eq_timeReversalSpinHalfMulti | the Marshall-rotated flipped Néel state coincides with the time-reversed Néel state in 1D, 2D, 3D — both sides equal the same explicit (-1)^K (1D) or +1 (2D, 3D) scaled basis vector. Establishes a direct bridge between the Marshall basis change (Tasaki §2.5 / Marshall-Lieb-Mattis) and the time-reversal operator (Tasaki §2.3) on the Néel ground-state ansatz | Quantum/NeelState.lean |
| marshallDressedBasis A σ | Marshall-dressed standard basis state := marshallSignOf A σ • basisVec σ on a generic finite vertex type V with sublattice indicator A : V → Bool (Tasaki §2.5 eq. (2.5.8), p. 41). The dressing produces a basis in which the spin-1/2 antiferromagnetic Heisenberg Hamiltonian on a connected bipartite graph has all off-diagonal matrix elements ≤ 0 (Marshall sign trick), the input to the Perron–Frobenius proof of the MLM theorem | Quantum/MarshallDressedBasis.lean |
| marshallDressedBasis_self / _of_ne / _apply | pointwise rules: Ψ̃^σ σ = marshallSignOf A σ; Ψ̃^σ τ = 0 for τ ≠ σ; explicit Ψ̃^σ τ = marshallSignOf A σ · basisVec σ τ | Quantum/MarshallDressedBasis.lean |
| marshallSignOf_sq_eq_one | each factor of marshallSignOf is ±1, so the sign squares to 1: (marshallSignOf A σ)² = 1 | Quantum/MarshallDressedBasis.lean |
| marshallDressedBasis_inner | orthonormality of the Marshall-dressed basis under the real bilinear pairing: Σ_τ Ψ̃^σ τ · Ψ̃^ρ τ = if ρ = σ then 1 else 0 (combines basisVec_inner with marshallSignOf_sq_eq_one) | Quantum/MarshallDressedBasis.lean |
| marshallDressedBasis_mem_magnetizationSubspace / _zero | the dressed basis state lies in the same magnetisation-M subspace H_M = H_{σ̄/2} as the underlying basisVec σ (Tasaki eq. (2.2.10)); the _zero specialisation places it in H_0 when Σ_x σ_x = 0 | Quantum/MarshallDressedBasis.lean |
| spinHalfDot_apply_im_eq_zero | every matrix entry of the two-site spin product Ŝ_x · Ŝ_y is real: ((spinHalfDot x y) σ σ').im = 0 for all x, y, σ, σ'. Case analysis on x = y / parallel / antiparallel via the existing spinHalfDot_mulVec_basisVec_{parallel,antiparallel} action lemmas. Property (i) ingredient for the Marshall–Lieb–Mattis theorem (Tasaki §2.5, p. 41) | Quantum/MarshallLiebMattis/Realness.lean |
| heisenbergHamiltonian_apply_im_eq_zero | for real coupling J : Λ → Λ → ℂ ((J x y).im = 0 for all x, y), every matrix entry of the Heisenberg Hamiltonian H = Σ_{x,y} J(x,y) · spinHalfDot x y is real: ((heisenbergHamiltonian J) σ σ').im = 0. ℝ-linearity + spinHalfDot_apply_im_eq_zero | Quantum/MarshallLiebMattis/Realness.lean |
| marshallSignOf_im_eq_zero | the Marshall sign marshallSignOf A σ is real: (marshallSignOf A σ).im = 0. Each factor of the product is ±1 ∈ ℝ (either 1 or (-1 : ℂ)^(σ x : ℕ) with (σ x : ℕ) ∈ {0, 1}); products of reals are real | Quantum/MarshallLiebMattis/Realness.lean |
| dot_marshallDressed_heisenbergHamiltonian_marshallDressed_im_eq_zero | MLM Property (i): for real coupling J, the dressed Heisenberg bilinear pairing Σ_τ \|Ψ̃^σ⟩ τ · (H · \|Ψ̃^{σ'}⟩) τ is real (Tasaki §2.5, p. 41 in the proof of Theorem 2.2). Reduces to marshallSignOf A σ · marshallSignOf A σ' · H σ σ' (each factor real) | Quantum/MarshallLiebMattis/Realness.lean |
| dot_marshallDressed_mulVec_marshallDressed_eq | for any operator M, the dressed bilinear pairing factorises: Σ_τ \|Ψ̃^σ⟩ τ · (M · \|Ψ̃^{σ'}⟩) τ = marshallSignOf A σ · marshallSignOf A σ' · M σ σ'. Generalises the inner-product computation used in Property (i) | Quantum/MarshallLiebMattis/MarshallSignTrick.lean |
| marshallSignOf_mul_marshallSignOf_basisSwap_of_bipartite_antiparallel | Marshall sign relation: for a bond {x, y} crossing the bipartition (A x ≠ A y) with σ antiparallel at {x, y} (σ x ≠ σ y), marshallSignOf A σ * marshallSignOf A (basisSwap σ x y) = -1. The combined product over Λ of pairwise factors collapses: outside {x, y} each pairwise factor is (±1)² = 1; at the unique site in A ∩ {x, y} the pair contributes (-1)^(σ x + σ y) = -1 since σ x ≠ σ y; the other site of {x, y} lies outside A and contributes 1 | Quantum/MarshallLiebMattis/MarshallSignTrick.lean |
| bond_dressed_contribution_re_nonpos | per-bond non-positivity: for σ ≠ σ' and any bond (x, y) with real non-negative J(x, y) supported on bipartite bonds, the contribution marshallSignOf A σ · marshallSignOf A σ' · J(x,y) · (spinHalfDot x y) σ σ' to the dressed off-diagonal element has non-positive real part. Case analysis on (spinHalfDot x y) σ σ' (zero off-diagonal except at σ = basisSwap σ' x y, antiparallel σ’, x ≠ y) combined with the Marshall sign relation | Quantum/MarshallLiebMattis/MarshallSignTrick.lean |
| dot_marshallDressed_heisenbergHamiltonian_marshallDressed_re_nonpos_of_ne | MLM Property (ii) (Tasaki §2.5, p. 41): for real non-negative J supported on bipartite bonds and σ ≠ σ', the dressed off-diagonal Heisenberg pairing Σ_τ \|Ψ̃^σ⟩ τ · (H · \|Ψ̃^{σ'}⟩) τ has non-positive real part. Sum bond-by-bond using bond_dressed_contribution_re_nonpos. The Marshall sign trick at the heart of the Marshall–Lieb–Mattis Theorem 2.2 proof | Quantum/MarshallLiebMattis/MarshallSignTrick.lean |
| SwapStep, SwapReachable | one-step swap relation σ ↦ basisSwap σ x y along a graph edge (x, y) with σ x ≠ σ y; reflexive transitive closure for multi-step reachability | Quantum/MarshallLiebMattis/Connectivity.lean |
| swapReachable_of_walk_of_ne | for any G-walk from x to y and σ x ≠ σ y, SwapReachable G σ (basisSwap σ x y). Walk induction with case analysis on σ z at intermediate vertex (Tasaki p. 41 “Proof of Property (iii)” Lemma) | Quantum/MarshallLiebMattis/Connectivity.lean |
| swapReachable_of_{reachable,preconnected}_of_ne | for any x, y reachable in G (or any x, y if G preconnected) with σ x ≠ σ y, the swap is reachable. MLM Property (iii) ingredient (Tasaki §2.5 p. 41) — combined with iteration over the magnetisation-difference, gives Perron–Frobenius irreducibility on H_M | Quantum/MarshallLiebMattis/Connectivity.lean |
| H₀Index Λ | index type {σ : Λ → Fin 2 // magnetization Λ σ = 0} for the zero-magnetisation subspace H_0; Fintype and DecidableEq instances | Quantum/MarshallLiebMattis/H0Matrix.lean |
| dressedHeisenbergMatrixH0 | real-valued matrix on H₀Index Λ with entries Re (marshallSignOf A σ · marshallSignOf A τ · (H_J)_{σ,τ}) — the matrix to which Tasaki’s Perron–Frobenius proof of MLM applies | Quantum/MarshallLiebMattis/H0Matrix.lean |
| dressedHeisenbergMatrixH0_isSymm | the matrix is symmetric for real symmetric J (Hermiticity of Heisenberg + realness of entries) | Quantum/MarshallLiebMattis/H0Matrix.lean |
| dressedHeisenbergMatrixH0_offdiag_nonpos | off-diagonal entries are non-positive for real non-negative bipartite J and distinct σ ≠ τ, packaged from PR α-3’s Property (ii) via dot_marshallDressed_mulVec_marshallDressed_eq | Quantum/MarshallLiebMattis/H0Matrix.lean |
| magnetization_basisSwap | basisSwap σ x y preserves total magnetisation. Proof uses the identification basisSwap σ x y = σ ∘ Equiv.swap x y (the swap is a permutation of Λ); the magnetisation ∑_z spinSign(σ z) is invariant under such reindexing (Equiv.sum_comp). Key ingredient for Tasaki §2.5 p. 42 Proposition (equal-magnetisation reachability) | Quantum/MarshallLiebMattis/EqMagnetization.lean |
| disagreementSet / configDist | the set / count of sites where σ and σ' disagree; configDist_eq_zero_iff characterises configuration equality | Quantum/MarshallLiebMattis/EqMagnetizationReachable.lean |
| exists_swap_pair_of_eq_magnetization | for σ ≠ σ' with equal magnetisation, there exist sites x (with σ x = 0, σ' x = 1) and y (with σ y = 1, σ' y = 0). Pigeonhole/cardinality argument: the (0, 1)-disagreement and (1, 0)-disagreement sets have equal cardinality from magnetisation equality, and the disagreement set is non-empty for σ ≠ σ' | Quantum/MarshallLiebMattis/EqMagnetizationReachable.lean |
| configDist_basisSwap_lt | swapping at sites x ∈ D01, y ∈ D10 strictly decreases the configuration distance to σ'. The disagreement set strictly shrinks (x newly agrees with σ' after swap) | Quantum/MarshallLiebMattis/EqMagnetizationReachable.lean |
| swapReachable_of_eq_magnetization | Tasaki §2.5 p. 42 Proposition: any two configurations σ, σ' with the same total magnetisation are connected by a chain of single-edge bond swaps, on a connected graph. Strong induction on configDist, reducing by ≥ 2 per step via the swap pair from exists_swap_pair_of_eq_magnetization. Final ingredient for Perron–Frobenius irreducibility on H_M | Quantum/MarshallLiebMattis/EqMagnetizationReachable.lean |
| dressedHeisenbergShifted | the shifted matrix B := c·I − M on H₀Index Λ. Used as input to Perron–Frobenius: B is symmetric, has non-negative off-diagonal (sign flip of M’s non-positive off-diagonal), and non-negative diagonal when c ≥ M σ σ for all σ. The maximum eigenvalue of B corresponds to the minimum eigenvalue of M (the H_0 ground state of the AFM Heisenberg) | Quantum/MarshallLiebMattis/H0Shifted.lean |
| dressedHeisenbergShifted_isSymm / _nonneg (_offdiag_nonneg, _diag_nonneg) | symmetry and (off-diagonal / full) non-negativity of B under the appropriate hypotheses on J and c | Quantum/MarshallLiebMattis/H0Shifted.lean |
| spinHalfDot_apply_basisSwap | the off-diagonal matrix entry (spinHalfDot x y) σ (basisSwap σ x y) = 1/2 for x ≠ y and antiparallel σ_x ≠ σ_y. Building block for the explicit Heisenberg matrix entry on swap-related configurations needed for Perron–Frobenius irreducibility | Quantum/MarshallLiebMattis/SpinDotSwapEntry.lean |
| basisSwap_basisSwap_ne_self_of_ne_bond | combinatorial helper: for x ≠ y, σ_x ≠ σ_y, and (u, v) ∉ {(x, y), (y, x)}, the configuration basisSwap (basisSwap σ x y) u v ≠ σ. Site analysis: σ and σ' = basisSwap σ x y differ at exactly {x, y}, so for the iterated swap to return to σ, the swap sites {u, v} must coincide with {x, y}. Used for off-bond vanishing in the Heisenberg matrix entry computation | Quantum/MarshallLiebMattis/HeisenbergSwapEntry.lean |
| spinHalfDot_apply_basisSwap_off_bond_eq_zero | for σ' = basisSwap σ x y (with x ≠ y, σ_x ≠ σ_y) and any (u, v) ∉ {(x, y), (y, x)}, the matrix entry (spinHalfDot u v) σ σ' = 0. Three cases: u = v (diagonal), u ≠ v parallel σ’ (constant action), u ≠ v antiparallel + off-bond (combinatorial helper) | Quantum/MarshallLiebMattis/SpinDotOffBond.lean |
| heisenbergHamiltonian_apply_basisSwap | the Heisenberg matrix entry on swap-related configurations: (heisenbergHamiltonian J) σ (basisSwap σ x y) = (J x y + J y x) / 2. Decomposes the double sum and uses α-5e (active bond = 1/2) + α-5g (off-bond = 0). For symmetric J, simplifies to J x y | Quantum/MarshallLiebMattis/HeisenbergSwapValue.lean |
| dressed_pairing_basisSwap_eq / dressedHeisenbergMatrixH0_apply_basisSwap | the dressed Heisenberg matrix entry on swap-related H_0 configurations: complex-level value -J(x, y) (Marshall sign trick × Heisenberg formula × symmetric J), real-part value -(J x y).re. Combined with J(x, y).re > 0 on graph edges gives strict negativity of M off-diagonal at swap pairs, hence strict positivity of B = c·I − M — the input for Perron–Frobenius irreducibility | Quantum/MarshallLiebMattis/DressedSwapValue.lean |
| dressedHeisenbergShifted_pos_of_basisSwap | strict positivity 0 < B σ τ on swap-related H_0 configurations with positive symmetric bipartite J. Combines the dressed matrix value -J(x, y).re (PR α-5i) with the off-diagonal definition B σ τ = -M σ τ (PR α-5d). Single-step strict positivity for Perron–Frobenius irreducibility | Quantum/MarshallLiebMattis/H0ShiftedSwap.lean |
| matrix_pow_succ_pos_of_path | generic matrix-power positivity from a positive path: for non-negative matrix B and a path p_0, ..., p_{k+1} with B(p_i, p_{i+1}) > 0 on every consecutive pair, (B^(k+1))(p_0)(p_{k+1}) > 0. Induction on k using pow_succ + Finset.sum_pos'. Used to lift single-step swap positivity (α-5j) to multi-step matrix-power positivity for PF irreducibility | Quantum/MarshallLiebMattis/MatrixPowPath.lean |
| matrix_pow_succ_pos_of_pow_pos_step | one-step extension: if (B^m) σ τ > 0 and B τ ρ > 0 for non-negative B, then (B^(m+1)) σ ρ > 0. Inductive building block for ReflTransGen-style matrix-power lifting | Quantum/MarshallLiebMattis/MatrixPowExtend.lean |
| dressedHeisenbergShifted_pow_pos_of_swapReachable | for σ : H₀Index Λ and any ξ with Relation.ReflTransGen (SwapStep G) σ.val ξ, there exists m with (B^m) σ ⟨ξ, h_mag⟩ > 0. Induction on ReflTransGen: refl gives m = 0, tail extends by one swap using α-5j (single-step swap positivity) and α-5l (one-step matrix-power extension). Key bridge from combinatorial reachability to PF irreducibility | Quantum/MarshallLiebMattis/H0ShiftedReachable.lean |
| dressedHeisenbergShifted_isIrreducible | B = c · I − M is irreducible on H_0 for connected bipartite G with positive symmetric real coupling supported on G-edges and shift constant c > M σ σ (strict). Cases on σ = τ (use diagonal positivity) vs σ ≠ τ (use α-5c reachability + α-5m matrix-power lift). Final input for Perron–Frobenius application | Quantum/MarshallLiebMattis/H0ShiftedIrreducible.lean |
| dressedHeisenbergShifted_isHermitian | the shifted matrix is Hermitian (= symmetric for real matrices). Wraps dressedHeisenbergShifted_isSymm (PR α-5d) into the IsHermitian form needed by Perron–Frobenius | Quantum/MarshallLiebMattis/H0PFApplication.lean |
| dressedHeisenbergShifted_exists_pos_eigenvec_max / _pos_eigenvec_unique | Perron–Frobenius applied to B = c · I − M on H_0: existence of a strictly positive eigenvector v for some real eigenvalue μ, and uniqueness up to positive scalar. Translating back to M, v is the eigenvector for the minimum eigenvalue (the H_0 ground state of the AFM Heisenberg). This is the matrix-level Tasaki (2.5.4): the H_0 ground-state expansion Σ_σ c_σ \|Ψ̃^σ⟩ with c_σ = v σ > 0 is unique up to positive scalar | Quantum/MarshallLiebMattis/H0PFApplication.lean |
| bipartiteCoupling / heisenbergToyHamiltonian | the Tasaki §2.5 p. 40 toy Hamiltonian setup: bipartiteCoupling A x y := if A x ≠ A y then 1 else 0 (the unnormalised bipartite coupling), and heisenbergToyHamiltonian A := heisenbergHamiltonian (bipartiteCoupling A). Real symmetric, non-negative, supported on bipartite bonds, positive on inter-sublattice pairs. Hermitian. Used in subsequent PRs to derive S_tot = 0 for the AFM Heisenberg ground state via inner-product comparison | Quantum/MarshallLiebMattis/ToyHamiltonian.lean |
| bipartiteGraphFromA | the complete bipartite graph on Λ from sublattice indicator A : Λ → Bool: vertices x, y are adjacent iff A x ≠ A y. The natural bond graph for the toy Hamiltonian (every edge of bipartiteCoupling A is a bipartiteGraphFromA A-edge and vice versa) | Quantum/MarshallLiebMattis/BipartiteGraph.lean |
| bipartiteGraphFromA_preconnected | bipartiteGraphFromA A is preconnected when both sublattices are non-empty. Cases on A x = A y (length-2 path via opposite sublattice) vs A x ≠ A y (direct edge). Provides the G.Preconnected hypothesis needed for MLM application to the toy Hamiltonian | Quantum/MarshallLiebMattis/BipartiteGraph.lean |
| dressedHeisenbergShifted_toy_exists_pos_eigenvec_max / _pos_eigenvec_unique | Matrix-level Tasaki (2.5.4) for the toy Hamiltonian: the shifted toy matrix B_toy = c · I − M_toy (under both-sublattices-nonempty + diagonal-shift hypothesis) has a unique-up-to-positive-scalar strictly positive eigenvector. Specialises α-5o to the toy via α-6a + α-6b | Quantum/MarshallLiebMattis/ToyPF.lean |
| sublatticeSpinHalfOp{1,2,3} | sublattice spin operators Ŝ_A^(α) := Σ_{x ∈ A} onSite x Ŝ^(α) for α ∈ {1, 2, 3}. Foundation for the Casimir identity Ĥ_toy = (1/(2|Λ|))((Ŝ_tot)² − (Ŝ_A)² − (Ŝ_B)²) (Tasaki §2.5 (2.5.11)) | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinSOp{1,2,3} / totalSpinSOp{1,2,3}_eq_sublattice_sum | Spin-S analogues: Ŝ_A^(α) := Σ_{x : A x} onSiteS x (spinSOp_α N) for α ∈ {1, 2, 3}, with decomposition Ŝ_tot^(α) = Ŝ_A^(α) + Ŝ_¬A^(α). First step toward Tasaki §2.5 Theorem 2.3 (γ-4, |A| ≠ |B| case) | Quantum/SpinS/SublatticeSpin.lean (PR #1042) |
| sublatticeSpinSOp{1,2,3}_isHermitian | Spin-S sublattice operator Hermiticity (γ-4 step 2). Sum of Hermitian summands is Hermitian | Quantum/SpinS/SublatticeSpin.lean (PR #1043) |
| sublatticeSpinSquaredS / sublatticeSpinSquaredS_isHermitian | spin-S sublattice Casimir (Ŝ_A)² := Σ_α (Ŝ_A^(α))² plus Hermiticity. Foundation for the Casimir identity in Tasaki §2.5 (2.5.11) at general spin-S (γ-4 step 3) | Quantum/SpinS/SublatticeSpin.lean (PR #1044) |
| sublatticeSpinSOp{1,2,3}_cross_commute | spin-S cross-sublattice same-axis commutativity Commute (Ŝ_A^(α)) (Ŝ_¬A^(α)) for α ∈ {1, 2, 3}. Sites in A vs ¬A are distinct, so per-site operators commute via onSiteS_commute_of_ne (γ-4 step 4) | Quantum/SpinS/SublatticeSpin.lean (PR #1045) |
| sublatticeSpinSOpGeneric_cross_commute / sublatticeSpinSOp{1,2,3}_cross_commute_op{1,2,3} | spin-S mixed-axes cross-sublattice commutativity: Commute (Ŝ_A^(α)) (Ŝ_¬A^(β)) for any α, β ∈ {1, 2, 3}. Generic helper for arbitrary single-site operators; six mixed-axis specialisations follow as one-line corollaries (γ-4 step 5) | Quantum/SpinS/SublatticeSpin.lean (PR #1046) |
| sublatticeSpinSquaredS_cross_commute | spin-S sublattice Casimir cross-commute: Commute (Ŝ_A)² (Ŝ_¬A)². Sets up the joint eigenbasis of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² for the toy-Hamiltonian eigenvalue analysis at general spin-S (γ-4 step 6) | Quantum/SpinS/SublatticeSpin.lean (PR #1047) |
| sublatticeSpinSOp{1,2,3}_commutator_sublatticeSpinSOp{2,3,1} | spin-S sublattice SU(2) algebra: [Ŝ_A^α, Ŝ_A^β] = i ε^αβγ Ŝ_A^γ. Generic helper sublatticeSpinS_commutator_general lifts the single-site commutator to the sublattice sum (γ-4 step 7) | Quantum/SpinS/SublatticeSpin.lean (PR #1048) |
| sublatticeSpinSquaredS_commutator_sublatticeSpinSOp{1,2,3} / sublatticeSpinSquaredS_commute_sublatticeSpinSOp{1,2,3} | spin-S sublattice Casimir self-invariance: [(Ŝ_A)², Ŝ_A^(α)] = 0, equivalently Commute (Ŝ_A)² Ŝ_A^(α). Uses the SU(2) algebra (PR #1048) plus the Leibniz identity (γ-4 step 8) | Quantum/SpinS/SublatticeSpin.lean (PR #1049) |
| sublatticeSpinSquaredS_commute_sublatticeSpinSOp{1,2,3}_complement | spin-S sublattice Casimir vs complement axis-α: Commute (Ŝ_A)² Ŝ_¬A^(α) for α ∈ {1, 2, 3}. Each axis-β square (Ŝ_A^(β))² commutes with Ŝ_¬A^(α) by Commute.mul_left applied to the mixed-axes cross-commute (γ-4 step 9) | Quantum/SpinS/SublatticeSpin.lean (PR #1050) |
| sublatticeSpinSquaredS_commute_totalSpinSOp{1,2,3} | spin-S sublattice Casimir vs total spin axis-α: Commute (Ŝ_A)² Ŝ_tot^(α) for α ∈ {1, 2, 3}. Combines self-invariance (PR #1049) with the complement-axis result (PR #1050) via Commute.add_right after rewriting Ŝ_tot^(α) = Ŝ_A^(α) + Ŝ_¬A^(α) (γ-4 step 10) | Quantum/SpinS/SublatticeSpin.lean (PR #1051) |
| sublatticeSpinSquaredS_commute_totalSpinSSquared | spin-S sublattice Casimir vs total Casimir: Commute (Ŝ_A)² (Ŝ_tot)². Third pairwise commutativity needed for the joint eigenbasis of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² (Tasaki §2.5 toy-Hamiltonian eigenvalue analysis). Combines the three axis results from PR #1051 via Commute.mul_right and Commute.add_right (γ-4 step 11) | Quantum/SpinS/SublatticeSpin.lean (PR #1052) |
| heisenbergToyHamiltonianS / heisenbergToyHamiltonianS_isHermitian | spin-S MLM toy Hamiltonian (Tasaki §2.5 eq. (2.5.10) without 1/\|Λ\|): Ĥ_toy_S A := heisenbergHamiltonianS (bipartiteCoupling A) N. Reuses spin-independent bipartiteCoupling from Quantum/MarshallLiebMattis/ToyHamiltonian.lean. Hermitian via heisenbergHamiltonianS_isHermitian_of_real (γ-4 step 12) | Quantum/SpinS/ToyHamiltonian.lean (PR #1053) |
| sublatticeSpinSDot / sublatticeSpinSDot_def / sublatticeSpinSDot_eq_sum_sum / sublatticeSpinSDot_complement_isHermitian | spin-S cross-sublattice spin dot product Ŝ_A · Ŝ_B := Σ_α Ŝ_A^(α) Ŝ_B^(α), definitional unfolding, bilinear expansion Ŝ_A · Ŝ_B = Σ_{x : A x} Σ_{y : B y} Ŝ_x · Ŝ_y, and Hermiticity for B = ¬A (each axis-α summand is a product of two commuting Hermitian operators) (γ-4 step 13) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1054) |
| sublatticeSpinSDot_complement_comm / heisenbergToyHamiltonianS_eq_sublatticeSpinSDot_sum / heisenbergToyHamiltonianS_eq_two_sublatticeSpinSDot | spin-S toy Hamiltonian decomposes as oriented cross-sublattice spin dot products: Ĥ_toy_S = Ŝ_A · Ŝ_¬A + Ŝ_¬A · Ŝ_A, and via cross-sublattice symmetry the closed form Ĥ_toy_S = 2 • Ŝ_A · Ŝ_¬A. Bridges the bipartite-bond sum (Tasaki §2.5 (2.5.10)) to the operator-level Casimir form (γ-4 step 14) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1055) |
| totalSpinSSquared_eq_sublattice_casimir / heisenbergToyHamiltonianS_eq_casimir_diff | spin-S Casimir identity (Tasaki §2.5 (2.5.11)): (Ŝ_tot)² = (Ŝ_A)² + 2 • (Ŝ_A · Ŝ_¬A) + (Ŝ_¬A)² (per-axis (a + b)² = a² + 2ab + b² via cross-commute), and the closed form (without 1/\|Λ\|) Ĥ_toy_S = (Ŝ_tot)² − (Ŝ_A)² − (Ŝ_¬A)² (γ-4 step 15) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1056) |
| heisenbergToyHamiltonianS_commute_totalSpinSSquared / _commute_sublatticeSpinSquaredS / _complement | spin-S toy Hamiltonian commutes with the three Casimirs (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)². The first via SU(2) invariance of any spin-S Heisenberg Hamiltonian; the other two via the closed form (PR #1056) and the three pairwise Casimir commutativities (PRs #1047, #1052). All four Casimir-style commutators of Ĥ_toy_S, prerequisite for the joint eigenbasis analysis (γ-4 step 16) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1057) |
| heisenbergToyHamiltonianS_mulVec_of_jointCasimirEigenvector / neelStateOfS_heisenbergToyHamiltonianS_expectation_via_joint | spin-S toy Hamiltonian eigenvalue on simultaneous Casimir eigenvectors: for v a joint eigenvector of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² at eigenvalues α, β_A, β_B, Ĥ_toy_S · v = (α − β_A − β_B) • v and ⟨v, Ĥ_toy_S v⟩ = (α − β_A − β_B) · ⟨v, v⟩. Direct application of PR #1056’s closed form Ĥ_toy_S = (Ŝ_tot)² − (Ŝ_A)² − (Ŝ_¬A)² and linearity of mulVec. Sets up the eigenvalue analysis underpinning Tasaki §2.5 Theorem 2.3 (γ-4): minimising (α − β_A − β_B) over admissible joint eigenvalues gives the predicted S_tot = ||A| − |¬A||·S ground state (PR #2774, file Quantum/SpinS/ToyHamiltonianJointEigenvalue.lean) |
| heisenbergToyHamiltonianS_jointCasimirEigenspace_le_eigenspace | subspace-level form of PR #2774: the meet of the three Casimir eigenspaces at (α, β_A, β_B) is contained in the Ĥ_toy_S-eigenspace at (α − β_A − β_B), i.e. eigenspace(Ŝ_tot²)_α ⊓ eigenspace(Ŝ_A²)_β_A ⊓ eigenspace(Ŝ_¬A²)_β_B ≤ eigenspace(Ĥ_toy_S)_{α−β_A−β_B}. Direct lift of PR #2774’s pointwise identity to Submodule via Module.End.mem_eigenspace_iff (PR #2775, file Quantum/SpinS/ToyHamiltonianJointEigenspace.lean) |
| bipartiteToyMinEnergyPredicted / bipartiteToyMinEnergyPredicted_eq_simplified / bipartiteToyGroundStateSubspacePredicted / bipartiteToyGroundStateSubspacePredicted_le_heisenbergToyHamiltonianS_eigenspace | predicted toy-Hamiltonian ground state for the bipartite |A| ≥ |¬A| case (Tasaki §2.5 Theorem 2.3): definition bipartiteToyMinEnergyPredicted A N := (s_A − s_B)(s_A − s_B + 1) − s_A(s_A+1) − s_B(s_B+1) with s_A = \|A\|·N/2, s_B = \|¬A\|·N/2; simplification to −\|A\|·\|¬A\|·N²/2 − \|¬A\|·N via ring; definition bipartiteToyGroundStateSubspacePredicted A N as the joint eigenspace at the three target eigenvalues (sublattice Casimirs at maximum, total Casimir at the triangle-inequality minimum); subspace inclusion bipartiteToyGroundStateSubspacePredicted ≤ eigenspace(Ĥ_toy_S)_{bipartiteToyMinEnergyPredicted} via PR #2775’s joint-Casimir-eigenspace inclusion. The minimality of bipartiteToyMinEnergyPredicted as the actual Ĥ_toy_S ground-state eigenvalue (variational lower bound + sector non-emptiness) is the next γ-4 milestone (PR #2778, file Quantum/SpinS/BipartiteToyMinEnergy.lean) |
| bipartiteToyMinEnergyPredicted_eq_zero_of_cardNotA_zero / bipartiteToyMinEnergyPredicted_eq_balanced_form_of_card_eq | structural properties of bipartiteToyMinEnergyPredicted: (i) saturated edge case \|¬A\| = 0 → energy 0 (trivial empty-cross-bond limit); (ii) balanced edge case \|A\| = \|¬A\| → energy collapses to −2 s_A(s_A+1), the anti-ferromagnetic-saturation value (PR #2779, file Quantum/SpinS/BipartiteToyMinEnergyProperties.lean) |
| bipartiteToyMinEnergyPredicted_sub_complement | complement-orientation gap identity: bipartiteToyMinEnergyPredicted A N − bipartiteToyMinEnergyPredicted (¬A) N = (\|A\| − \|¬A\|)·N. Quantifies the orientation-asymmetry of the signed-difference formula in PR #2778: the true Tasaki §2.5 Theorem 2.3 prediction is min(E(A), E(¬A)), achieved at the orientation \|A\| ≥ \|¬A\| (or the complement orientation). Direct ring computation from PR #2779’s simplified form via (¬¬A) = A at the filter level (PR #2780, file Quantum/SpinS/BipartiteToyMinEnergyComplement.lean) |
| bipartiteToyMinEnergyPredictedSymm / _eq_predicted_of_cardNotA_le_cardA / _eq_complement_predicted_of_cardA_le_cardNotA / _complement | sublattice-swap symmetric predicted min energy: bipartiteToyMinEnergyPredictedSymm A N := −\|A\|·\|¬A\|·N²/2 − min(\|A\|, \|¬A\|)·N, the true Tasaki §2.5 Theorem 2.3 prediction independent of orientation. Bridges: equals bipartiteToyMinEnergyPredicted A N when \|¬A\| ≤ \|A\|, equals bipartiteToyMinEnergyPredicted (¬A) N when \|A\| ≤ \|¬A\|. Sublattice-swap invariant: Symm (¬A) N = Symm A N via Nat.min_comm + (¬¬A) = A (PR #2781, file Quantum/SpinS/BipartiteToyMinEnergySymm.lean) |
| sublatticeSpinSquaredS_commute_totalSpinSOpPlus / _totalSpinSOpMinus / bipartiteToyGroundStateSubspacePredicted_totalSpinSOpPlus_invariant / _totalSpinSOpMinus_invariant | Ŝ^+_tot / Ŝ^-_tot-invariance of the predicted GS subspace: derived commutations [(Ŝ_A)², Ŝ^±_tot] = 0 via the Cartesian commutations + totalSpinSOp{Plus,Minus}_eq_add/sub, plus the predicted-GS invariance under each ladder operator via the same pattern as PR #2798. Combined with PRs #2798 / #2799, full su(2) algebra closure: predicted GS is invariant under Cartan {Ŝ^z_tot} and ladders {Ŝ^+_tot, Ŝ^-_tot}, hence under the entire su(2) Lie algebra generated by these (PR #2800, file Quantum/SpinS/BipartiteToyGSLadderInvariant.lean) |
| bipartiteToyGroundStateSubspacePredicted_le_totalSpinSSquaredEigenspace / _le_sublatticeSpinSquaredSEigenspace / _le_sublatticeSpinSquaredS_complementEigenspace | predicted GS ⊆ each individual Casimir eigenspace at target (any A, any N, no saturation): three inclusions packaging the joint Casimir definition’s projections as standalone subspace inclusions (PR #2815, file Quantum/SpinS/BipartiteToyGSLeTotalSpinSSquaredEigenspace.lean) |
| bipartiteImbalanceWeight_eq_ofReal / bipartiteImbalanceWeight_im_zero / bipartiteImbalanceWeight_re_eq | bipartiteImbalanceWeight is real: realises bipartiteImbalanceWeight A N as the lift of the real-axis imbalance times N/2, so its imaginary part is 0 and its real part is (\|A\| − \|¬A\|)·N/2 : ℝ. Cleans up Tasaki §2.5 Theorem 2.3’s real-axis comparisons by removing the implicit ℝ → ℂ coercion (PR #2825, file Quantum/SpinS/BipartiteImbalanceWeightImZero.lean) |
| bipartiteImbalanceWeight_norm_eq | norm of bipartiteImbalanceWeight: ‖bipartiteImbalanceWeight A N‖ = \|\|A\| − \|¬A\|\| · N/2. This is the \|\|A\| − \|¬A\|\| · S predicted total spin that appears explicitly in Tasaki §2.5 Theorem 2.3 (S = N/2). Direct from PR #2825’s ofReal realisation + Complex.norm_real (PR #2826, file Quantum/SpinS/BipartiteImbalanceWeightAbs.lean) |
| bipartiteImbalanceWeight_norm_eq_re_of_cardNotA_le_cardA | norm = real part when \|A\| ≥ \|¬A\|: ‖bipartiteImbalanceWeight A N‖ = (bipartiteImbalanceWeight A N).re. Since the value is real (PR #2825) and non-negative in this case (PR #2773), norm = .re directly (PR #2862, file Quantum/SpinS/BipartiteImbalanceWeightNormEqRe.lean) |
| cardA_add_cardNotA_eq_card / filter_notA_eq_filter_not_A_eq_true | bipartition cardinality sum: for A : Λ → Bool, \|A\| + \|¬A\| = Fintype.card Λ. Foundational identity bridging \|A\|, \|¬A\|, and \|Λ\| across the γ-4 chain (PR #2870, file Quantum/SpinS/CardSumEqFintype.lean) |
| bipartiteToyMinEnergyPredictedSymm_re_via_imbalance_sq | bridge identity between the symm-energy real part and the imbalance-weight squared real part: 8·((bipartiteToyMinEnergyPredictedSymm A N).re + min(\|A\|, \|¬A\|)·N) + \|Λ\|²·N² = 4·((bipartiteImbalanceWeight A N).re)². Algebraic consequence of 4·\|A\|·\|¬A\| = (\|A\|+\|¬A\|)² - (\|A\|-\|¬A\|)² combined with \|A\| + \|¬A\| = \|Λ\| (PR #2870) (PR #2876, file Quantum/SpinS/BipartiteToyMinEnergySymmViaImbalance.lean) |
| bipartiteImbalanceWeight_norm_mul_self_eq_re_mul_self / bipartiteToyMinEnergyPredictedSymm_re_via_imbalance_norm_sq | norm-squared = real-part squared (‖biw‖·‖biw‖ = biw.re·biw.re, since biw is real, PR #2825) and the resulting bridge identity in ‖biw‖² form: 8·((bipartiteToyMinEnergyPredictedSymm A N).re + min(\|A\|, \|¬A\|)·N) + \|Λ\|²·N² = 4·‖bipartiteImbalanceWeight A N‖². Substitutes (biw.re)² = ‖biw‖² into PR #2876; natural form for Tasaki §2.5 Theorem 2.3 where the predicted spin magnitude ‖biw‖ = \|\|A\| − \|¬A\|\|·N/2 appears directly (PR #2877, file Quantum/SpinS/BipartiteToyMinEnergySymmReViaImbalanceNormSq.lean) |
| min_cardA_cardNotA_mul_N_eq_half_card_times_N_sub_imbalance_norm | linear identity bridging min·N and ‖biw‖: min(\|A\|, \|¬A\|)·N = \|Λ\|·N/2 − ‖bipartiteImbalanceWeight A N‖. Direct from PR #2826 (‖biw‖ = \|\|A\|−\|¬A\|\|·N/2) + PR #2870 (\|A\|+\|¬A\| = \|Λ\|) via the elementary identity 2·min = (\|A\|+\|¬A\|) − \|\|A\|−\|¬A\|\|. Enables min·N-free reformulations of all Tasaki §2.5 Theorem 2.3 (γ-4) energy bounds (PR #2887, file Quantum/SpinS/MinNEqHalfCardTimesNMinusImbalanceNorm.lean) |
| neelStateOfS_totalSpinSSquared_expectation_re_via_imbalance_norm_sq | Néel-state (Ŝ_tot)² expectation real part in ‖biw‖² form: (<Φ_Néel\|(Ŝ_tot)²\|Φ_Néel>).re = ‖biw‖² + \|Λ\|·N/2. Direct from γ-4 step 225 (= ((\|A\|-\|¬A\|)·N/2)² + \|Λ\|·N/2) + PR #2877 helper (‖biw‖² = (biw.re)²). Connects the Néel Casimir expectation to the predicted spin magnitude squared (‖biw‖² = (predicted S_tot)²) plus the lattice-size offset m_max = \|Λ\|·N/2 (PR #2896, file Quantum/SpinS/NeelStateOfSTotalSpinSSquaredReViaImbalanceNormSq.lean) |
| neelStateOfS_totalSpinSSquared_expectation_re_sub_predicted_eq_min_N | Néel-vs-predicted (Ŝ_tot)² gap = min·N: (<Φ_Néel\|(Ŝ_tot)²\|Φ_Néel>).re − (‖biw‖² + ‖biw‖) = min(\|A\|, \|¬A\|)·N. Direct parallel of energy gap PR #2884 to the (Ŝ_tot)² Casimir: the Néel state’s (Ŝ_tot)² expectation is exactly min·N above the predicted S_tot·(S_tot+1) = ‖biw‖·(‖biw‖+1) eigenvalue (Tasaki §2.5 Theorem 2.3). Gap vanishes at saturated edges (PR #2901, file Quantum/SpinS/NeelStateOfSTotalSpinSSquaredVsPredictedGap.lean) |
| neelStateOfS_totalSpinSSquared_expectation_re_gt_predicted_of_nondegenerate | strict positive Néel-vs-predicted (Ŝ_tot)² gap at non-degenerate: ‖biw‖² + ‖biw‖ < (<Φ_Néel\|(Ŝ_tot)²\|Φ_Néel>).re when \|A\| ≥ 1, \|¬A\| ≥ 1, N ≥ 1. Strict version of PR #2901; gap = min·N > 0. Demonstrates the Néel state spans multiple S_tot sectors (not the GS) at non-degenerate (PR #2902, file Quantum/SpinS/NeelStateOfSTotalSpinSSquaredVsPredictedGapPosNondegenerate.lean) |
| neelStateOfS_mem_joint_sublattice_casimir_eigenspace | Néel ∈ joint sublattice-Casimir eigenspace: Φ_Néel(A, N) ∈ eigenspace((Ŝ_A)², s_A·(s_A+1)) ⊓ eigenspace((Ŝ_¬A)², s_B·(s_B+1)). Two-thirds of the predicted GS subspace conditions. Néel is NOT in the full predicted GS subspace because its (Ŝ_tot)² expectation (‖biw‖²+\|Λ\|·N/2, PR #2896) exceeds the predicted eigenvalue ‖biw‖·(‖biw‖+1) by min·N (PR #2901) (PR #2913, file Quantum/SpinS/NeelStateOfSMemJointSublatticeCasimirEigenspace.lean) |
| neelStateOfS_notMem_bipartiteToyGroundStateSubspacePredicted_of_nondegenerate | Néel ∉ predicted GS at non-degenerate: at \|A\| ≥ 1, \|¬A\| ≥ 1, N ≥ 1, \|¬A\| ≤ \|A\|, Φ_Néel(A, N) ∉ bipartiteToyGroundStateSubspacePredicted A N. By contradiction: if Néel were in the GS, <(Ŝ_tot)²>_Néel would equal the predicted eigenvalue ‖biw‖·(‖biw‖+1), but PR #2902 shows strict <(Ŝ_tot)²>_Néel > ‖biw‖·(‖biw‖+1). Complements PR #2914 (saturated case: Néel ∈ GS) (PR #2919, file Quantum/SpinS/NeelStateOfSNotMemBipartiteToyGSPredictedNondegenerate.lean) |
| joint_sublattice_casimir_eigenspace_strict_supset_predicted_gs_of_nondegenerate | Joint sublattice-Casimir eigenspace strictly contains predicted GS at non-degenerate (\|¬A\| ≤ \|A\|): bipartiteToyGroundStateSubspacePredicted A N ⊊ eigenspace((Ŝ_A)², s_A·(s_A+1)) ⊓ eigenspace((Ŝ_¬A)², s_B·(s_B+1)). The Néel state witnesses the strict inclusion: ∈ joint Casimir eigenspace (PR #2913) but ∉ predicted GS (PR #2919). The “extra” states have max sublattice spins but wrong total spin (PR #2923, file Quantum/SpinS/JointSublatticeCasimirStrictSupsetPredictedGS.lean) |
| jointSublatticeCasimirEigenspace / bipartiteToyGroundStateSubspacePredicted_finrank_lt_joint_eigenspace_finrank_of_nondegenerate | Predicted GS finrank < joint Casimir finrank at non-deg: finrank (predicted GS A N) < finrank (joint Casimir eigenspace A N). Direct from PR #2923’s strict subspace inclusion in finite-dim space. Quantifies the “extra” subspace beyond the predicted GS (PR #2924, file Quantum/SpinS/PredictedGSFinrankLtJointCasimirFinrank.lean) |
| bipartiteToyMinEnergyPredictedSymm_im_zero / _re_eq | bipartiteToyMinEnergyPredictedSymm is real: imaginary part is 0 and real part is -\|A\|·\|¬A\|·N²/2 - min(\|A\|, \|¬A\|)·N (with min taken in ℝ after Nat.cast_min). Mirrors PR #2825 for the asymmetric form (PR #2843, file Quantum/SpinS/BipartiteToyMinEnergySymmReal.lean) |
| sublatticeSpinSquaredS_eq_sum_dot | spin-S sublattice Casimir as a double-sum of two-site dot products: (Ŝ_A)² = Σ_{x ∈ A} Σ_{y ∈ A} Ŝ_x · Ŝ_y. Specialisation B = A of sublatticeSpinSDot_eq_sum_sum (PR #1054), foundation for sublattice Casimir eigenvalue formulas on constant-on-A configurations (γ-4 step 17) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1058) |
| sublatticeSpinSquaredS_mulVec_allAlignedStateS_zero | spin-S sublattice Casimir eigenvalue on the all-up state: (Ŝ_A)² · \|σ_⊤⟩ = ((\|A\|·N/2)·(\|A\|·N/2+1)) · \|σ_⊤⟩ — the maximum-spin Casimir value of the A-subsystem at total spin J_A = \|A\|·N/2 = \|A\|·S. From the bilinear expansion (PR #1058) plus diagonal Ŝ_x · Ŝ_x = N(N+2)/4 · 1 and off-diagonal Ŝ_x · Ŝ_y · \|σ_⊤⟩ = N²/4 · \|σ_⊤⟩ for x ≠ y. First eigenvalue lemma in the joint eigenbasis analysis underpinning Tasaki §2.5 Theorem 2.3 (γ-4 step 18) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1059) |
| heisenbergToyHamiltonianS_mulVec_allAlignedStateS_zero | spin-S toy Hamiltonian eigenvalue on the all-up state: Ĥ_toy_S · \|σ_⊤⟩ = ((\|Λ\|·N/2)(\|Λ\|·N/2+1) − (\|A\|·N/2)(\|A\|·N/2+1) − (\|¬A\|·N/2)(\|¬A\|·N/2+1)) · \|σ_⊤⟩. Direct combination of closed form (PR #1056), total Casimir on \|σ_⊤⟩ (existing in AllAlignedStateCore.lean), and sublattice Casimirs on \|σ_⊤⟩ (PR #1059) (γ-4 step 19) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1060) |
| heisenbergToyHamiltonianS_mulVec_allAlignedStateS_zero_simplified | simplified spin-S toy Hamiltonian eigenvalue on the all-up state: Ĥ_toy_S · \|σ_⊤⟩ = (\|A\|·\|¬A\|·N²/2) · \|σ_⊤⟩. Algebraic simplification of PR #1060 via \|Λ\| = \|A\| + \|¬A\| and the identity (a+b)(a+b+1) − a(a+1) − b(b+1) = 2ab. Specialises to spin-1/2 eigenvalue \|A\|·\|¬A\|/2. Non-negative on bipartite lattices, strictly positive when both sublattices non-empty (γ-4 step 20) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1061) |
| sublatticeSpinSquaredS_mulVec_allAlignedStateS_last | spin-S sublattice Casimir eigenvalue on the all-down state: (Ŝ_A)² · \|σ_⊥⟩ = ((\|A\|·N/2)·(\|A\|·N/2+1)) · \|σ_⊥⟩ — same maximum-spin Casimir value as PR #1059, since both sit in the J_A = \|A\|·N/2 irrep. Mirror of _zero using the lowest-weight off-diagonal formula spinSDot_mulVec_allAlignedStateS_last_of_ne (γ-4 step 21) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1062) |
| heisenbergToyHamiltonianS_mulVec_allAlignedStateS_last / _simplified | spin-S toy Hamiltonian eigenvalue on the all-down state plus simplified form \|A\|·\|¬A\|·N²/2. Symmetric to PRs #1060 / #1061; combines closed form (PR #1056) with total / sublattice Casimirs on \|σ_⊥⟩ (existing + PR #1062) (γ-4 step 22) | Quantum/SpinS/ToyHamiltonianCasimir.lean (PR #1063) |
| spinSDot_mulVec_basisVecS_zero_of_ne | spin-S two-site dot on configs with σ x = σ y = 0 (highest weight at the two sites, σ arbitrary elsewhere): Ŝ_x · Ŝ_y · \|σ⟩ = (N²/4) · \|σ⟩ for x ≠ y. Generalises spinSDot_mulVec_allAlignedStateS_zero_of_ne to allow non-constant configs outside {x, y}. Foundation for the spin-S Néel state Casimir eigenvalue (γ-4 step 23) | Quantum/SpinS/SpinSDotAllAlignedZero.lean (PR #1064) |
| spinSDot_mulVec_basisVecS_last_of_ne | lowest-weight counterpart of PR #1064: spin-S two-site dot on configs with σ x = σ y = Fin.last N: Ŝ_x · Ŝ_y · \|σ⟩ = (N²/4) · \|σ⟩ for x ≠ y. Same value as PR #1064; both highest-weight (σ x = 0) and lowest-weight (σ x = Fin.last N) configurations give (N/2)² = N²/4 (γ-4 step 24) | Quantum/SpinS/SpinSDotAllAlignedLast.lean (PR #1065) |
| sublatticeSpinSquaredS_mulVec_basisVecS_of_const_zero_on / _of_const_last_on | spin-S sublattice Casimir eigenvalue on configs constant on A (at highest weight 0 or lowest weight Fin.last N): (Ŝ_A)² · \|σ⟩ = ((\|A\|·N/2)·(\|A\|·N/2+1)) · \|σ⟩. Generalises PRs #1059 / #1062 to allow σ to be arbitrary on ¬A. Foundation for the spin-S Néel state (γ-4 step 25) | Quantum/SpinS/SublatticeSpinDot.lean (PR #1066) |
| neelConfigOfS / neelStateOfS / sublatticeSpinSquaredS_mulVec_neelStateOfS / _complement_mulVec_neelStateOfS | spin-S Néel state on a bipartite graph: σ x := 0 for A x = true (highest weight on A), Fin.last N otherwise (lowest weight on ¬A); together with the sublattice Casimir eigenvalues (Ŝ_A)² · \|Φ_Néel⟩ = (\|A\|·N/2)(\|A\|·N/2+1) · \|Φ_Néel⟩ and (Ŝ_¬A)² · \|Φ_Néel⟩ = (\|¬A\|·N/2)(\|¬A\|·N/2+1) · \|Φ_Néel⟩. Mirrors Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (γ-4 step 26) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (PR #1067) |
← 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)) →