S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) (part 2 of 4)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 |
|—|—|
| spinSDotXXZSwap, singleIonAnisotropyS2, axisSwappedAnisotropicHeisenbergS | Axis-swapped anisotropic Hamiltonian (Tasaki (2.5.15), Issue #3739, PR #3749): the spin-axis-2↔3 relabelling of (2.5.14), Ĥ' = Σ_{x,y} J_{x,y}(Ŝ¹_x Ŝ¹_y + λ Ŝ²_x Ŝ²_y + Ŝ³_x Ŝ³_y) + D Σ_x (Ŝ²_x)² — anisotropy now in the transverse plane, so its (2.5.16) ladder form has the ±2-magnetization Ŝ⁺Ŝ⁺/Ŝ⁻Ŝ⁻ terms coupling sectors into even/odd parity (where the Perron–Frobenius ≤2 degeneracy bound is proved). Hermitian for real J, λ, D (axisSwappedAnisotropicHeisenbergS_isHermitian_of_real). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.15) (file Quantum/SpinS/AxisSwappedAnisotropicHeisenberg.lean) |
| manyBodyTensorS, manyBodyTensorS_mul | Many-body tensor (product) operator and its functoriality (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3750): manyBodyTensorS W = ⊗_x W x (entry ∏_x (W x) (σ' x) (σ x)), with manyBodyTensorS W * manyBodyTensorS W' = manyBodyTensorS (fun x => W x * W' x) (a product of sums is a sum of products, Fintype.prod_sum) and manyBodyTensorS (fun _ => 1) = 1. This is the general single-site-operator lift (generalising the configuration-permutation manyBodyReversalS to a non-permutation W, e.g. the Wigner d-matrix gauge rotation); it gives Θ_U (onSiteS z A) Θ_U⁻¹ = onSiteS z (U A U⁻¹) for the axis-swap gauge of Theorem 2.4. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ManyBodyTensorS.lean) |
| onSiteS_eq_manyBodyTensorS, manyBodyTensorS_conj_onSiteS | Gauge conjugation of a single-site operator (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3751): onSiteS z A equals the tensor with A at z and 1 elsewhere (onSiteS_eq_manyBodyTensorS, via Finset.prod_boole); hence the tensor unitary Θ_U = ⊗_x U conjugates it, Θ_U (onSiteS z A) Θ_{U⁻¹} = onSiteS z (U A U⁻¹) (manyBodyTensorS_conj_onSiteS, for U·Uinv = 1, via the functoriality #3750). This is the single-site step that lifts the axis-swap rotation to Θ_U Ĥ Θ_{U⁻¹} = Ĥ'. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ManyBodyTensorConj.lean) |
| AxisSwapUnitaryS, AxisSwapUnitaryS.tensor_conj_anisotropicHeisenbergS | Gauge equivalence of the anisotropic and axis-swapped Hamiltonians (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3752): AxisSwapUnitaryS N bundles a single-site π/2 rotation about axis 1 (invertible U with U Ŝ¹ U⁻¹ = Ŝ¹, U Ŝ² U⁻¹ = Ŝ³, U Ŝ³ U⁻¹ = −Ŝ²). Its many-body lift Θ_U = ⊗_x U satisfies Θ_{U⁻¹} Θ_U = 1, conjugates products (tensor_conj_mul) and single-site operators (tensor_conj_onSiteS), and carries the anisotropic Hamiltonian (2.5.14) to its axis-swapped image (2.5.15): Θ_U Ĥ Θ_{U⁻¹} = Ĥ' (tensor_conj_anisotropicHeisenbergS; the Ŝ³ → −Ŝ² sign squares away in the bilinear bond and (Ŝ³)² terms). With the similarity invariant #3746 this transfers the ground-state degeneracy; the explicit U (spin-1/2 / Wigner d-matrix) instantiates the interface. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.15) (file Quantum/SpinS/AxisSwapGaugeEquiv.lean) |
| spinReversalS, spinReversalS_conj_spinSOp3, spinReversalS_conj_spinSOpPlus, spinReversalS_conj_spinSOpMinus, spinReversalS_conj_spinSOp1, spinReversalS_conj_spinSOp2 | Single-site spin reversal (π-rotation about axis 1) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3743): the permutation matrix F of Fin.rev (k ↦ N−k); conjugation reindexes by Fin.rev ((F·M·F) i j = M (rev i) (rev j)), giving F Ŝ³ F = −Ŝ³, F Ŝ⁺ F = Ŝ⁻, F Ŝ⁻ F = Ŝ⁺ (hence Ŝ¹↦Ŝ¹, Ŝ²↦−Ŝ²), and F is an involution. The many-site product Θ = ⊗_x F will give the M ↔ −M reflection symmetry Θ Ŝ³_tot Θ⁻¹ = −Ŝ³_tot, Θ Ĥ Θ⁻¹ = Ĥ used in the Mattis–Nishimori uniqueness argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/SpinSReversal.lean) |
| manyBodyReversalS, manyBodyReversalS_conj_onSiteS, manyBodyReversalS_conj_totalSpinSOp3 | Many-body spin reversal and the magnetization reflection (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3744): the configuration-reversal permutation Θ (σ ↦ Fin.rev ∘ σ); conjugation reindexes by revConfigS ((Θ·M·Θ) σ' σ = M (rev∘σ') (rev∘σ)), is an involution, conjugates a single-site operator Θ (onSiteS z A) Θ = onSiteS z (F A F), and reverses the total Ŝ³: Θ Ŝ³_tot Θ = −Ŝ³_tot. This is the M ↔ −M magnetization reflection used in the Mattis–Nishimori uniqueness argument (E_M = E_{−M} and, with the ground state in H_0, Ŝ³_tot Φ_GS = 0). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ManyBodyReversalS.lean) |
| manyBodyReversalS_conj_anisotropicHeisenbergS (with manyBodyReversalS_conj_mul, ..._conj_spinSDotXXZ, ..._conj_singleIonAnisotropyS; single-site spinReversalS_conj_spinSOp{1,2} now live in SpinSReversal.lean) | Reflection invariance of the anisotropic Hamiltonian (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3745): Θ Ĥ Θ = Ĥ for the anisotropic XXZ + single-ion Hamiltonian. The single-site reversal fixes Ŝ¹ and flips Ŝ² ↦ −Ŝ², Ŝ³ ↦ −Ŝ³, so each bilinear bond term Ŝ^α Ŝ^α and the single-ion (Ŝ³)² are preserved; conjugation distributes over products (manyBodyReversalS_conj_mul, inserting Θ² = 1). Together with Θ Ŝ³_tot Θ = −Ŝ³_tot (#3744) this completes the M ↔ −M reflection symmetry of the Mattis–Nishimori argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicReflectionSymmetry.lean) |
| matrix_similar_eigenspace_finrank_eq | Eigenspace dimension is a similarity invariant (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3746): for invertible U (U·Uinv = Uinv·U = 1) and H' = Uinv·H·U, every μ-eigenspace of H' and of H has equal finrank — the map v ↦ U *ᵥ v (Matrix.toLin'OfInv) carries eigenspace H' μ isomorphically onto eigenspace H μ (LinearEquiv.submoduleMap + LinearEquiv.finrank_eq). This transfers the ground-state degeneracy bound between the anisotropic Hamiltonian and its axis-swapped gauge image (only the degeneracy count is needed, so similarity — not unitarity — suffices). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/GaugeEigenspaceFinrank.lean) |
| AxisSwapUnitaryS.anisotropic_axisSwapped_eigenspace_finrank_eq (with AxisSwapUnitaryS.tensor_mul_tensorInv) | Equal ground-state degeneracy of Ĥ and Ĥ' (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3753): combining the gauge equivalence Θ_U Ĥ Θ_{U⁻¹} = Ĥ' (#3752) with the similarity invariant (#3746), every μ-eigenspace of the anisotropic Hamiltonian (2.5.14) and of its axis-swapped image (2.5.15) has equal finrank. The needed second inverse identity Θ_U Θ_{U⁻¹} = 1 (tensor_mul_tensorInv) follows from manyBodyTensorS functoriality and U · Uinv = 1. This is the bridge that carries the parity-sector Perron–Frobenius degeneracy bound (proved on Ĥ') back to the original Ĥ. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AxisSwapDegeneracy.lean) |
| axisSwapUnitarySpinHalf, spinHalf_anisotropic_axisSwapped_eigenspace_finrank_eq | Explicit spin-1/2 axis-swap unitary + degeneracy milestone (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3754): the AxisSwapUnitaryS 1 interface is instantiated by the π/2 rotation about spin-axis 1, Û^{(1)}_{π/2} = spinHalfRot1 (π/2) — conjugation fixes Ŝ¹, sends Ŝ² ↦ Ŝ³, Ŝ³ ↦ −Ŝ² (the axis-2↔3 swap), proved from the existing π/2 adjoint-conjugation lemmas via a generic Û†ŜÛ → ÛŜÛ† swap. Combined with #3753 this gives the spin-1/2 milestone: on any finite lattice the spin-1/2 anisotropic Hamiltonian (2.5.14) and its axis-swapped image (2.5.15) have equal μ-eigenspace dimension, hence equal ground-state degeneracy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44; §2.1 eq. (2.1.15) (file Quantum/SpinS/AxisSwapUnitarySpinHalf.lean) |
| manyBodyReversalS_anisotropic_sector_eigenspace_finrank_eq (with totalSpinSOp3_mul_manyBodyReversalS, anisotropicHeisenbergS_mul_manyBodyReversalS, manyBodyReversalS_mulVec_mem_magSubspaceS_neg) | M ↔ −M reflection symmetry of the per-sector spectrum (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3755): the spin reversal Θ (manyBodyReversalS, axis-1 π-rotation) anticommutes with Ŝ³_tot (Ŝ³_tot Θ = −Θ Ŝ³_tot) and commutes with Ĥ (Ĥ Θ = Θ Ĥ, from Θ Ĥ Θ = Ĥ, #3745). Hence Θ maps magnetization sector M onto sector −M (manyBodyReversalS_mulVec_mem_magSubspaceS_neg) while preserving every Ĥ-eigenspace, so the μ-eigenspace of Ĥ intersected with sector M and with sector −M have equal finrank (E_M = E_{-M}). This is the reflection symmetry behind the “first crossing forces ≥3-fold degeneracy” step of the Mattis–Nishimori uniqueness argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicReflectionEigenspace.lean) |
| spinSDotXXZSwap_ladder_form | Ladder form of the axis-swapped bond (Tasaki eq. (2.5.16), Issue #3739, PR #3756): Ŝ¹_x Ŝ¹_y + λ Ŝ²_x Ŝ²_y + Ŝ³_x Ŝ³_y = (1+λ)/4 (Ŝ⁺_x Ŝ⁻_y + Ŝ⁻_x Ŝ⁺_y) + (1−λ)/4 (Ŝ⁺_x Ŝ⁺_y + Ŝ⁻_x Ŝ⁻_y) + Ŝ³_x Ŝ³_y. The decisive (1−λ)/4 (Ŝ⁺Ŝ⁺ + Ŝ⁻Ŝ⁻) term changes the total magnetization by ±2, coupling the Ŝ³_tot sectors into the two even/odd parity blocks where the Marshall-sign Perron–Frobenius argument gives at-most-double degeneracy. Proved from the two-site ladder identities (#3747) by expanding Ŝ¹, Ŝ² into Ŝ± and module. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.16) (file Quantum/SpinS/AxisSwapLadderForm.lean) |
| onSiteS_spinSOpPlus_mul_onSiteS_spinSOpPlus_mulVec_mem_magSubspaceS (with the Ŝ⁻Ŝ⁻, Ŝ⁺Ŝ⁻, Ŝ⁻Ŝ⁺ variants and totalSpinSOp3_mul_onSiteS_spinSOp{Plus,Minus}) | Parity preservation of the axis-swapped ladder bond (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3757): the two-site ladder operators shift the total magnetization by an even amount — Ŝ⁺_x Ŝ⁺_y by +2, Ŝ⁻_x Ŝ⁻_y by −2, Ŝ⁺_x Ŝ⁻_y and Ŝ⁻_x Ŝ⁺_y by 0 (as mulVec-maps between magSubspaceS sectors). Hence every term of Ĥ' in ladder form (2.5.16) preserves the even/odd magnetization parity — the structure behind the parity-block Perron–Frobenius bound. Proved from single-site shifts [Ŝ³_tot, onSiteS x Ŝ±] = ±onSiteS x Ŝ± (onSiteS_commutator_totalOnSiteS + single-site Cartan) lifted through a generic two-factor shift lemma. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapLadderMagShift.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS, dressedAxisSwappedAnisotropicHeisenbergS_eigenspace_finrank_eq (with _diag, _eq_diag_conj, marshallDiagonal_mul_self) | Marshall-dressed axis-swapped Hamiltonian (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3758): the Marshall gauge dresses Ĥ' entrywise by marshallSignS A σ · marshallSignS A σ' · Ĥ'_{σσ'}, equivalently Ĥ'_dressed = Θ_A Ĥ' Θ_A with Θ_A = diagonal (marshallSignS A) (_eq_diag_conj). Since each Marshall sign is ±1, Θ_A is its own inverse (marshallDiagonal_mul_self), so this is a similarity: every μ-eigenspace of Ĥ'_dressed and of Ĥ' has equal finrank (via #3746); the diagonal entries are unchanged (_diag). In this dressed basis the off-diagonal entries become sign-definite (≤ 0 for case (i)), powering the parity-sector Perron–Frobenius degeneracy bound. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwappedAnisotropic.lean) |
| onSiteS_spinSOpPlus_mul_onSiteS_spinSOpPlus_apply_im_zero_re_nonneg (with the Ŝ⁻Ŝ⁻, Ŝ⁺Ŝ⁻, Ŝ⁻Ŝ⁺ variants and generic onSiteS_mul_onSiteS_apply_{im_zero_of_real, re_nonneg_of_real_nonneg}) | Config-basis entries of the axis-swapped ladder bond terms are real and non-negative (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3759): each cross-site product onSiteS x Ŝ^a · onSiteS y Ŝ^b (a,b ∈ {+,−}, x ≠ y) of the (2.5.16) ladder form has real (im = 0), non-negative (re ≥ 0) matrix elements — a product of two single-site raising/lowering entries (themselves real and non-negative). This is the bare-sign input to the Marshall-dressed off-diagonal sign analysis: in the dressed basis these positive entries are flipped to ≤ 0 (case (i)). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapLadderEntry.lean) |
| dressed_entry_re_nonpos_bipartite_x, dressed_entry_re_nonpos_bipartite_y | Marshall dressing flips non-negative entries to non-positive on a bipartite bond (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3760): for a bipartite bond x ≠ y (A-site on x, resp. y) with configurations agreeing off {x, y} and an odd total shift on the A-site, the Marshall sign product marshallSignS A σ · marshallSignS A σ' = −1 (marshallSignS_mul_of_agree_off_two_site_bipartite_{x,y}), so any operator with real non-negative config entries acquires Re ≤ 0 after dressing. This holds for BOTH the transverse hop (Ŝ⁺_x Ŝ⁻_y) and the parity hop (Ŝ⁺_x Ŝ⁺_y) — any ±1 move on the A-site makes (σ' · ) + (σ · ) odd — the joint sign-consistency making the whole dressed Ĥ' off-diagonal non-positive (case (i)). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedBipartiteSign.lean) |
| spinSOp2_mul_spinSOp2_ladder_form, singleIonAnisotropyS2_ladder_form | Ladder form of the single-ion anisotropy term (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3761): the single-site square Ŝ²_x Ŝ²_x = ¼(Ŝ⁺Ŝ⁻ + Ŝ⁻Ŝ⁺) − ¼(Ŝ⁺Ŝ⁺ + Ŝ⁻Ŝ⁻) (from the two single-site transverse-ladder identities #3742), so D Σ_x (Ŝ²_x)² has same-site ±2 parity coupling −D/4 (Ŝ⁺_x Ŝ⁺_x + Ŝ⁻_x Ŝ⁻_x). For case (i) (D ≥ 0) the coefficient −D/4 ≤ 0, and the same-site Marshall sign is +1 (the ±2 shift is even), so the dressed single-ion off-diagonal entry stays ≤ 0. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/SingleIonOffDiag.lean) |
| onSiteS_spinSOp3_mul_onSiteS_spinSOp3_apply_eq_zero_of_ne, spinSDotXXZSwap_apply_im_zero | Off-diagonal structure of the axis-swapped bond (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3762): for a bond x ≠ y the longitudinal Ŝ³_x Ŝ³_y is diagonal (off-diagonal config entries vanish), so every off-diagonal element of spinSDotXXZSwap x y λ comes from the transverse/parity ladder terms; combined with their realness (#3759), the whole bond off-diagonal element is real for real λ. This is the input needed to discuss its sign in the Marshall-dressed basis. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapBondOffDiag.lean) |
| spinSDotXXZSwap_apply_re_nonneg | Non-negativity of the axis-swapped bond off-diagonal entry (case (i)) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3763): for a bond x ≠ y and real λ with −1 ≤ λ ≤ 1, the off-diagonal config entry of spinSDotXXZSwap x y λ has Re ≥ 0 — the Ŝ³Ŝ³ part is diagonal, the transverse/parity ladder entries are real non-negative (#3759), and the coefficients (1+λ)/4, (1−λ)/4 ≥ 0. With the realness (#3762), the bipartite Marshall sign then flips this to ≤ 0 (#3760). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapBondReNonneg.lean) |
| spinSDotXXZSwap_apply_eq_zero_of_x_not_pm1 | Vanishing of the axis-swapped bond entry away from a single ladder step (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3764): every ladder term of spinSDotXXZSwap x y λ raises/lowers x by exactly one unit, so if x is neither raised (σx+1 ≠ σ'x) nor lowered (σ'x+1 ≠ σx) the off-diagonal bond entry is 0 (the diagonal Ŝ³Ŝ³ is killed by σ' ≠ σ). This restricts the non-vanishing dressed-sign cases to a ±1 shift on the A-site, where the Marshall sign is −1. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapBondVanish.lean) |
| dressedAxisSwapped_bond_re_nonpos_bipartite_x, dressedAxisSwapped_bond_re_nonpos_bipartite_y (with spinSDotXXZSwap_apply_eq_zero_of_y_not_pm1) | Marshall-dressed axis-swapped bond off-diagonal sign (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3765): for a bipartite bond x ≠ y (A-site at x, resp. y) and case-(i) λ (−1 ≤ λ ≤ 1 real), the dressed bond off-diagonal entry (marshallSignS A σ · marshallSignS A σ' · spinSDotXXZSwap x y λ σ' σ).re ≤ 0. Case split on the A-site shift: unchanged or ≥2 ⟹ bond entry vanishes (#3764); ±1 ⟹ odd shift ⟹ Marshall sign −1 (#3760) flips the real non-negative bond entry (#3762, #3763). This is the per-bond ingredient of the full dressed-Ĥ' off-diagonal non-positivity. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapBondSign.lean) |
| spinSOp2_mul_spinSOp2_apply_offdiag_re_nonpos, spinSOp2_mul_spinSOp2_apply_offdiag_im_zero (with _offdiag_eq, matrix_mul_self_apply_{im_zero,re_nonneg}) | Sign of the single-site (Ŝ²)² off-diagonal entries (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3766): the off-diagonal (i ≠ j) entries of (Ŝ²)² are real and ≤ 0 — in the ladder form (Ŝ²)² = ¼(Ŝ⁺Ŝ⁻+Ŝ⁻Ŝ⁺) − ¼(Ŝ⁺Ŝ⁺+Ŝ⁻Ŝ⁻) (#3761) the Ŝ⁺Ŝ⁻+Ŝ⁻Ŝ⁺ part is diagonal (#PlusMinusDiag, vanishes off-diagonal) and Ŝ⁺Ŝ⁺+Ŝ⁻Ŝ⁻ has real non-negative entries, so the −¼ coefficient makes them ≤ 0. With D ≥ 0 and the same-site Marshall sign +1 (the ±2 shift is even) this is the non-positive dressed single-ion off-diagonal contribution. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/SingleIonOffDiag.lean) |
| spinSOp2_mul_spinSOp2_apply_eq_zero_of_odd (with spinSOpPlus_mul_spinSOpPlus_apply_eq_zero_of_ne, spinSOpMinus_mul_spinSOpMinus_apply_eq_zero_of_ne) | Parity vanishing of the single-site (Ŝ²)² (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3767): (Ŝ²)²_{i j} = 0 whenever i.val + j.val is odd — (Ŝ⁺)² connects only j = i+2, (Ŝ⁻)² only i = j+2, both even differences. This makes the same-site Marshall sign (−1)^{σ'_x + σ_x} = +1 on the support of the single-ion term, so the dressed single-ion off-diagonal entries keep the sign −D/4 ≤ 0. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/SingleIonOffDiag.lean) |
| dressed_singleIonAnisotropyS2_re_nonpos (with dressed_onSiteS_spinSOp2_sq_re_nonpos) | Marshall-dressed single-ion off-diagonal non-positivity (case (i)) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3769): for D ≥ 0, the dressed off-diagonal entries of D Σ_x (Ŝ²_x)² have Re ≤ 0. Per site the (Ŝ²)² entry vanishes unless the shift is ±2 (even), where the same-site Marshall sign (marshallSignS_mul_of_agree_off_site) is +1, leaving the non-positive (Ŝ²)² off-diagonal entry (SingleIonOffDiag); multiplying by D ≥ 0 and summing over the (single) differing site preserves the sign. This is the single-ion ingredient of the full dressed-Ĥ' off-diagonal non-positivity. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedSingleIonSign.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_offdiag_re_nonpos (with spinSDotXXZSwap_apply_eq_zero_of_not_agree) | Full off-diagonal non-positivity of the Marshall-dressed axis-swapped Hamiltonian (case (i)) (Tasaki §2.5 Property (ii) / Theorem 2.4, Issue #3739, PR #3770): for a bipartite AFM coupling (J real ≥ 0, no self-bonds J x x = 0, cross-sublattice support J x y ≠ 0 ⟹ A x ≠ A y) and case-(i) anisotropy (−1 ≤ λ ≤ 1, D ≥ 0), every off-diagonal entry of Ĥ'_dressed has Re ≤ 0. Assembles the per-bond sign (#3765) over the double bond sum (bipartite bonds flipped by Marshall, off-sublattice / self bonds vanish or have J = 0) plus the single-ion sign (#3769). This is the Perron–Frobenius input: −Ĥ'_dressed is entrywise real with non-negative off-diagonal part. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapOffDiag.lean) |
| spinSDotXXZSwap_apply_eq_zero_of_local_odd (with spinSOpPlus_apply_eq_zero_of_even, spinSOpMinus_apply_eq_zero_of_even) | Parity preservation of the axis-swapped bond (matrix-entry form) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3771): the bond entry spinSDotXXZSwap x y λ σ' σ vanishes when the local occupation parity (σ'_x + σ_x) + (σ'_y + σ_y) is odd — each ladder term raises/lowers each site by exactly one unit, so non-vanishing contributions change the local sum by an even amount (Ŝ±_{ij} = 0 when i+j is even). This is the entry-level input to the parity-block decomposition of the dressed Ĥ' (PR5 of the parity-sector Perron–Frobenius route). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapBondParity.lean) |
| axisSwappedAnisotropicHeisenbergS_apply_eq_zero_of_magSum_parity_ne (with magSumS_add_parity_eq_of_agree_off_{two_site,site}, spinSDotXXZSwap_apply_eq_zero_of_magSum_parity_ne, onSiteS_spinSOp2_sq_apply_eq_zero_of_magSum_parity_ne) | Parity block-diagonality of Ĥ' (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3772): with no self-bonds (J x x = 0), the off-diagonal entry Ĥ'_{σ' σ} vanishes when magSumS σ' = Σ_x (σ_x) and magSumS σ have different parities — each bond/single-ion move changes the total occupation by an even amount. Hence Ĥ' is block-diagonal w.r.t. the even/odd magnetization parity, the decomposition on which the parity-sector Perron–Frobenius degeneracy bound runs (PR5). Proved by lifting the bond (#3771) and single-ion (SingleIonOffDiag) parity vanishing through Finset parity bookkeeping (agree-off ⟹ global parity = local parity). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapParityBlock.lean) |
| magParityDiagS, magParityDiagS_mul_self, axisSwappedAnisotropicHeisenbergS_commute_magParityDiagS | Magnetization-parity operator and its commutation with Ĥ' (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3773): the diagonal operator P = diag((−1)^{magSumS σ}) is an involution (P² = 1, eigenvalues ±1); by the parity block-diagonality (#3772), Ĥ' commutes with P (no self-bonds), so the two P-eigenspaces (even/odd magnetization parity) are each Ĥ'-invariant — the decomposition on which the parity-sector Perron–Frobenius degeneracy bound runs. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/MagParityOperator.lean) |
| eigenspace_finrank_le_of_commuting_involution, axisSwappedAnisotropicHeisenbergS_eigenspace_finrank_le_parity_blocks | Eigenspace finrank split under the magnetization-parity involution (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3774): for finite-dimensional T, P with T ∘ P = P ∘ T and P² = id, finrank (eigenspace T μ) ≤ finrank (eigenspace T μ ⊓ eigenspace P 1) + finrank (eigenspace T μ ⊓ eigenspace P (−1)) (via the ½(1 ± P) projection decomposition + finrank subadditivity over ⊔). Applied to Ĥ' and the parity operator P (#3773), this bounds any Ĥ'-eigenspace degeneracy by the sum of its even/odd-parity contributions — reducing the ≤ 2 ground-state bound to ≤ 1 per parity block. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/MagParityEigenspaceDecomp.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_isHermitian_of_real | Hermiticity of the dressed axis-swapped Hamiltonian (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3775): for real J, λ, D, Ĥ'_dressed = Θ_A Ĥ' Θ_A is Hermitian — the conjugation of the Hermitian Ĥ' by the Hermitian (real ±1-diagonal) Marshall sign matrix Θ_A. With the off-diagonal non-positivity (#3770), −Ĥ'_dressed is a real symmetric matrix with non-negative off-diagonal entries — the symmetric Perron–Frobenius input. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapHermitian.lean) |
| axisSwappedAnisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one | ≤ 2 degeneracy of Ĥ' from per-parity-block simplicity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3776): combining the eigenspace finrank split under the parity involution (#3774) with the per-parity-block Perron–Frobenius simplicity (each parity-block restricted μ-eigenspace has dimension ≤ 1), the global Ĥ'-eigenspace has dimension ≤ 2. This isolates the precise remaining Perron–Frobenius obligation (the per-block simplicity hypotheses). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ParityDegeneracyBound.lean) |
| parityConfigS (with parityConfigS_magSumS_parity, Fintype/DecidableEq instances) | Magnetization-parity configuration subtype (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3777): parityConfigS Λ N p = {σ // magSumS σ % 2 = p}, with Fintype/DecidableEq instances (paralleling magConfigS) — the index type on which the Marshall-dressed Ĥ' restricts to a parity block, the foundation for the per-parity-block Perron–Frobenius simplicity. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityConfig.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSOnParityBlock (with _apply, _isHermitian_of_real) | Dressed Ĥ' restricted to a magnetization-parity block (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3778): the submatrix of Ĥ'_dressed on parityConfigS Λ N p (= submatrix Subtype.val Subtype.val). Since Ĥ' is block-diagonal in parity (#3772), these blocks carry its full action; each is Hermitian for real couplings (_isHermitian_of_real), the Perron–Frobenius matrix on which the ≤ 1 per-block degeneracy bound is proved. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedParityBlockMatrix.lean) |
| PerronFrobenius.eigenspace_finrank_le_one_of_pos_eigenvec | Perron eigenspace is at most one-dimensional (Issue #3739, PR #3779): for an irreducible non-negative real matrix A with a strictly positive eigenvector v at μ, the μ-eigenspace of Matrix.toLin' A has finrank ≤ 1 — it is contained in span {v} by geometric simplicity (eigenvec_proportional_of_pos_eigenvec). This is the abstract Perron–Frobenius simplicity bridge (pos_eigenvec proportionality ⟹ finrank ≤ 1) that converts the per-parity-block irreducibility into the ≤ 1 per-block degeneracy needed for Theorem 2.4. (file Math/PerronFrobeniusFinrank.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSReMatrix (with _apply, _isSymm_of_real, _offdiag_nonpos) | Real-part matrix of the dressed Ĥ' (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3780): (σ,σ') ↦ Re(Ĥ'_dressed σ σ'), the real symmetric matrix on which Perron–Frobenius runs. It is symmetric for real couplings (_isSymm_of_real, from dressed Hermiticity #3775) and has non-positive off-diagonal entries for case (i) bipartite AFM (_offdiag_nonpos, #3770) — so a shift c·1 − ReMatrix is entrywise non-negative, the Perron–Frobenius matrix whose top eigenvalue is the dressed ground energy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapPFMatrix.lean) |
| shiftedDressedAxisSwappedReMatrix (with _apply_off_diag, _apply_diag, _isSymm_of_real, _nonneg) | Shifted real-part matrix c·1 − ReMatrix (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3781): the entrywise non-negative Perron–Frobenius matrix — off-diagonal = −ReMatrix ≥ 0 (#3780), diagonal = c − ReMatrix σσ ≥ 0 for c above all diagonal entries (case (i) bipartite AFM). Symmetric for real couplings; _nonneg gives the entrywise ≥ 0. Its top eigenvalue corresponds to the dressed ground energy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapPFMatrix.lean) |
| shiftedDressedAxisSwappedReMatrixOnParityBlock (with _apply, _nonneg, _isSymm_of_real) | Shifted dressed Ĥ' matrix restricted to a parity block (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3782): the submatrix of c·1 − ReMatrix on parityConfigS Λ N p — entrywise non-negative (_nonneg, #3781) and symmetric (_isSymm_of_real) for case (i) bipartite AFM. This is the per-parity-block Perron–Frobenius matrix; combined with parity-block irreducibility and the simplicity bridge (#3779) it yields the ≤ 1 per-block degeneracy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapPFMatrix.lean) |
| shiftedDressedAxisSwappedReMatrix_diag_pos, shiftedDressedAxisSwappedReMatrixOnParityBlock_diag_pos | Strict positivity of the shifted diagonal (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3783): for a strict shift c above every real-part diagonal entry, c·1 − ReMatrix has strictly positive diagonal — the input to the diagonal case of Matrix.isIrreducible_iff_exists_pow_pos ((M^1)_{σσ} > 0) in the parity-block irreducibility proof. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapPFMatrix.lean) |
| ParityStepS, ParityReachableS (with ParityBondStepS, SingleIonStepS, _of_{raiseLower,bond,singleIon}) | Parity-block reachability relation (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3785): the reflexive-transitive closure of the off-diagonal moves of Ĥ' within a magnetization-parity block — transverse hop (RaiseLowerStepS, mag-preserving), bond parity hop (ParityBondStepS, ±2), and single-ion ±2 move (SingleIonStepS). Two configurations connected by ParityReachableS lie in the same parity block; with strictly positive step amplitudes (case (i)) this gives a positive power of the shifted Perron–Frobenius matrix — the input to parity-block irreducibility. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachable.lean) |
| parityStepS_magSumS_parity_eq, parityReachableS_magSumS_parity_eq | Parity-block reachability preserves the magnetization parity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3786): every parity-block move changes magSumS by an even amount (transverse +1,−1; bond hop +1,+1/−1,−1; single-ion ±2), so ParityReachableS configurations have equal magSumS % 2 — the relation is internal to each parity block (well-formedness for the irreducibility argument). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachableMagSum.lean) |
| exists_matrixPow_apply_pos_of_parityReachableS | Matrix-power positivity from parity-block reachability (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3787): for a non-negative matrix B strictly positive on every ParityStepS, ParityReachableS G σ σ' gives some k with 0 < (B^k) σ' σ (by induction on the ReflTransGen chain). Applied to the shifted dressed Perron–Frobenius matrix (strictly positive on the moves, case (i)), this turns parity-block reachability into the matrix-power positivity feeding Matrix.isIrreducible_iff_exists_pow_pos. Parity-block analogue of exists_matrixPow_apply_pos_of_raiseLowerReachableS. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachableMatrixPow.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_eq_zero_of_parity_ne, shiftedDressedAxisSwappedReMatrix_apply_eq_zero_of_parity_ne | Parity block-diagonality of the (shifted) dressed real-part matrix (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3788): the dressed Ĥ' real-part matrix and its shift c·1 − ReMatrix vanish across magnetization-parity classes (magSumS parities differ), inheriting the block-diagonality of Ĥ' (#3772, no self-bonds). So matrix powers restrict cleanly to each parity block — the input letting the parity-block reachability matrix-power positivity (#3787) descend to the parity-block submatrix. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ShiftedDressedAxisSwapBlockDiag.lean) |
| shiftedDressedAxisSwappedReMatrixOnParityBlock_pow_apply | Parity-block matrix powers restrict from the full matrix (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3789): (blockMatrix^k) σ' σ = (fullMatrix^k) σ'.1 σ.1, by induction on k using the parity block-diagonality (#3788) to restrict the matrix-product sum to the block (Finset.sum_subset over the parity filter). This lets the parity-block reachability matrix-power positivity (#3787, on the full matrix) descend to the parity-block submatrix, the input to Matrix.isIrreducible_iff_exists_pow_pos. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ShiftedDressedAxisSwapBlockPow.lean) |
| spinSDotXXZSwap_apply_re_pos_of_raiseLowerStepS_witness | Strict positivity of the axis-swapped bond entry on a RaiseLowerStepS witness, case (i) strict (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3790): for −1 < λ.re ≤ 1 real and a transverse witness on {x, y} (Fin indices oppositely shifted by ±1), Re(spinSDotXXZSwap x y λ N σ' σ) > 0. Ladder-form decomposition: the matching transverse ladder product (Ŝ⁻_x Ŝ⁺_y or Ŝ⁺_x Ŝ⁻_y depending on direction) gives a strict positive real factor at both sites (spinSOpPlus_apply_re_pos_of_raise, spinSOpMinus_apply_re_pos_of_lower); the off-direction transverse, both parity hops, and Ŝ³Ŝ³ vanish by Fin-index mismatch / off-diagonality; coefficient (1 + λ.re)/4 > 0 strict (from λ.re > −1). The bond core of (c) step-positivity for the transverse RaiseLowerStepS move. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AxisSwapBondReStrictPos.lean) |
| dressedAxisSwapped_bond_re_neg_bipartite_x_of_raiseLower_witness, ..._y_... | Strict negativity of the Marshall-dressed axis-swapped bond on a RaiseLowerStepS witness (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3791): for a bipartite bond {x, y} (A-site at either x or y) under case (i) strict (−1 < λ.re ≤ 1 real), the dressed bond entry marshallSignS(σ) · marshallSignS(σ') · spinSDotXXZSwap x y λ σ' σ has strict negative real part. The Marshall sign product equals −1 on any ±1 move on the A-site (#3760), flipping the strict-positive bond entry (#3790) to strict-negative. The per-bond ingredient of the full dressed-Ĥ' strict negativity on a transverse step. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapBondReStrictNeg.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_apply_re_neg_of_raiseLowerStepS_witness_bipartite, shiftedDressedAxisSwappedReMatrix_apply_pos_of_raiseLowerStepS_bipartite | Full dressed Ĥ' strict negativity & shifted PF strict positivity on a transverse step (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3792): for a RaiseLowerStepS on bipartiteCompleteGraphOf A under case (i) strict (−1 < λ.re ≤ 1 real, D.re ≥ 0), Re(dressed Ĥ' τ σ) < 0 and shiftedDressedAxisSwappedReMatrix A J λ D N c τ σ > 0. Strictness comes from the matching (x, y) bond by #3791; all other per-bond contributions (#3770’s _bipartite_x/y) and the dressed single-ion (#3770’s dressed_singleIonAnisotropyS2_re_nonpos) are non-positive. The double sum is closed via a Finset.sum_neg_of_forall_nonpos_of_exists_neg helper, applied nested over the outer and inner sums. This is the hB_step of Matrix.isIrreducible_iff_exists_pow_pos for the transverse RaiseLowerStepS move in PR5 (parity-block Perron–Frobenius irreducibility). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapRaiseLowerStrictNeg.lean) |
| shiftedDressedAxisSwappedReMatrix_apply_pos_of_parityBondStepS_bipartite | Shifted PF strict positive on a bond parity step (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3793): for a ParityBondStepS (both endpoints of a bond shifted in the same Fin direction by ±1) on bipartiteCompleteGraphOf A under case (i) strict² (−1 < λ.re < 1 real, D.re ≥ 0), the shifted matrix entry is strict positive. Parallels the transverse step (#3792) with the parity ladder product (Ŝ⁻Ŝ⁻ for both-raised, Ŝ⁺Ŝ⁺ for both-lowered) replacing the transverse ladder; coefficient (1 − λ.re)/4 > 0 strict from λ.re < 1; the same nested Finset.sum_neg_of_forall_nonpos_of_exists_neg assembly. The hB_step of Matrix.isIrreducible_iff_exists_pow_pos for the bond-parity ±2-move. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapParityBondStrictPos.lean) |
| shiftedDressedAxisSwappedReMatrix_apply_pos_of_singleIonStepS | Shifted PF strict positive on a single-ion step (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3794): for a SingleIonStepS witness (same-site ±2-move at some x) under case (i.2) (real λ, real D > 0 strict), the shifted matrix entry is strict positive. Bond contributions all vanish: either x ∉ {a, b} ⟹ NOT agree-off-{a, b}; or x ∈ {a, b} ⟹ no single ladder operator (Ŝ⁺, Ŝ⁻, Ŝ³) connects ±2-shifted Fin indices. Single-ion contribution: only y = x survives (off-x δ-product vanishes); (Ŝ²)²(i, j).re = −(1/4) · ((Ŝ⁺)² + (Ŝ⁻)²)(i, j).re < 0 strict (one of the two parity-square ladder products strict positive). Marshall sign at same-site even (±2) shift = +1 (no flip). The hB_step of Matrix.isIrreducible_iff_exists_pow_pos for the single-ion ±2-move. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapSingleIonStrictPos.lean) |
| shiftedDressedAxisSwappedReMatrix_apply_pos_of_parityStepS_bipartite | Unified ParityStepS strict positivity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3795): for any ParityStepS = RaiseLowerStepS ∨ ParityBondStepS ∨ SingleIonStepS on bipartiteCompleteGraphOf A under case (i.2) strict (−1 < λ.re < 1 real, real D > 0 strict), the shifted matrix entry is strict positive. Case-splits on the move type and dispatches to #3792 / #3793 / #3794. The unified hB_step of Matrix.isIrreducible_iff_exists_pow_pos. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapParityStepStrictPos.lean) |
| shiftedDressedAxisSwappedReMatrixOnParityBlock_pow_apply_pos_of_parityReachable | Block matrix power positivity from parity reachability (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3796): for any ParityReachableS σ.1 σ'.1 between two parity-block configurations under case (i.2) strict (−1 < λ.re < 1 real, real D > 0 strict, c above all diagonal entries), ∃ k, (parityBlockMatrix^k) σ' σ > 0. Combines the unified ParityStepS strict positivity (#3795) + the path-positivity lift on the full matrix (#3787, applying #3782 nonneg + #3795 step-pos) + the block-power-from-full identity (#3789). The per-pair pow positivity input of Matrix.isIrreducible_iff_exists_pow_pos — modulo the remaining (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapBlockPowPos.lean) |
| shiftedDressedAxisSwappedReMatrixOnParityBlock_isIrreducible_of_parityReachable_total | Parity-block matrix is irreducible (conditional on reachability totality) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3797): under case (i.2) strict (−1 < λ.re < 1 real, real D > 0 strict, c strict above all diagonal entries) and reachability totality (every two distinct same-parity configs ParityReachableS-connected), the parity-block shifted PF matrix is Matrix.IsIrreducible. Diag pos at k=1 (#3783); off-diag via #3796 + a k ≥ 1 extraction (since k=0 ⟹ 1 σ' σ = 0 contradicts > 0). The irreducibility step (e) of PR5 modulo the remaining (d). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapBlockIrreducible.lean) |
| raiseLowerStepS_pair_shift_{lower_a_raise_b,raise_a_lower_b}, parityBondStepS_pair_{raise,lower}, singleIonStepS_{raise,lower} | Concrete witness constructors for ParityStepS (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3798): explicit σ → σ' move witnesses for RaiseLowerStepS (Fin index ±1 swap on a bipartite edge), ParityBondStepS (both Fin indices ±1 together on a bipartite edge), and SingleIonStepS (same-site ±2-move). The foundational building blocks for (d) reachability totality: each lemma gives an explicit configUpdateOne/Two target plus a short Step witness, used to assemble ParityReachableS chains. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachWitness.lean) |
| parityReachableS_shuffle_a_to_aprime_via_b | A-side magnetization shuffle via a B-site (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3799): for a, a' on the same sublattice opposite to b, a ≠ a', with 1 ≤ σ a, σ a' + 1 ≤ N, σ b + 1 ≤ N, the two-step transverse chain (a, b)-lower-a-raise-b then (a', b)-raise-a’-lower-b transfers one unit from a to a' (with b returning to its original value). The canonical “use the opposite sublattice as a temporary store” trick for the bipartite complete graph — used in subsequent reachability totality bricks. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachShuffle.lean) |
| parityReachableS_shuffle_n_units | Iterated n-unit shuffle (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3800): from σ with n ≤ σ a, σ a' + n ≤ N, σ b + 1 ≤ N, the config shifting n units from a to a' is ParityReachableS-reachable. Proven by induction on n composing the single-unit shuffle (#3799) n times. The magnitude-iterating piece of (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachShuffleIter.lean) |
| parityReachableS_transfer_n_units | Iterated n-unit cross-sublattice transfer (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3801): from σ with n ≤ σ a and σ b + n ≤ N on a bipartite bond (a, b), the config shifting n units from a to b is ParityReachableS-reachable. Proven by induction on n composing single transverse moves at the same bond. The cross-sublattice analogue of the iterated shuffle (#3800) and another foundational primitive for (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachTransferIter.lean) |
| parityReachableS_drain_a_into_a0 | Drain a into a₀ via the iterated shuffle (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3802): starting from σ, the config with σ' a = 0 and σ' a₀ = (σ a₀).val + (σ a).val (with b net unchanged and everything else unchanged) is ParityReachableS-reachable provided (σ a₀).val + (σ a).val ≤ N and (σ b).val + 1 ≤ N. Specialises the n-unit shuffle (#3800) to n = (σ a).val. The “drain one site” primitive for the multi-site concentration argument of (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachDrainOne.lean) |
| parityReachableS_drainSetInto | Multi-site concentration via iterated drain (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3803): for a finite set S of sites disjoint from a₀ and adjacent to b (and a₀ adjacent to b), starting from σ with (σ a₀).val + ∑_{s∈S} (σ s).val ≤ N and (σ b).val + 1 ≤ N, the config that drains every s ∈ S (setting σ' s = 0) into a₀ (setting σ' a₀ = (σ a₀).val + ∑_{s∈S} (σ s).val) is ParityReachableS-reachable. Proven by Finset.induction_on generalizing σ over S, composing single drains (#3802). The multi-site concentration primitive for (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachConcentrate.lean) |
| parityReachableS_concentrate_A_at_a0 | A-side concentration at a₀ (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3804): starting from σ with a₀ ∈ A and a B-site b ∉ A, the config that drains every A-site a ≠ a₀ into a₀ is ParityReachableS-reachable. Specialises #3803 with S = aSitesExcept A a₀ = Finset.univ.filter (fun v => A v = true ∧ v ≠ a₀). Hypotheses: A a₀, ¬ A b, (σ a₀).val + ∑_{s ∈ aSitesExcept A a₀} (σ s).val ≤ N, (σ b).val + 1 ≤ N. The A-side half of the canonical-representative reduction in (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachConcentrateA.lean) |
| parityReachableS_concentrate_B_at_b0 | B-side concentration at b₀ (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3805): symmetric to #3804 with A/B swapped. Starting from σ with b₀ ∉ A (B-side) and an A-site a ∈ A as temporary store, the config that drains every B-site b ≠ b₀ into b₀ is ParityReachableS-reachable. Hypotheses: ¬ A b₀, A a, (σ b₀).val + ∑_{s ∈ bSitesExcept A b₀} (σ s).val ≤ N, (σ a).val + 1 ≤ N. The B-side half of the canonical-representative reduction in (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachConcentrateB.lean) |
| parityReachableS_concentrate_AB | Combined A+B concentration to a two-site canonical form (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3806): composing #3804 (A-concentration via b₀ as temp) with #3805 (B-concentration via the post-A-concentration a₀ ∈ A as temp). The resulting σ_AB has σ_AB a₀ = (σ a₀).val + Σ_{aSitesExcept} (σ s).val (total A-mass), σ_AB b₀ = (σ b₀).val + Σ_{bSitesExcept} (σ s).val (total B-mass), and σ_AB = 0 on aSitesExcept ∪ bSitesExcept. Hypotheses: A a₀, ¬ A b₀, A/B totals fit at their targets, plus (σ b₀).val + 1 ≤ N (room at b₀ for A-concentration) and (σ a₀).val + Σ_{aSitesExcept} (σ s).val + 1 ≤ N (room at the post-concentration a₀ for B-concentration). The two-site canonical form target for (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachConcentrateAB.lean) |
| parityReachableS_canonical_transfer | Canonical-to-canonical reachability at the same total magnetization (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3807): from a two-site canonical config (mass concentrated at (a₀, b₀)), an iterated transverse at the canonical bond (a₀, b₀) transfers n units between a₀ and b₀, preserving the canonical shape (= 0 elsewhere) and the total m_A + m_B. A semantically-renamed specialisation of #3801 used as a black-box in the canonical-to-canonical chain of (d) reachability totality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachCanonicalTransfer.lean) |
| parityReachableS_canonical_singleIon{Raise,Lower}_{a,b} | Canonical ±2 magSum shift via single-ion at a₀/b₀ (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3808): wraps the SingleIonStepS witnesses (#3798) as ParityReachableS single steps at either endpoint of the canonical bond. Used in the canonical chain of (d) reachability totality to change the total magnetization by ±2 (preserving parity). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/ParityReachCanonicalMagShift.lean) |
| complex_dressed_parity_block_submatrix_eigenspace_finrank_le_one | (f.3-finish) complex dressed parity-block submatrix finrank ℂ ≤ 1 at the PF eigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3831): combines the parity-block real-form Perron–Frobenius simplicity (...ReMatrixOnParityBlock_eigenspace_finrank_le_one, #3827) with the real-to-complex eigenspace bridge matrix_complex_eigenspace_finrank_le_one_of_real (#3828) via the matrix identity (dressed_re.submatrix valS valS).map ((↑) : ℝ → ℂ) = dressed_complex.submatrix valS valS — which holds because every entry of dressed_complex is real under real coefficients (#3830 dressedAxisSwappedAnisotropicHeisenbergS_apply_im_zero lifting #3829 axisSwappedAnisotropicHeisenbergS_apply_im_zero through the Marshall sign factors). Statement: under physical hyps on J, lam, D, ∃ ν : ℝ, finrank ℂ (eig dressed_Ĥ'.submatrix valS valS) (ν : ℂ) ≤ 1 for the parity-p submatrix. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ComplexDressedParityBlockFinrank.lean) |
| parity_block_full_eigenspace_inter_finrank_le_submatrix (with parityRestrictMap, ker_magParityDiagS_apply_eq_zero_of_parity_ne, sum_parityConfigS_eq_sum_filter) | (f.4) block-diag bridge (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3832): for a parity-block-diagonal complex matrix M, the restriction-to-parity-p map parityRestrictMap : (eig M ν ⊓ ker(P=(-1)^p)) →ₗ[ℂ] eig (M.submatrix valS valS) ν is injective (image lands in the submatrix eigenspace via the block-diag identity; injectivity uses that vectors in ker(P=(-1)^p) vanish off parityConfigS p). Hence finrank ℂ (eig M ν ⊓ ker(P=(-1)^p)) ≤ finrank ℂ (eig M.submatrix ν) for p < 2. The bridge for lifting the per-block PF bound (#3831) to the full eigenspace ⊓ parity ker. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BlockDiagSubmatrixBridge.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one (with ..._apply_eq_zero_of_magSum_parity_ne, ..._commute_magParityDiagS, ..._eigenspace_finrank_le_parity_blocks) | (g.1) dressed Ĥ' eigenspace finrank ℂ ≤ 2 via parity-block decomposition (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3833): the dressed axis-swapped Hamiltonian (i) inherits parity-block-diagonality from the bare via dressed σ τ = m_A(σ) m_A(τ) * bare σ τ, (ii) commutes with P = magParityDiagS entrywise (since Θ_A and P are both diagonal, hence the entire Θ_A Ĥ' Θ_A commutes with P), (iii) so eigenspace_finrank_le_of_commuting_involution (#3776) applies and the eigenspace splits across ±1 parity blocks. Given per-block ≤ 1 bounds, full dressed eig ≤ 2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedAxisSwapDegeneracyBound.lean) |
| dressed_full_eigenspace_inter_parity_finrank_le_one | (g.2) dressed Ĥ' per-block full-eigenspace finrank ℂ ≤ 1 at the PF ν (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3834): combines #3831 (parity-submatrix eig ≤ 1) with #3832 (block-diag bridge) under the dressed parity-block-diagonality (#3833 step 1). Result: ∃ ν : ℝ, finrank ℂ (eig dressed_Ĥ' ν ⊓ ker(P=(-1)^p)) ≤ 1 for p < 2. The per-block input consumed by the dressed eig ≤ 2 assembly. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedFullEigInterParityLeOne.lean) |
| matrix_similar_eigenspace_inter_finrank_eq | (g.3) similarity-invariant intersection eigenspace finrank (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3835): generalises matrix_similar_eigenspace_finrank_eq (#3746 family) to intersections with a second operator’s eigenspace, provided the similarity U commutes with that operator Q. Given U * Uinv = 1, Uinv * U = 1, H' = Uinv * H * U, AND Q * U = U * Q, then finrank ℂ (eig H' μ ⊓ ker(Q=c)) = finrank ℂ (eig H μ ⊓ ker(Q=c)). The core technical step for transferring per-parity-block PF bounds from the dressed Ĥ'_dressed to the bare Ĥ', since the Marshall sign diagonal Θ_A commutes with the diagonal magParityDiagS P. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/GaugeIntersectionEigenspaceFinrank.lean) |
| bare_axisSwapped_full_eigenspace_inter_parity_finrank_le_one (with marshallDiagonal_commute_magParityDiagS) | (g.4) bare Ĥ' per-block PF finrank ℂ ≤ 1 via Marshall similarity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3836): transfers the dressed Ĥ'_dressed per-block bound (#3834) to the bare axis-swapped Ĥ' via the Marshall similarity for intersected eigenspaces (#3835). Key observation: the Marshall sign diagonal Θ_A and the magnetization parity diagonal P = magParityDiagS are both diagonal and hence commute, so the intersection eig Ĥ' μ ⊓ ker(P=c) is preserved by the Marshall similarity dressed → bare. Result for p < 2: ∃ ν : ℝ, finrank ℂ (eig (axisSwappedAnisotropicHeisenbergS J lam D N) (ν : ℂ) ⊓ ker(P=(-1)^p)) ≤ 1. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareAxisSwapFullEigInterParityLeOne.lean) |
| anisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one (with spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one) | (g.5) bare anisotropic Ĥ eigenspace finrank ℂ ≤ 2 (conditional, via axis-swap) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3837): wraps the conditional bare Ĥ' eig ≤ 2 from per-block ≤ 1 (axisSwappedAnisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one, #3776 family) with the axis-swap unitary equivalence (AxisSwapUnitaryS.anisotropic_axisSwapped_eigenspace_finrank_eq, #3753) to give the same conditional bound for the bare anisotropic Hamiltonian Ĥ. General N version requires an explicit AxisSwapUnitaryS N instance; spin-1/2 (N = 1) instance via axisSwapUnitarySpinHalf. This closes the bare Ĥ ≤ 2 link in the (g) chain, conditional on per-parity-block PF hypotheses (discharged separately per sector by #3836). The remaining gap to unconditional obligation (1) is the ν-sector matching (PF eigenvalues of even/odd sectors coinciding at the ground-state energy), which is mathematically distinct (Hermitian spectral minimisation) and deferred. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareAnisotropicEigLeTwoConditional.lean) |
| parity_block_submatrix_full_inter_finrank_eq (with parity_block_submatrix_eigenspace_finrank_le_full_inter, parityEmbedMap) | (h.1) reverse block-diag bridge (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3840): for a parity-block-diagonal complex M, the parity-p submatrix’s ν-eigenspace embeds INJECTIVELY into eig M ν ⊓ ker(P=(-1)^p) via the zero-extension map (extend by 0 off parityConfigS p). Combined with the forward direction (#3832), gives the finrank equality finrank ℂ (eig M.submatrix ν) = finrank ℂ (eig M ν ⊓ ker(P=(-1)^p)) for p < 2. The equality unlocks ν-sector matching arguments: per-block submatrix eig finrank equals the full eig ⊓ ker(P) finrank, so per-sector PF simplicity (#3834/#3836) directly transfers to constraints on the FULL eigenspace at that energy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BlockDiagSubmatrixEmbed.lean) |
| eigenspace_finrank_eq_of_commuting_involution | (h.2) involution eigenspace decomposition — finrank EQUALITY (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3841): strengthens eigenspace_finrank_le_of_commuting_involution (#3776) from ≤ to =. For finite-dim T, P with T∘P = P∘T and P∘P = id, the T-eigenspace at any μ splits as a direct sum across the two P-eigenspaces ±1. The ≤ was tight because the two intersected ±1 eigenspaces of P are disjoint (a single eigenvector cannot have two distinct P-eigenvalues), so Submodule.finrank_sup_add_finrank_inf_eq collapses to a sum (inf = 0). Used by (h.3) to derive the block-sum equality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/InvolutionEigenspaceDecompEq.lean) |
| matrix_eigenspace_finrank_eq_sum_parity_blocks (with dressedAxisSwappedAnisotropicHeisenbergS_..._sum_parity_blocks, axisSwappedAnisotropicHeisenbergS_..._sum_parity_blocks) | (h.3) block-sum finrank equality (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3842): combines (h.1) #3840 and (h.2) #3841 to give the block-sum equality for any parity-block-diagonal M commuting with magParityDiagS: finrank ℂ (eig M μ) = finrank ℂ (eig M.submatrix_0 μ) + finrank ℂ (eig M.submatrix_1 μ). Specialised to the dressed Ĥ'_dressed and the bare Ĥ' (both block-diagonal and commuting with P). Central tool for unconditional ≤ 2 at any μ where both per-block bounds hold simultaneously. Combined with PF (per-sector simplicity at the per-sector spectrum minimum) and a Hermitian spectral identification of the GS energy as min(ν_0, ν_1), gives the unconditional bare Ĥ' GS degeneracy ≤ 2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BlockSumFinrankEq.lean) |
| matrix_eigenspace_finrank_le_two_of_submatrix_blocks_le_one (with dressedAxisSwappedAnisotropicHeisenbergS_..._of_submatrix_blocks, axisSwappedAnisotropicHeisenbergS_..._of_submatrix_blocks_le_one, anisotropicHeisenbergS_..._of_submatrix_blocks_le_one, spinHalf_..._of_submatrix_blocks_le_one) | (h.4) ≤ 2 wrappers from per-block submatrix simplicity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3844): wraps (h.3) #3842 into easier-to-use forms for consumers of per-sector PF simplicity. Hypotheses stated on the SUBMATRIX eigenspaces (directly produced by #3831/#3836), bypassing the eig ⊓ ker(P) intersection form. 5 theorems: generic block-diag wrapper, dressed Ĥ’, bare Ĥ’, bare Ĥ via AxisSwapUnitaryS N, and spin-1/2 specialisation. Proofs via (h.3) sum equality + omega; the bare anisotropic Ĥ versions additionally use the axis-swap unitary equivalence (#3753 family). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/SubmatrixSimpleEigLeTwo.lean) |
| axisSwappedAnisotropicHeisenbergS_submatrix_isHermitian_of_real (with dressedAxisSwappedAnisotropicHeisenbergS_submatrix_isHermitian_of_real) | (i.1) parity-block submatrix Hermiticity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3846): the parity-p submatrix of the bare and dressed axis-swapped Hamiltonians inherits Hermiticity from the full Hamiltonian via Matrix.IsHermitian.submatrix. Starting point for Hermitian spectral analysis of the per-sector matrix — needed to identify the per-sector PF eigenvalue as the spectrum minimum and ultimately bridge the conditional ≤ 2 (g/h chains) to the unconditional ground-state degeneracy bound. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ParityBlockSubmatrixHermitian.lean) |
| hermitian_eigenvalue_im_zero (with axisSwappedAnisotropicHeisenbergS_submatrix_eigenvalue_im_zero, dressedAxisSwappedAnisotropicHeisenbergS_submatrix_eigenvalue_im_zero) | (i.2) submatrix eigenvalue realness (Hermitian) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3847): parity-p submatrix of the bare/dressed axis-swapped Hamiltonian has all eigenvalues real (μ.im = 0). Combines (i.1) #3846 with the existing isHermitian_eigenvalue_star_eq. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/SubmatrixEigenvalueReal.lean) |
| hermitianMinEigenvalue (with hermitian_min_eigenvalue_mem_image, hermitian_min_eigenvalue_le, axisSwappedAnisotropicHeisenbergS_submatrix_min_eigenvalue, dressedAxisSwappedAnisotropicHeisenbergS_submatrix_min_eigenvalue) | (i.3) submatrix minimum eigenvalue (Hermitian) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3848): for a Hermitian matrix M on a non-empty finite-dim space, the minimum of its eigenvalue function (Matrix.IsHermitian.eigenvalues) is well-defined as a real number via Finset.min'. The min is in the image of the eigenvalue function (hence one of the eigenvalues) and ≤ every eigenvalue. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/SubmatrixMinEigenvalue.lean) |
| hermitian_eigenspace_eq_bot_of_real_lt_min | (i.4) Hermitian eigenspace = ⊥ below min eigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3849): for a Hermitian matrix M on a finite-dim complex space, if μ < hermitianMinEigenvalue M, then the eigenspace at (μ : ℂ) is ⊥. Proof via spectrum-eigenvalues bridge (HasEigenvalue.mem_spectrum → Matrix.spectrum_toLin' → spectrum.algebraMap_mem_iff → IsHermitian.spectrum_real_eq_range_eigenvalues). Rules out eigenvalues below the minimum. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/HermitianEigenspaceBotBelowMin.lean) |
| matrix_eigenspace_eq_bot_of_real_lt_both_block_mins (with axisSwappedAnisotropicHeisenbergS_eigenspace_eq_bot_of_real_lt_both_block_mins) | (i.5) block-diag eigenspace = ⊥ below joint per-block minimum (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3850): for a parity-block-diagonal M commuting with magParityDiagS, if μ : ℝ is strictly less than the minimum eigenvalues of BOTH per-block submatrices, then the full eigenspace at (μ : ℂ) is ⊥. Combines (h.3) #3842 + (i.4) #3849. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BlockEigBotBelowJointMin.lean) |
| matrix_eigenspace_finrank_le_two_at_min_block_mins | (i.6) full eig ≤ 2 at min(per-block mins) given per-block ≤ 1 at min (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3851): the FINAL assembly step. Given per-block bounds finrank ≤ 1 at the per-block minimum eigenvalues, the full-eigenspace at min(min_0, min_1) has finrank ≤ 2. Case analysis: min_0 = min_1 both contribute ≤ 1; min_0 ≠ min_1 the higher block contributes 0 by (i.4) #3849, the lower ≤ 1. Bridge from per-block PF simplicity to the unconditional global ground-state degeneracy ≤ 2 (modulo identification of PF eigenvalue with hermitianMinEigenvalue). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BlockMinLeTwo.lean) |
| axisSwappedAnisotropicHeisenbergS_eigenspace_finrank_le_two_at_min_block_mins | (i.7) bare Ĥ' eig ≤ 2 at min(per-block mins) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3854): specialises (i.6) #3851 to the bare axis-swapped anisotropic Heisenberg Ĥ'. Discharges the block-diag (via axisSwapped_apply_eq_zero_of_magSum_parity_ne) and commute (via axisSwapped_commute_magParityDiagS) hypotheses inline. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareAxisSwapMinLeTwo.lean) |
| anisotropicHeisenbergS_eigenspace_finrank_le_two_at_min_block_mins (with spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_at_min_block_mins) | (i.8) bare anisotropic Ĥ eig ≤ 2 at min(per-block mins) via axis-swap (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3855): wraps (i.7) #3854 with the axis-swap unitary equivalence (#3753 family AxisSwapUnitaryS.anisotropic_axisSwapped_eigenspace_finrank_eq) to lift the bound to the bare anisotropic Hamiltonian Ĥ. General N version requires an AxisSwapUnitaryS N instance; spin-1/2 (N = 1) instance via axisSwapUnitarySpinHalf. Analogue of (g.5) #3837 with per-block-min hypotheses threading the Hermitian spectral chain — the remaining gap is identification of the per-sector PF eigenvalue with hermitianMinEigenvalue submatrix_p (which would discharge h0/h1 to yield the unconditional ground-state degeneracy ≤ 2 for bare anisotropic Ĥ). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareAnisotropicMinLeTwo.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSReMatrixOnParityBlock_pos_eigenvector_exists | (j.1) PF positive eigenvector for unshifted dressed-Ĥ' submatrix (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3857): from PF on the shifted parity-block matrix (B = c·I − M for M = dressed_re.submatrix), the PF positive eigenvector v > 0 is also a positive eigenvector of the un-shifted matrix M at ν = c − μ_PF. The existence half of the identification ν = hermitianMinEigenvalue M. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedSubmatrixPFEigenvectorStructural.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_submatrix_complex_eigenvector_exists | (j.2) Lift PF eigenvector to complex dressed submatrix (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3858): lifts (j.1) #3857 (positive real eigenvector for the real-form dressed submatrix) to the complex form via Complex.ofReal. Uses the matrix identity #3831 (dressed_re.submatrix).map ofReal = dressed_complex.submatrix. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/ComplexDressedSubmatrixPFEigenvector.lean) |
| hermitian_min_eigenvalue_le_of_eigenvector_exists | (j.3) hermitianMinEigenvalue ≤ μ from eigenvector existence (Hermitian) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3859): for a Hermitian matrix M on a non-empty finite-dim complex space, if w ≠ 0 satisfies M w = (μ : ℂ) w (for some μ : ℝ), then hermitianMinEigenvalue M ≤ μ. Proof: contrapositive of (i.4) #3849. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/HermitianMinLeOfEigenvector.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_submatrix_min_le_pf_eigenvalue | (j.4) Package PF eigenvector + hermitianMinEigenvalue ≤ ν (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3860): combines (j.2) #3858 + (j.3) #3859 into ∃ ν : ℝ, hermitianMinEigenvalue ≤ ν ∧ ∃ w ≠ 0, dressed.submatrix *ᵥ w = (ν : ℂ) • w. ONE-DIRECTION half of the per-block identification. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedSubmatrixPFAtMin.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_submatrix_finrank_le_one_at_min_conditional | (j.5) Per-block bound at hermitianMinEigenvalue (conditional) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3861): given a specific ν : ℝ with the PF bound AND ν = hermitianMinEigenvalue, the bound transfers to (hermitianMinEigenvalue : ℂ). Consumer-friendly form for (i.7) #3854’s per-block hypotheses — once the PF = min identification is proven, this discharges (i.7)’s hypotheses unconditionally. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedSubmatrixBoundAtMin.lean) |
| hermitianMinEigenvalue_eq_of_spectrum_eq | (j.6) hermitianMinEigenvalue agrees under same ℝ-spectrum (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3863): for two Hermitian matrices with the same ℝ-spectrum, hermitianMinEigenvalue is the same. Proof via spectrum_real_eq_range_eigenvalues. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/HermitianMinSimilarInvariance.lean) |
| matrix_similar_spectrum_complex_eq (with matrix_similar_spectrum_real_eq) | (j.7) Spectrum equality under matrix similarity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3864): for similar matrices M' = Uinv * M * U, spectrum ℂ M = spectrum ℂ M' (and spectrum ℝ ditto). Proof: bridge spectrum ↔ HasEigenvalue + finrank equality from #3746. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/MatrixSimilaritySpectrum.lean) |
| bare_dressed_submatrix_hermitianMinEigenvalue_eq (with marshallDiagonalOnParity, marshallDiagonalOnParity_mul_self, dressedAxisSwapped_submatrix_eq_marshall_conj_bare) | (j.8) Marshall submatrix similarity → bare/dressed equal hermitianMinEigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3865): the Marshall sign diagonal Θ_A restricted to parityConfigS Λ N p gives a similarity dressed.submatrix = Θ_p * bare.submatrix * Θ_p. Combined with (j.6) + (j.7), hermitianMinEigenvalue bare.submatrix = hermitianMinEigenvalue dressed.submatrix. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/MarshallSubmatrixMinEq.lean) |
| axisSwappedAnisotropicHeisenbergS_submatrix_pf_eigenspace_finrank_le_one | (j.10) Bare submatrix finrank ≤ 1 at PF ν via Marshall similarity (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3868): combines #3831 (dressed submatrix finrank ≤ 1 at PF ν) with matrix_similar_eigenspace_finrank_eq (#3746) and the Marshall similarity (j.8) #3865 to give the bare submatrix ∃ ν : ℝ, finrank ℂ (eigenspace bare.submatrix (ν : ℂ)) ≤ 1. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareSubmatrixPFFinrank.lean) |
| axisSwappedAnisotropicHeisenbergS_submatrix_finrank_le_one_at_min_conditional | (j.11) Bare submatrix finrank ≤ 1 at hermitianMinEigenvalue (conditional) (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3869): bare-side analogue of (j.5) #3861. Given a specific ν with both the bare-side PF bound (from (j.10) #3868) and ν = hermitianMinEigenvalue bare.submatrix (the deferred PF=min identification), the bound transfers to (hermitianMinEigenvalue : ℂ). Consumer-friendly form for (i.7) #3854’s h0/h1 per-parity hypotheses. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareSubmatrixBoundAtMin.lean) |
| anisotropicHeisenbergS_eigenspace_finrank_le_two_at_min_block_mins (with spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_at_min_block_mins) | (j.12) Capstone: bare anisotropic Ĥ ≤ 2 modulo PF=min identification (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3870): wraps the bare Ĥ' per-parity ≤ 1 at hermitianMinEigenvalue (conditional via (j.11)) with the axis-swap unitary equivalence (anisotropic_axisSwapped_eigenspace_finrank_eq, #3753 family) to give finrank ℂ (eigenspace Ĥ (min(ν_0, ν_1) : ℂ)) ≤ 2. General N version requires an AxisSwapUnitaryS N instance; spin-1/2 (N = 1) instance via axisSwapUnitarySpinHalf. Still conditional on the PF=min h0/h1 per-parity inputs. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareAnisotropicMinLeTwo.lean) |
| rayleigh_quotient_at_eigenvector | (j.13.a) Rayleigh quotient at PF eigenvector = μ (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3872): for a real matrix M with a nonzero eigenvector v at eigenvalue μ, (∑ i, v i * (M *ᵥ v) i) / (∑ i, v i * v i) = μ. Foundational step of the (j.13) Collatz-Wielandt chain identifying the Perron-Frobenius eigenvalue with the maximum Hermitian eigenvalue. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/RayleighAtEigenvector.lean) |
| hermitianMaxEigenvalue (with hermitian_max_eigenvalue_mem_image, hermitian_eigenvalue_le_max) | (j.13.b) hermitianMaxEigenvalue definition + existence (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3873): for a non-empty Hermitian matrix M : Matrix n n ℂ, hermitianMaxEigenvalue hM := (Finset.univ.image hM.eigenvalues).max'. Mirror of hermitianMinEigenvalue for the maximum side. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianMaxEigenvalue.lean) |
| hermitian_eigenspace_eq_bot_of_real_gt_max | (j.13.c) Hermitian eigenspace = ⊥ above max eigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3874): for a Hermitian matrix M on a non-empty finite-dim complex space, if hermitianMaxEigenvalue M < μ, then End.eigenspace (toLin' M) (μ : ℂ) = ⊥. Mirror of (i.4) #3849. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianEigenspaceBotAboveMax.lean) |
| hermitian_max_eigenvalue_ge_of_eigenvector_exists | (j.13.d) hermitianMaxEigenvalue ≥ μ from eigenvector existence (Hermitian) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3875): for a Hermitian matrix M on a non-empty finite-dim complex space, if w ≠ 0 satisfies M w = (μ : ℂ) w (for some μ : ℝ), then μ ≤ hermitianMaxEigenvalue M. Proof: contrapositive of (j.13.c). Mirror of (j.3) #3859. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianMaxGeOfEigenvector.lean) |
← Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) · Catalogue · Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) →