LatticeSystem/Fermion/JordanWigner.lean is a façade module
re-exporting the full Jordan–Wigner machinery. Following the refactor
plan v4 §3.1 (Phase 2 PR 10–14), it is a thin re-import of the sub-files
under LatticeSystem/Fermion/JordanWigner/ (originally five core files;
further extended with single-mode-mirror and Hubbard algebra lemmas during
the 2026-05-04 autonomous fermion expansion). Old
import LatticeSystem.Fermion.JordanWigner continues to work unchanged via
this façade (see docs/refactoring-conventions.md §2 “Façade module policy”).
The table below is the per-sub-file overview (one row per sub-module). It was moved here verbatim from the façade module’s header so that the module itself stays under the long-line / long-file style budget; each sub-module’s own doc comment remains the primary source for its contents.
| sub-file | content |
|---|---|
String.lean |
JW string fundamentals |
Operators.lean |
multi-mode c_i, c_i†, on-site CAR, hermiticity, number op |
CAR.lean |
full canonical anticommutation (same-site + cross-site, factorisations) |
CAR/CrossSiteOfNe.lean |
symmetric _of_ne cross-site CAR (4 lemmas) |
Number.lean |
number commutators, Hubbard skeleton, fermion vacuum |
FockProduct.lean |
(model-agnostic) generic move-through lemmas for operator products on the JW vacuum: anticomm_listProd_mulVec_vacuum, charge_listProd_mulVec_vacuum, dualAnnihilation_peel_listProd_mulVec_vacuum (reusable across flat-band models) |
NumberAnticommutators.lean |
same-site {n_i, c_i}, {n_i, c_i†} anticommutators |
NumberPow.lean |
n_i^(k+1) = n_i (idempotent projection power) |
CDaggerCCommutator.lean |
same-site [c_i, c_i†] = 1 − 2·n_i |
CDaggerCIdentity.lean |
same-site c_i · c_i† = 1 − n_i, n_i + c_i · c_i† = 1 |
CDaggerCProjection.lean |
hole-projection idempotency (c_i · c_i†)² = c_i · c_i† + powers |
CDaggerCHermitian.lean |
hole projection Hermitian (c_i · c_i†)ᴴ = c_i · c_i† |
ProjectionsOrthogonal.lean |
n_i · (c_i · c_i†) = 0, (c_i · c_i†) · n_i = 0 |
ProjectionsCommute.lean |
Commute n_i (c_i · c_i†) (both products zero) |
AnnihilationNumberIdentities.lean |
n_i · c_i = 0, c_i · n_i = c_i |
CreationNumberIdentities.lean |
c_i† · n_i = 0, n_i · c_i† = c_i† |
PartialIsometry.lean |
c_i · c_i† · c_i = c_i, c_i† · c_i · c_i† = c_i† |
HoleProjectionsCommute.lean |
Commute (c_i · c_i†) (c_j · c_j†) for any i, j |
HoleProjectionCommuteLadder.lean |
Commute (c_i · c_i†) c_j and …c_j† for i ≠ j |
HoleProjectionCommuteNumber.lean |
Commute (c_i · c_i†) n_j for any i, j |
CDaggerCLadderZero.lean |
c_i · (c_i · c_i†) = 0, (c_i · c_i†) · c_i† = 0 |
Hubbard.lean |
spinful wrappers, on-graph Hubbard, 1D open / periodic chain Gibbs |
Hubbard/Charges.lean |
N_↑, N_↓, S^z_tot, vacuum eigenstates, cross-spin commutes |
Hubbard/Graph.lean |
graph-centric wrappers, chain/cycle Hamiltonians + Gibbs families |
Hubbard/SpinSymmetryAux.lean |
(split from SpinSymmetry) U(1)×U(1) auxiliary: Hermiticity/adjoints of N_↑/N_↓, spin-site injectivity, per-spin number commutators + hopping commute, and [S^z_tot, H]=0 (Tasaki §9.3.3) |
Hubbard/SpinSymmetry.lean |
SU(2) part of the §9.3.3 spin symmetry: Ŝ^±_tot definitions + [Ŝ^±_tot, H]=0 (imports SpinSymmetryAux; downstream API unchanged) |
Hubbard/SpinChargeCommutation.lean |
(model-agnostic) [Ŝ^-_tot, N̂]=0 + the number-preserving lowering tower fermionTotalNumber_mulVec_spinMinusPow_eigenvalue (deduplicated; used by both Nagaoka §11.2 and the flat-band capstone §11.3.1) |
Hubbard/AllUpState.lean |
all-up state: H_kin eigenvalue, no double occupancy |
Hubbard/AllDownState.lean |
all-down state: H_int · |↓..⟩ = 0 (mirror) |
Hubbard/AllDownStateTotalNumber.lean |
N_↓ · |↓..⟩ = (N+1)·|↓..⟩, S^z·|↓..⟩ = -(N+1)/2·|↓..⟩ |
Hubbard/SpinTotHermitian.lean |
(Ŝ^-)ᴴ = Ŝ^+, (Ŝ^z)/(Ŝ²) Hermitian |
Hubbard/SaturatedFerromagnetism.lean |
spin Casimir, Def 11.1, SU(2) algebra |
Hubbard/HardcoreSubspace.lean |
hard-core subspace + H_int vanishing (Tasaki §11.2) |
Hubbard/HardcoreProjection.lean |
hard-core projection ∏ᵢ (1 - n_↑n_↓) (Tasaki §11.2) |
Hubbard/HardcoreBasis.lean |
one-hole hard-core basis states \|Φ_{x,σ}⟩ (Tasaki §11.2) |
Hubbard/HardcoreSpan.lean |
one-hole hard-core sector spanned by the basis states (Tasaki §11.2 fn. 8) |
Hubbard/EffectiveHamiltonian.lean |
effective Hamiltonian Ĥ_eff = P̂_hc H P̂_hc + U→∞ reduction (Tasaki §11.2) |
Hubbard/TasakiBasis.lean |
Tasaki ordered-creation basis \|Φ_{x,σ}⟩ = ε • basisVec + orthonormality (Tasaki §11.2 eq. (11.2.3)) |
Hubbard/TasakiHopAction.lean |
uniform-sign hole-filling action ĉ†_{x,s}ĉ_{z,s}\|Φ_{x,σ}⟩ = -\|Φ_{z,σ_{z→x}}⟩ + sign ε = (-1)^x (Tasaki §11.2 eq. (11.2.4)) |
Hubbard/HopSignBetween.lean |
Forward-hop JW sign as a strictly-between parity (Issue #4230 PR3c-3): jwSign_mul_jwSign_update_forward — for a forward hop q→p (q.val<p.val, source c q=1), jwSign q c · jwSign p (update c q 0) = (-1)^(#occupied modes strictly between q,p); the 2·E_q of the modes below the source cancels in parity. jwSign_mul_jwSign_update_backward — the backward analogue (p.val<q.val, target c p=0) = (-1)^(#strictly between p,q). Model-agnostic; underlies the sign-free d=1 t-J hopping. Axiom-free |
Hubbard/EffectiveHamiltonianMatrix.lean |
off-diagonal matrix element ⟨Φ_{y,τ}\|Ĥ_eff\|Φ_{x,σ}⟩ = -t_{x,y}·[τ=σ_{y→x}] (Tasaki §11.2 eq. (11.2.5)) |
Hubbard/WeakNagaoka.lean |
Cauchy–Schwarz energy bound ⟨Φ_↑\|Ĥ_eff\|Φ_↑⟩ ≤ ⟨Φ\|Ĥ_eff\|Φ⟩ (Tasaki §11.2 eq. (11.2.9)) |
Hubbard/EffectiveHamiltonianSpinSymmetry.lean |
SU(2) symmetry of the effective Hamiltonian [Ĥ_eff, Ŝ^±_tot] = 0 (Tasaki §11.2, degeneracy backbone) |
Hubbard/WeakNagaokaTheorem.lean |
weak Nagaoka spin multiplet weakNagaoka_spinMultiplet: a ferromagnetic GS generates N+1 degenerate ground states with S_tot=S_max via the SU(2) ladder (Tasaki §11.2.1, Theorem 11.5) |
Hubbard/WeakNagaokaGroundState.lean |
Tasaki Theorem 11.5 weakNagaoka_theorem_11_5: existence of the ferromagnetic ground multiplet via the all-up block M_↑ = Tasaki matrix of Ĥ_eff; operator lift Ĥ_eff Φ_p = Σ_q ⟨Φ_q\|Ĥ_eff\|Φ_p⟩ Φ_q, sector completeness, N+1 = 2S_max+1 linearly independent degenerate eigenvectors with S_tot=S_max (Tasaki §11.2.1) |
Hubbard/WeakNagaokaGlobalMin.lean |
Tasaki Theorem 11.5 global form weakNagaoka_theorem_11_5_global: min(M_↑) = min(M) via the Schwarz bound (11.2.9) ferromagnetization (real Tasaki matrix + real min eigenvector), so the multiplet sits at the global one-hole ground energy — genuine ground states (Tasaki §11.2.1) |
Hubbard/NagaokaMagnetizationSector.lean |
Tasaki §11.2.2 foundations: the S_z^{(3)} magnetization grading (configMag/holeSpinMag), block-diagonality of M, sector matrices (HoleMagSector, tasakiEffReMatrixOnSector, nagaokaPFMatrixOnSector), Definition 11.6 (nagaokaConnectivity), and the per-sector Perron–Frobenius non-degenerate ground state |
Hubbard/NagaokaPerronFrobenius.lean |
Tasaki §11.2.2 upper bound: sector min = −μ (Collatz–Wielandt), min M ≤ min M_m, per-sector finrank ≤ 1 at the global min, and tasakiEffMatrix_ground_finrank_le_N_add_one (≤ N+1) |
Hubbard/NagaokaConnectivity.lean |
Tasaki Theorem 11.7 nagaoka_theorem_11_7 / nagaoka_theorem_11_7_degeneracy: the capstone — coefficient↔full bridge + SU(2) spin-multiplet lower bound (≥ N+1); with the connectivity condition and t≥0, the one-hole ground eigenspace is (N+1)-dimensional and every ground state has S_tot=S_max — Nagaoka’s theorem. Sorry-free, axiom-clean (Tasaki §11.2.2) |
Hubbard/TasakiFlatBandModel.lean |
Tasaki §11.3.1 flat-band model setup (d=1 decorated/Delta chain): external/internal site embeddings deltaExternalSite/deltaInternalSite into the physical chain Fin (2K+2), single-particle states flatBandAlpha/flatBandBeta (11.3.1/11.3.2), fermion operators flatBandA{Annihilation,Creation}/flatBandB{…} (11.3.3/11.3.4) + adjoints, the Hamiltonian flatBandHamiltonian = t Σ b̂†b̂ + U Σ n↑n↓ (11.3.5/11.3.6) + Hermiticity. First file of §11.3.1 (Issue #4158) |
Hubbard/TasakiFlatBandBasis.lean |
Tasaki §11.3.1 Lemma 11.10: {α_p} ∪ {β_u} is a basis of the single-particle Hilbert space Fin (2K+2) → ℂ (flatBand_linearIndependent, flatBandBasis). Diagonal evaluations, even/odd site-split equiv, cross-orthogonality ⟨α_p,β_u⟩=0, combined linear independence, and the basis (sorry-free) (Issue #4158) |
Hubbard/TasakiFlatBandCAR.lean |
Tasaki §11.3.1 eq. (11.3.7) flatBandBAnnihilation_ACreation_anticomm: {b̂_{u,σ}, â†_{p,τ}} = 0 (the b̂/↠operators anticommute, since ⟨α_p,β_u⟩=0), via the spinful CAR {ĉ_{x,σ},ĉ†_{y,τ}}=[x=y∧σ=τ] and bilinear expansion. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandGroundState.lean |
Tasaki §11.3.1 eqs. (11.3.8)/(11.3.9): the all-up α Slater state flatBandAlphaAllUpState = (∏_p â†_{p,↑})|vac⟩, the move-through lemma anticomm_listProd_mulVec_vacuum, b̂_{u,σ}|Φα⟩=0 (zero-energy condition), and Ĥ_hop|Φα⟩=0 (flatBandHopping_mulVec_alphaAllUpState) — |Φα,all↑⟩ is a zero-energy state of the hopping Hamiltonian. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandZeroEnergy.lean |
Tasaki §11.3.1 (toward Thm 11.11): Ĥ_int|Φα⟩=0 and Ĥ|Φα⟩=0 (flatBandHamiltonian_mulVec_alphaAllUpState) — the all-up α state is a zero-energy state of the full flat-band Hamiltonian (down annihilation ĉ_{x↓}|Φα⟩=0 ⇒ no double occupancy). Sorry-free (Issue #4158) |
Hubbard/SpinLoweringTowerGeneral.lean |
Tasaki §11.2.1/§11.3.1 (toward Thm 11.11, existence): the SU(2) spin-lowering tower at an arbitrary highest weight m = L/2 (the N/2-specialised tower of WeakNagaokaTheorem.lean covers only the chain maximum). General Ŝ^z/Ŝ^+Ŝ^-/highest-weight Casimir formulas + finite-tower nonvanishing/linear independence + the packaged highestWeight_spinMultiplet_general (a highest-weight v generates an (L+1)-dim maximal-spin multiplet). Needed because Tasaki’s flat-band ferromagnet has Ŝ^z=(K+1)/2 < N/2. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandHighestWeight.lean |
Tasaki §11.3.1 (toward Thm 11.11, existence): the all-up α state |Φα,all↑⟩ is the SU(2) highest-weight state of the ferromagnetic multiplet — Ŝ^+_tot|Φα⟩=0 (flatBandTotalSpinPlus_mulVec_alphaAllUpState), N̂_↑|Φα⟩=(K+1)|Φα⟩ (flatBandTotalUpNumber_mulVec_alphaAllUpState, via a charge move-through charge_listProd_mulVec_vacuum + the [N̂_↑,â†_{p,↑}]=â†_{p,↑} commutator), N̂_↓|Φα⟩=0, hence Ŝ^z_tot|Φα⟩=((K+1)/2)|Φα⟩ (flatBandTotalSpinZ_mulVec_alphaAllUpState, eq. (11.3.10)) — the half-filled-band highest weight m=(K+1)/2=|E|/2, strictly below the chain max N/2. These are exactly the hypotheses of highestWeight_spinMultiplet_general. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandNonvanishing.lean |
Tasaki §11.3.1 (toward Thm 11.11, existence): |Φα,all↑⟩ ≠ 0 (flatBandAlphaAllUpState_ne_zero), the last input to the existence half. No Slater/Gram machinery — the α orbitals are unit vectors on the external sites (α_p(2q)=δ_{pq}), so the external up annihilation ĉ_{2q,↑} is the canonical dual {ĉ_{2q,↑},â†_{p,↑}}=δ_{pq} (flatBandExtUpAnnihilation_ACreation_anticomm); the ordered dual annihilations collapse the creation product back to |vac⟩ (flatBandAlpha_listProd_exists_collapse via the peel lemma dualAnnihilation_peel_listProd_mulVec_vacuum), and |vac⟩≠0 (fermionMultiVacuum_ne_zero). Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandMultiplet.lean |
Tasaki §11.3.1 Theorem 11.11 (existence half, spin content): flatBand_ferromagnetic_multiplet — the K+2 = 2S_max+1 lowered states (Ŝ^-_tot)^k|Φα,all↑⟩ (k=0..K+1) are linearly independent and all carry total spin S_tot=S_max=(K+1)/2=N_e/2 (eigenstates of (Ŝ_tot)² at S_max(S_max+1)). Packages the general tower (#4164), highest-weight data (#4165), and nonvanishing (#4166) via highestWeight_spinMultiplet_general at L=K+1. (That every member is a zero-energy ground state needs the energy tower + PSD, in subsequent steps.) Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandEnergyTower.lean |
Tasaki §11.3.1 (toward Thm 11.11, existence): flat-band SU(2) lowering symmetry [Ŝ^±_tot, Ĥ]=0 (fermionTotalSpinPlus/Minus_commute_flatBandHamiltonian) and the energy tower Ĥ(Ŝ^-_tot)^k|Φα,all↑⟩=0 (flatBandHamiltonian_mulVec_spinMinusPow_alphaAllUpState) — every member of the ferromagnetic multiplet is a zero-energy state. The kinetic term is SU(2)-invariant: the b̂ operators form a spin doublet (built from the same spatial β_u), so the spin-summed mode number Σ_σ b̂†_{u,σ}b̂_{u,σ} commutes with Ŝ^+ (off-diagonal b̂†_↑b̂_↓ terms cancel, commute_two_component_kinetic_of_spinPlus_relations); the interaction reuses fermionTotalSpinPlus_commute_hubbardDoubleOccupancy; Ŝ^- follows by adjoint. (That 0 is the ground energy needs Ĥ≥0, the remaining step.) Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandPosSemidef.lean |
Tasaki §11.3.1 Theorem 11.11 (existence half, ground states): Ĥ≥0 (flatBandHamiltonian_posSemidef, for t,U≥0) — a nonnegative combination of PSD terms (b̂†b̂=(b̂)ᴴb̂; n̂↑n̂↓ a Hermitian-idempotent projection P=PᴴP); hence the energy rayleighOnVec Ĥ ψ≥0 everywhere while the tower states attain 0, so flatBand_alphaTower_isGroundState: each (Ŝ^-_tot)^k|Φα⟩ minimizes the energy (is a ground state). With flatBand_ferromagnetic_multiplet (LI + S_tot=S_max=(K+1)/2), this is the (2S_max+1)-dim maximal-spin degenerate ground-state multiplet — the existence half of Theorem 11.11. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandFrustrationFree.lean |
Tasaki §11.3.1 (toward Thm 11.11, uniqueness): frustration-free conditions on any flat-band ground state v (energy rayleighOnVec Ĥ v=0, t,U>0) — b̂_{u,σ}v=0 (flatBand_groundState_BAnnihilation_mulVec_eq_zero, eq. (11.3.11)) and n̂_{x↑}n̂_{x↓}v=0 (flatBand_groundState_doubleOccupancy_mulVec_eq_zero, no-double-occupancy form of (11.3.12)). Via generic helpers: Ĥ=ΣPSD energy decomposition (flatBandHamiltonian_rayleighOnVec_decompose) + each PSD term’s energy is ≥0 ⇒ each vanishes (posSemidef_mulVec_eq_zero_of_rayleighOnVec_zero, Matrix.PosSemidef.dotProduct_mulVec_zero_iff), and (b̂)ᴴb̂ v=0⇒b̂v=0 (conjTranspose_mul_self_mulVec_eq_zero). Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandNumberConservation.lean |
Tasaki §11.3.1 (toward Thm 11.11, uniqueness structure): particle-number conservation [Ĥ, N̂]=0 (flatBandHamiltonian_commute_fermionTotalNumber) — each kinetic mode b̂†_{u,σ}b̂_{u,σ} is number-conserving (b̂ lowers, b̂† raises N̂ by one: flatBandBAnnihilation/BCreation_commutator_fermionTotalNumber) and the interaction n̂↑n̂↓ is too; so ground states split into fixed-N sectors (Tasaki works in N_e=K+1). Plus flatBand_groundState_mem_hardcoreSubspace: any ground state lies in the Hubbard hard-core subspace (no double occupancy). Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandSubspaces.lean |
Tasaki §11.3.1 (toward Thm 11.11, uniqueness framework): the two subspaces of the uniqueness argument — flatBandAlphaFockSubmodule (span of all α-band Slater states flatBandAlphaSlaterState, with flatBandAlphaAllUpState_mem_alphaFockSubmodule: |Φα,all↑⟩ lives in it) and flatBandBKernelSubmodule = ⨅_{u,σ} ker b̂_{u,σ} (with mem_flatBandBKernelSubmodule_iff and flatBand_groundState_mem_BKernelSubmodule: every ground state lies in it, from frustration-free (11.3.11)). Tasaki’s uniqueness = the inclusion BKernel ⊆ αFock (no β-occupation) + symmetric/maximal-spin classification. Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandAlphaFockKernel.lean |
Tasaki §11.3.1 (toward Thm 11.11, uniqueness): the easy inclusion flatBandAlphaFockSubmodule ≤ flatBandBKernelSubmodule (flatBandAlphaFockSubmodule_le_BKernelSubmodule) — every α-Slater state is annihilated by every b̂_{u,σ} (flatBandBAnnihilation_mulVec_alphaSlaterState), since b̂ anticommutes with all ↠(11.3.7) and kills the vacuum (move-through by direct induction on the ordered product). The hard reverse inclusion BKernel ⊆ αFock (no β-occupation ⇒ flat-band) needs the Fock-space factorisation of the non-orthogonal {α}∪{β} basis, now proved (flatBandBKernelSubmodule_le_alphaFockSubmodule, TasakiFlatBandUniqueness.lean). Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandTheorem11_11.lean |
Tasaki §11.3.1 Theorem 11.11 support (particle number + submodule definitions): flatBandTotalNumber_commutator_ACreation ([N̂,â†_{p,↑}]=â†_{p,↑}), flatBandTotalNumber_mulVec_alphaAllUpState (N̂\|Φα,all↑⟩=(K+1)\|Φα,all↑⟩), flatBandFerromagneticMultipletSubmodule (span of the K+2=2S_max+1 lowered states (Ŝ^-_tot)^k\|Φα,all↑⟩), and flatBandHalfFilledGroundSubmodule (the zero-energy ker Ĥ states in the N_e=K+1 sector). The capstone theorems identifying these two submodules are proved, axiom-free, in TasakiFlatBandClassification.lean (below). Sorry-free (Issue #4158) |
Hubbard/TasakiFlatBandClassification.lean |
Tasaki §11.3.1 Theorem 11.11 (uniqueness ≤ half + capstone, dimension route, PROVED AXIOM-FREE — Issue #4346): flatBandFerromagneticMultipletSubmodule_finrank = K+2; [Ŝ^z_tot,Ĥ_flat]=0 (fermionTotalSpinZ_commute_flatBandHamiltonian, via su(2) Ŝ⁺Ŝ⁻−Ŝ⁻Ŝ⁺=2Ŝ^z); Ŝ^z preserves the ground subspace; the Ŝ^z-weight decomposition flatBandHalfFilledGroundSubmodule = ⨆_μ G ⊓ eigenspace(Ŝ^z,μ) collapsing to the K+2 half-integer weights a−(K+1)/2 (flatBandHalfFilledGroundSubmodule_eq_iSup_weight, off-weight blocks ⊥); flatBandFerromagneticMultipletSubmodule_le_groundSubmodule (existence side); and the capstone reduction flatBand_groundSubmodule_eq_multipletSpan_of_blocks — IF each Ŝ^z-weight block of the ground subspace is ≤ 1-dimensional THEN the ground subspace equals the multiplet (via Math/EigenspaceWeightFinrank.finrank_le_of_weight_blocks + Submodule.eq_of_le_of_finrank_le), combined with the discharged block bound flatBand_block_finrank_le_one (TasakiFlatBandSwapCoeff.lean) this file hosts the capstone theorems flatBand_theorem_11_11_groundSubmodule_eq_multipletSpan / flatBand_theorem_11_11_groundState_maximalSpin (no sorryAx, no axioms beyond propext/Classical.choice/Quot.sound). Sorry-free |
Hubbard/MielkeHamiltonian.lean |
Tasaki §11.3.2 (Mielke’s flat-band ferromagnetism, model): mielkeHamiltonian on a graph G (eqs. (11.3.31)/(11.3.6) — uniform hopping t + 2t·N̂ shift + on-site U, = hubbardHamiltonianOnGraph + 2t·N̂); Hermiticity, particle-number conservation [Ĥ,N̂]=0, and SU(2) invariance [Ŝ^±_tot,Ĥ]=0. Line-graph structure + Theorems 11.12/11.13 in a companion file (Issue #4177) |
Hubbard/MielkeTheorems.lean |
Tasaki §11.3.2 Theorem 11.13 (AXIOMATIZED) + Theorem 11.12 statement data: mielkeFlatBandDim D(Λ̃,B̃) (=\|B̃\|-\|Λ̃\|+1 bipartite else \|B̃\|-\|Λ̃\|), mielkeSingleElectronOp (the 11.3.32 single-electron operator on the line graph); the line graph is mathlib SimpleGraph.lineGraph (realized via SimpleGraph.Iso G (lineGraph Gbase)). IsMaximalSpinMultipletSubmodule N sub D (shared predicate: sub is the (D+1)-fold maximal-spin multiplet ground subspace — finrank = D+1 + all (Ŝ_tot)² eigenvectors at S_max(S_max+1), S_max=D/2; reused by generalFlatBandFerromagnetic and §11.5). axiom mielke_theorem_11_13 (Mielke ferromagnetism: biconnected base, N=D ⇒ IsMaximalSpinMultipletSubmodule) — Tasaki states it without proof (Theorem 11.8 policy). Theorem 11.12 is no longer an axiom: it is proved in MielkeIncidenceMatrix.lean (§11.3.3, Issue #4180), which imports this file. The Mielke Hamiltonian model + symmetries are axiom-free (Issue #4177) |
Hubbard/MielkeIncidenceMatrix.lean |
Tasaki §11.3.3 (incidence-matrix SᴴS factorisation): mielkeSingleElectronOpOn (single-electron operator over an arbitrary finite vertex type; mielkeSingleElectronOp is now the Fin (M+1) wrapper), mielkeIncidence (S = √t· mathlib incMatrix, restricted to genuine edges), and mielkeIncidence_conjTranspose_mul_self: SᴴS = mielkeSingleElectronOpOn (lineGraph G) t for t ≥ 0 (eqs. (11.3.36)–(11.3.39)). Presents the line-graph operator as a PSD Gram matrix whose kernel is ker S. Carries the §11.3.3 proof through: mielke_lineGraph_ker_finrank_eq (rank step dim ker T = \|B\|−rank S), mielke_conjTranspose_ker_finrank (signless-Laplacian zero-mode count dim ker(SSᴴ)=Colorable 2 ? 1 : 0 for a connected base, via ker Sᴴ/bipartite sign vector), mielke_lineGraph_ker_finrank_eq_dim (assembled D=\|B\|−(\|Λ̃\|−bip)), and mielke_theorem_11_12 — now a proved theorem (formerly an axiom): transports the flat-band dimension to the Fin (M+1) realisation along the line-graph SimpleGraph.Iso via Matrix.rank_submatrix (needs \|Λ̃\| ≤ \|B\|, i.e. the base has a cycle). Discharges Issue #4180 |
Hubbard/GeneralFlatBand.lean |
Tasaki §11.3.4 Theorem 11.15 (general flat-band ferromagnetism, PROVED axiom-free): for a Hermitian PSD hopping matrix T (Matrix.PosSemidef) with flat band h₀=ker T, D₀=dim h₀>0, U>0, at filling N=D₀. generalFlatBandProjectionMatrix P₀ = orthogonal projection onto ker T (Matrix.toEuclideanLin → Submodule.starProjection → LinearMap.toMatrixOrthonormal); generalFlatBandActiveSites Λ₀={x\|(P₀)_{x,x}≠0}; generalFlatBandProjectionIrreducible = Matrix.IsIrreducible of the real support matrix Complex.normSq (P₀) on Λ₀ (Tasaki block-decomposability; P₀ Hermitian ⇒ symmetric support); generalFlatBandFerromagnetic = ground subspace finrank = D₀+1 + all (Ŝ_tot)² eigenvectors at S_max=D₀/2 (mirrors mielke_theorem_11_13). theorem tasaki_theorem_11_15 (now PROVED axiom-free in GeneralFlatBandTheorem1115.lean, Issue #4453): ferromagnetic ⇔ P₀\|Λ₀ irreducible — discharged by composing Theorem 11.17 (ferro⇔connected) with the bridge projectionIrreducible⇔basis-connected (via the generalFlatBandProjectionBlockReducible cut). Plus Lemma 11.16 (IsGeneralFlatBandSpecialBasis + now-discharged (axiom-free) theorem generalFlatBand_lemma_11_16: ker T has a site-localised basis {μ_z}_{z∈I}, \|I\|=D₀, μ_z(z)≠0, μ_z(z')=0 for z'≠z — built from the reflexive predual of a D₀-subset of separating coordinate functionals) and Theorem 11.17 (generalFlatBandBasisGraph/generalFlatBandBasisConnected; theorem generalFlatBand_theorem_11_17 now PROVED axiom-free in GeneralFlatBandDisconnected.lean (⇒ direction + capstone) / GeneralFlatBandMultiplet.lean (⇐ direction), Issue #4363: ferromagnetic ⇔ the special basis is connected — Mielke’s second nec-&-suf condition). Theorem 11.15 + Lemma 11.16 + Theorem 11.17 all discharged axiom-free (Issues #4186/#4363/#4453) |
Hubbard/SectorMinEnergy.lean |
Tasaki §11.4 (sector minimum energy + ferromagnetism criterion, eq. (11.4.26)): spinSector twoS (unit EuclideanSpace vectors with (Ŝ_tot)² Φ = (twoS/2)(twoS/2+1) Φ, twoS=2S), sectorMinEnergy H twoS = E_min(S) = ⨅ of rayleighOnVec H over that sector (L² unit norm via EuclideanSpace, matching the project min-eigenvalue convention), and exhibitsFerromagnetism H twoSmax = ∀ twoS<twoSmax, E_min(Smax) < E_min(twoS). Foundation (definitions only) for the non-singular Hubbard Theorems 11.18–11.20 (Issue #4189) |
Hubbard/NonsingularHubbardModel.lean |
Tasaki §11.4 non-singular Hubbard model (eq. (11.4.23)) + symmetries: nonsingularHubbardHamiltonian K ν t ζ tPert U = flatBandHamiltonian K ν t U + (ζ:ℂ) • hubbardKinetic (2K+1) tPert (the flat-band model t Σ b̂†b̂ + U Σ n̂↑n̂↓ perturbed by ζ Σ t_xy ĉ†ĉ; ζ=0 recovers the flat band). Proven symmetries (by .add of the flat-band + kinetic lemmas): Hermiticity (tPert Hermitian), [Ĥ,N̂]=0, and SU(2) invariance [Ŝ^±_tot,Ĥ]=0 (spin-minus via the adjoint of spin-plus + Hermiticity). Model setup for Theorems 11.18–11.20 (Issue #4189), axiom-free |
Hubbard/NonsingularLocalStability.lean |
Tasaki §11.4 Theorem 11.18 (local stability, AXIOMATIZED): IsNonsingularHopping K tPert t R (the (11.4.24) cyclic translation-invariance + (11.4.25) range-R summability of the perturbation), and axiom nonsingular_theorem_11_18: ∃ ν₀,η₀,ξ₀>0 (uniform in system size, dep. on d=1,R) s.t. under the parameter bounds 0<ν≤ν₀, |ζ|≤ν³η₀, U≥ξ₀t|ζ|/ν² the maximal-spin sector lies below the once-flipped sector, sectorMinEnergy H (K+1) < sectorMinEnergy H (K−1) (S_max=(K+1)/2) — stability against a single spin flip (eq. (11.4.29)). Deep perturbation-theory result, deferred (Issue #4189; Theorem 11.8/11.13 policy) |
Hubbard/TasakiNonsingularFerro.lean |
Tasaki §11.4.3 Theorem 11.20 (ferromagnetism in the non-singular Hubbard model) — the §11.4 culmination (first proof of Hubbard ferromagnetism with no singularity). tasakiNonsingularHamiltonian K ν t s U = flatBandHamiltonian K ν t U − s•Σ_{p,σ} â†_{p,σ}â_{p,σ} (eq. (11.4.38); tasakiNonsingularHamiltonian_zero_s: s=0 ⇒ = flatBandHamiltonian). Theorem 11.20 is PROVED as tasaki_theorem_11_20 in NonsingularFerromagnetism.lean (resting on the analytic Lemma 11.22, a documented axiom, and the axiom-free Theorem 11.11 classification in TasakiFlatBandClassification.lean) |
Hubbard/NonsingularLocalHamiltonian.lean |
Tasaki §11.4.3 frustration-free local Hamiltonian ĥ_p + Lemmas 11.22/11.23 (AXIOMATIZED) — the analytic proof-internal results of Theorem 11.20. flatBandANumber/flatBandBNumber; nonsingularLocalHamiltonian K ν s t U lam κ i = ĥ_p (eq. (11.4.48), d=1: (1+2ν²)s·1 − s·â†â_i + ((t−lam)/2)Σ_{u∈{i−1,i}}b̂†b̂_u + (1−κ)(U−lam)·n↑n↓_{2i} + ((U−lam)/2)Σ_{u∈{i−1,i}}n↑n↓_{2u+1} + (κ/2)(U−lam)Σ_{q∈{i−1,i+1}}n↑n↓_{2q}); nonsingular_lemma_11_22 (∃ thresholds, t/s,U/s large ⇒ ∀p ĥ_p≥0, lam,κ ∝ s), nonsingular_lemma_11_23 (t,U↑∞ limit: sector-min of ĥ_p strictly positive below S_max). Documented axioms (genuine eigenvalue-continuity perturbation theory; Issue #4189) |
Hubbard/NonsingularFerromagnetism.lean |
Tasaki §11.4.3 Lemma 11.21 + Theorem 11.20 (PROVED, d=1, 1≤K) — discharges the former axiom nonsingular_lemma_11_21 and axiom tasaki_theorem_11_20. nonsingular_exhibitsFerromagnetism (Lemma 11.21: ∀p ĥ_p≥0 ⇒ exhibitsFerromagnetism H (K+1) (K+1)) via the frustration-free decomposition (Ĥ+C≥0, all-up state achieves −C, every lower sector strictly above −C by compact-eigenSphere attainment + Theorem 11.11); tasaki_theorem_11_20 assembles it through Lemma 11.22. Generic bricks: isCompact_eigenSphere, continuous_rayleighOnVec, lt_iInf_rayleigh_of_eigenSphere (Issue #4189) |
Hubbard/NonsingularFrustrationFree.lean |
Tasaki §11.4.3: the frustration-free decomposition eq. (11.4.46) (Issue #4189, towards Lemma 11.21): cyclic-reindex helpers sum_shift_sub_one/sum_shift_add_one (∑ f(p∓1)=∑ f p on Fin (K+1)), sum_nonsingularLocalHamiltonian (the ∑_i ĥ_p collapses to the canonical single-species sums via the β/double-occupancy multiplicities — κ cancels by incidence), and tasakiNonsingular_eq_sum_localHamiltonian: tasakiNonsingularHamiltonian = (∑_i ĥ_p i) − (K+1)(1+2ν²)s·1 + lam·(∑_u N̂^β_u + ∑_x n̂↑n̂↓_x) (for all lam, κ). The foundational operator identity behind Lemma 11.21. Axiom-free |
Hubbard/NonsingularFrustrationFreePos.lean |
Tasaki §11.4.3: frustration-free positivity Ĥ + const ≥ 0 (Issue #4189, towards Lemma 11.21): nonsingularRemainder_eq_flatBand (Σ N̂^β + Σ n↑n↓ = flatBandHamiltonian K ν 1 1) + tasakiNonsingular_add_const_posSemidef — if every ĥ_p ≥ 0 and lam ≥ 0 then (tasakiNonsingularHamiltonian + (K+1)(1+2ν²)s·1).PosSemidef (sum of the PSD ĥ_p and the PSD lam-remainder, by eq. (11.4.46)). So the ground energy is ≥ −(K+1)(1+2ν²)s. Axiom-free |
Hubbard/FermionSiteSpin.lean |
Per-site fermionic spin operators (towards §11.5 t-J model): fermionSiteSpinPlus/Minus N i (Ŝ^±_x = ĉ†_{x↑}ĉ_{x↓} / ĉ†_{x↓}ĉ_{x↑}), fermionSiteSpinZ N i ((n̂_{x↑}−n̂_{x↓})/2), and fermionSpinDot N i j (Ŝ_x·Ŝ_y = ½(Ŝ^+_xŜ^-_y+Ŝ^-_xŜ^+_y)+Ŝ^z_xŜ^z_y) — the building blocks for the t-J Heisenberg coupling (eq. (11.5.4)). fermionTotalSpinPlus/Minus_eq_sum_siteSpin* (the totals are the per-site sums). Axiom-free (Issue #4198) |
Hubbard/TJModel.lean |
Tasaki §11.5.2 the ferromagnetic t-J model (eq. (11.5.4)): fermionSiteNumber N i (n̂_x = n̂_{x↑}+n̂_{x↓}); tJHamiltonian N G τ J = −τ P̂hc (Σ_{⟨x,y⟩,σ}ĉ†_{x,σ}ĉ_{y,σ}) P̂hc + J Σ_{⟨x,y⟩}(n̂_x n̂_y/4 − Ŝ_x·Ŝ_y) (hopping = hubbardKineticOnGraph sandwiched by hubbardHardcoreProjection, exchange via fermionSpinDot; ordered-pair bond sums, τ,J>0). Ground-subspace statement uses the generic groundSubmoduleAtFilling (GroundSubspaceAtFilling.lean, below). Proposition 11.24 is now PROVED (proposition_11_24 in TJProposition1124.lean, Issue #4230); model axiom-free (Issue #4198) |
Hubbard/TJProposition1124.lean |
Tasaki §11.5.2 Proposition 11.24 (ferromagnetism in the d=1 ferromagnetic t-J model) — PROVED (Issue #4230, E6 capstone): proposition_11_24 — on cycleGraph (N+1) at odd filling Ne<N+1, IsMaximalSpinMultipletSubmodule N (groundSubmoduleAtFilling (tJHamiltonian …) Ne) Ne (ground states S_tot=Ne/2 and Ne+1-fold degeneracy). Assembles finrank G = Ne+1 (le_antisymm of the SU(2)-tower lower bound #4305 and the Ŝ³-weight upper bound #4312) with the maximal-spin (Ŝ_tot)²-eigenvalue: the Ne+1 LI tower states (Ŝ⁻)^k Ω span G (card = finrank) and each is an (Ŝ_tot)² eigenvector at (Ne/2)(Ne/2+1) (highestWeight_spinMultiplet_general), so every v∈G is. Discharges the former axiom; now fully axiom-free (A.17 exists_joint_su2_energy_eigenstate discharged §A.3.2) |
Hubbard/TJSpinSymmetry.lean |
Tasaki §11.5: total-Ŝ³ conservation of the t-J model (Issue #4230 PR1a, towards discharging Prop 11.24): fermionTotalSpinZ_commute_tJHamiltonian ([Ĥ_tJ, Ŝ³_tot]=0, axiom-free) — the U(1) part of SU(2) invariance for the magnetization-sector decomposition. Site weight relations [Ŝ³_tot, Ŝ^±_x]=±Ŝ^±_x (totalSpinZ_mul_siteSpinPlus/Minus) from the CAR number/creation commutators + totalSpinZ_commute_fermionSpinDot (SU(2) scalar, weight 0) + _fermionSiteNumber + _tJKinetic (hard-core sandwich) |
Hubbard/TJSpinSymmetryRaising.lean |
Tasaki §11.5: total-Ŝ⁺ invariance of the t-J model (Issue #4230 PR1b): fermionTotalSpinPlus_commute_tJHamiltonian ([Ĥ_tJ, Ŝ⁺_tot]=0, axiom-free). Site su(2) relations [Ŝ⁺_tot, Ŝ³_x]=−Ŝ⁺_x (totalSpinPlus_mul_siteSpinZ), [Ŝ⁺_tot, Ŝ⁻_x]=2Ŝ³_x (totalSpinPlus_mul_siteSpinMinus), [Ŝ⁺_tot, Ŝ⁺_x]=0 — from the single-operator commutators fermionUpAnnihilation_commutator_fermionTotalSpinPlus etc. + totalSpinPlus_commute_fermionSpinDot (SU(2) scalar via A/B/C cancellation) + _fermionSiteNumber + _tJKinetic. With TJSpinSymmetry (Ŝ³) gives the U(1)×raising part of SU(2); the lowering follows by Hermitian adjoint (next) |
Hubbard/TJHermitian.lean |
Tasaki §11.5: Hermiticity + total-Ŝ⁻ invariance of the t-J model (Issue #4230 PR1c, completes the SU(2) invariance): tJHamiltonian_isHermitian (Ĥ_tJ self-adjoint — interaction self-adjoint as a sum via (f x y)ᴴ=f y x + Finset.sum_comm; also the input for A.18’s real symmetric sector matrix) + fermionTotalSpinMinus_commute_tJHamiltonian ([Ĥ_tJ, Ŝ⁻_tot]=0, by adjoint of the raising commute). Site-spin adjoints (Ŝ⁺_x)ᴴ=Ŝ⁻_x, (Ŝ_x·Ŝ_y)ᴴ=Ŝ_y·Ŝ_x. All axiom-free. With PR1a/PR1b this gives full SU(2) invariance → A.17 spin-½ sector |
Hubbard/TJSectorReduction.lean |
Tasaki §11.5: spin-½ sector reduction (A.17 applied to Ĥ_tJ) (Issue #4230 PR2a): tJHamiltonian_eigenstate_spin_zero_or_half — every eigenvalue of Ĥ_tJ has an eigenstate with Ŝ³_tot=0 or =½ (exactly the A.17 step Tasaki cites to open the Prop 11.24 proof). Cartesian total spin tJTotalSpinOne=½(Ŝ⁺+Ŝ⁻), tJTotalSpinTwo=−(i/2)(Ŝ⁺−Ŝ⁻) + Hermitian + commute (PR1) + su(2) (tJTotalSpin_su2_12/23/31 from the ladder commutators) + [Ŝ³,Ŝ⁺]=Ŝ⁺ (adjoint). Axiom-free (A.17’s matrix simul-diagonalization step now discharged §A.3.2) |
Hubbard/TJSectorBasis.lean |
Tasaki §11.5: Ŝ³=½ sector basis skeleton (Issue #4230 PR2b): site-state s : Fin(N+1)→Fin 3 (0/1/2 = empty/↑/↓) → tJConfigOf spinful occupation; tJConfigOf_apply_up/down (orbital values), tJConfigOf_mem_hardcore (always hard-core), tJConfigOf_injective (config recovers the site state) ⇒ tJConfigOf_basisVec_inner (orthonormal). Foundation for the real-symmetric sector matrix; Ŝ³=½ constraint + hop matrix elements (wrap sign (-1)^(Ne-1)) follow |
Hubbard/TJSectorSpin.lean |
Tasaki §11.5: spin eigenvalues of the t-J sector basis (Issue #4230 PR3a): basisVec (tJConfigOf s) is a simultaneous N̂_↑/N̂_↓/Ŝ³_tot eigenvector — fermionTotalUpNumber/DownNumber_mulVec_tJConfigOf (eigenvalues #{s=↑}/#{s=↓} via tJConfigOf_up/down_count), fermionTotalSpinZ_mulVec_tJConfigOf (½(#↑−#↓)), and fermionTotalSpinZ_mulVec_tJConfigOf_half (Ŝ³=½ when #↑=#↓+1). Upgrades the skeleton toward a basis of the physical Ŝ³=½ sector; axiom-free |
Hubbard/TJSectorNumber.lean |
Tasaki §11.5: electron-number eigenvalue of the t-J sector basis (Issue #4230 PR3b): fermionTotalNumber_mulVec_tJConfigOf (N̂ eigenvalue #{s=↑}+#{s=↓} = #occupied sites, via sum_spinful_reindex + Fin.sum_univ_two + the up/down counts) and fermionTotalNumber_mulVec_tJConfigOf_eq (N̂ = Ne when #↑+#↓ = Ne). With PR3a’s Ŝ³=½ this places the basis in the N̂=Ne, Ŝ³=½ sector; axiom-free |
Hubbard/TJSectorHop.lean |
Tasaki §11.5: the site-hop move + sector preservation (Issue #4230 PR3c-1): tJSiteHop s a b (move the electron a→b); tJSiteHop_eq_comp_swap (= s ∘ Equiv.swap a b when b empty), so an allowed hop is a transposition of sites and tJSiteHop_count preserves every state-count — tJSiteHop_up_count/_down_count keep the basis in the same N̂/Ŝ³ sector. Prepares the off-diagonal hop matrix elements; axiom-free |
Hubbard/TJSectorHopConfig.lean |
Tasaki §11.5: the hop config identity (Issue #4230 PR3c-2): tJConfigOf_tJSiteHop_up/_down — the spinful occupation of the hopped site-state tJSiteHop s a b equals tJConfigOf s updated by the single hop (a,σ)↦0, (b,σ)↦1 (the config produced by ĉ†_{bσ}ĉ_{aσ} on basisVec (tJConfigOf s), up to the Jordan–Wigner sign). Axiom-free |
Hubbard/TJSectorHopAction.lean |
Tasaki §11.5: the forward-hop matrix element on the sector basis (Issue #4230 PR3c-4): tJ_uphop_forward_mulVec/tJ_downhop_forward_mulVec — for a forward allowed hop (a.val < b.val, source a of spin σ, target b empty), ĉ†_{bσ}ĉ_{aσ}\|Φ_s⟩ = (-1)^(occupied modes strictly between (a,σ),(b,σ)) · \|Φ_{tJSiteHop s a b}⟩, composing the single-hop action + config identity + sign parity. Axiom-free |
Hubbard/TJSectorHopNN.lean |
Tasaki §11.5: the NN hop is sign-free on the sector basis (Issue #4230 PR3c-5): tJ_uphop_nn_mulVec/tJ_downhop_nn_mulVec — for a forward nearest-neighbour hop (b.val = a.val + 1, non-wrap), the single intervening orbital is forced empty by the hop conditions, so the strictly-between exponent is 0 and ĉ†_{bσ}ĉ_{aσ}\|Φ_s⟩ = \|Φ_{tJSiteHop s a b}⟩ (no sign). Axiom-free |
Hubbard/TJSectorHopBackward.lean |
Tasaki §11.5: the leftward NN hop (Issue #4230 PR-B7-3b): tJ_uphop/downhop_backward_nn_mulVec (ĉ†_{aσ}ĉ_{bσ}\|Φ_s⟩ = \|Φ_{tJSiteHop s b a}⟩, electron b→a, sign-free +1 via jwSign_mul_jwSign_update_backward) + _matrixElement (= [s'=tJSiteHop s b a]). The leftward kinetic terms of the cyclic hopping. Axiom-free |
Hubbard/TJSectorHopBackwardWrap.lean |
Tasaki §11.5: the leftward wrap hop (Issue #4230 PR-B7-3c): tJ_uphop/downhop_backward_wrap_mulVec + _matrixElement — the leftward wrap hop ĉ†_{0σ}ĉ_{Nσ}\|Φ_s⟩ = \|Φ_{tJSiteHop s b a}⟩ (electron N→0), sign-free +1 for odd Ne (between = Ne−1 via the backward sign + boundary sums). Axiom-free |
Hubbard/TJOccupationCount.lean |
Tasaki §11.5: total occupation count + three-way mode split (Issue #4230 PR3c-6): tJConfigOf_total_count (∑_k (tJConfigOf s k).val = #↑+#↓, the electron number) and sum_split_le_between_ge (model-agnostic: ∑_all = ∑_{k≤q} + ∑_{q<k<p} + ∑_{k≥p}). Infrastructure for the wrap-bond hop sign (-1)^(Ne−1). Axiom-free |
Hubbard/TJSectorHopWrap.lean |
Tasaki §11.5: the wrap bond is sign-free for odd Ne (Issue #4230 PR3c-7): tJ_uphop_wrap_mulVec/tJ_downhop_wrap_mulVec — for the cycle’s wrap bond (a.val=0, b.val=N), source a of spin σ, target b empty, odd Ne=#↑+#↓, the strictly-between occupation is Ne−1 (even, via the three-way split + total count + boundary sums), so ĉ†_{bσ}ĉ_{aσ}\|Φ_s⟩ = \|Φ_{tJSiteHop s a b}⟩ (no sign). Axiom-free |
Hubbard/TJEffMatrix.lean |
Tasaki §11.5: the t-J effective matrix in the site-state basis (Issue #4230 PR-A): tJEmbedding (columns = \|Φ_s⟩, s : Fin(N+1)→Fin 3), tJEffMatrix = Tᴴ Ĥ_tJ T, tJEffMatrix_isHermitian (compression of the Hermitian Ĥ_tJ), tJEffMatrix_apply (M_{s',s} = ⟨Φ_{s'}\|Ĥ_tJ\|Φ_s⟩). The finite real-symmetric matrix fed to Perron–Frobenius (A.18). Axiom-free |
Hubbard/TJSectorExchange.lean |
Tasaki §11.5: the exchange spin-flip on the sector basis (Issue #4230 PR-B1/B2): tJSpinSwap s i j (swap the spins of sites i,j) + tJConfigOf_tJSpinSwap (config identity) + fermionSiteSpinPlus_mul_Minus_mulVec_tJConfigOf — for s i=↓, s j=↑ (i≠j), Ŝ⁺_iŜ⁻_j\|Φ_s⟩ = \|Φ_{tJSpinSwap s i j}⟩ with net JW sign +1 (the two same-site creation/annihilation pairs each contribute a squared string sign =1, via jwSign_succ_cancel_low/high). Axiom-free |
Hubbard/TJKineticSector.lean |
Tasaki §11.5: the kinetic sandwich reduction on the sector basis (Issue #4230 PR-B3): tJKinetic_sandwich_mulVec_tJConfigOf — since tJConfigOf s is hard-core, the inner projection fixes \|Φ_s⟩, so P̂hc·K·P̂hc\|Φ_s⟩ = P̂hc(K\|Φ_s⟩); tJKinetic_sandwich_mulVec_mem (the result is hard-core). Isolates the hopping matrix elements from the projection bookkeeping. Axiom-free |
Hubbard/TJKineticMatrixElement.lean |
Tasaki §11.5: the forward hop matrix elements (Issue #4230 PR-B4): tJ_uphop_nn_matrixElement/tJ_downhop_nn_matrixElement + wrap variants — ⟨Φ_{s'}\|ĉ†_{bσ}ĉ_{aσ}\|Φ_s⟩ = [s' = tJSiteHop s a b] for a forward allowed NN/wrap hop, combining the sign-free hop actions with the basis orthonormality (tJConfigOf_basisVec_inner). The off-diagonal −τ kinetic entry. Axiom-free |
Hubbard/TJExchangeMatrixElement.lean |
Tasaki §11.5: the exchange matrix element (Issue #4230 PR-B5): fermionSpinFlip_matrixElement — ⟨Φ_{s'}\|Ŝ⁺_iŜ⁻_j\|Φ_s⟩ = [s' = tJSpinSwap s i j] for an antiparallel pair (s i=↓, s j=↑, i≠j), combining the sign-free exchange action with the basis orthonormality. The off-diagonal −J/2 exchange entry. Axiom-free |
Hubbard/TJDiagonalMatrixElement.lean |
Tasaki §11.5: the diagonal terms have no off-diagonal matrix element (Issue #4230 PR-B6): fermionSiteNumber_mulVec_basisVec/fermionSiteSpinZ_mulVec_basisVec (diagonal actions) + diagonal_offdiag_matrixElement_eq_zero (a scalar-acting operator’s off-diagonal ME vanishes) + fermionSiteNumber_mul_offdiag_matrixElement_eq_zero/fermionSiteSpinZ_mul_offdiag_matrixElement_eq_zero — the n̂_xn̂_y and Ŝ³_xŜ³_y terms contribute 0 off-diagonal. Axiom-free |
Hubbard/TJOffDiagonal.lean |
Tasaki §11.5: the hard-core bra drops the projection (Issue #4230 PR-B7): tJ_hardcore_proj_apply ((P̂hc u)(tJConfigOf s') = u(tJConfigOf s') — the P̂hc row at a hard-core config is the unit vector, by Hermiticity) + tJKinetic_matrixElement_eq (the kinetic sandwich matrix element = ⟨Φ_{s'}\|K\|Φ_s⟩, both projections dropped) + tJKinetic_matrixElement_expand (⟨Φ_{s'}\|K\|Φ_s⟩ = Σ_σΣ_iΣ_j couplingOf G · ⟨Φ_{s'}\|ĉ†_{iσ}ĉ_{jσ}\|Φ_s⟩). Returns the kinetic ME to plain inner-product normal form. Axiom-free |
Hubbard/TJKineticNonneg.lean |
Tasaki §11.5: the general single-hop matrix element (Issue #4230 PR-B7-3d): tJ_hop_matrixElement_apply — for arbitrary i,j,σ, ⟨Φ_{s'}\|ĉ†_{iσ}ĉ_{jσ}\|Φ_s⟩ = (when source (j,σ) occupied + target (i,σ) empty) the two string signs times [s'=hopped], else 0; tJ_hop_matrixElement_eq_zero_of_source/_of_target/_of_target_other — the element vanishes when the source is empty, the target is already filled with the same spin, or the target site carries the opposite spin (the hopped config would be doubly-occupied, hence non-hard-core ≠ any bra). Foundation for the kinetic off-diagonal non-negativity. Axiom-free |
Hubbard/TJKineticSummand.lean |
Tasaki §11.5: the cyclic kinetic matrix element is a non-negative real (Issue #4230 PR-B7-3f): tJ_kinetic_summand_zero_or_one — each summand couplingOf(cycleGraph) i j · ⟨Φ_{s'}\|ĉ†_{iσ}ĉ_{jσ}\|Φ_s⟩ is 0 or 1 (non-adjacent killed by the coupling; adjacent dispatched to the rightward/leftward NN + wrap hop matrix elements via cycleGraph_adj_val_cases, or to the source/target vanishing) — and tJKinetic_matrixElement_nonneg (0 ≤ ⟨Φ_{s'}\|K\|Φ_s⟩.re ∧ .im = 0). The kinetic off-diagonal entry −τ·(≥0) ≤ 0, the Perron–Frobenius input. Axiom-free |
Hubbard/TJExchangeNonneg.lean |
Tasaki §11.5: the exchange spin-flip matrix element is 0 or 1 (Issue #4230 PR-B7-3g): fermionSpinFlip_matrixElement_eq_zero_of_source (s j ≠ ↑ ⟹ Ŝ⁻_j\|Φ_s⟩ = 0 ⟹ ⟨Φ_{s'}\|Ŝ⁺_iŜ⁻_j\|Φ_s⟩ = 0), fermionSpinFlip_matrixElement_eq_zero_of_target (i ≠ j, s j = ↑, s i ≠ ↓ ⟹ the raising Ŝ⁺_i hits an empty down-orbital ⟹ = 0), tJ_exchange_summand_zero_or_one (each summand couplingOf(cycleGraph) i j · ⟨Φ_{s'}\|Ŝ⁺_iŜ⁻_j\|Φ_s⟩ ∈ {0,1}: non-adjacent killed by the coupling; adjacent antiparallel s i=↓,s j=↑ gives the sign-free indicator [s'=tJSpinSwap], else vanishes). The exchange off-diagonal entry −(J/2)·(≥0) ≤ 0, the Perron–Frobenius input. Axiom-free |
Hubbard/TJExchangeBondSum.lean |
Tasaki §11.5: the t-J effective-matrix off-diagonal is non-positive (Issue #4230 PR-B7-3h): fermionSiteSpinMinus_mul_Plus_comm (different-site ladders commute Ŝ⁻_xŜ⁺_y = Ŝ⁺_yŜ⁻_x for x≠y, via four cross-site anticommutations), tJ_exchange_swap_summand_zero_or_one (couplingOf·⟨Ŝ⁻_xŜ⁺_y⟩ ∈ {0,1} by commutation + the (y,x) summand), tJInteraction_matrixElement_eq (the interaction off-diagonal = −½·Σ_{x,y}(couplingOf·⟨Ŝ⁺_xŜ⁻_y⟩ + couplingOf·⟨Ŝ⁻_xŜ⁺_y⟩); density/Ŝ³ products drop), tJInteraction_matrixElement_nonpos (J ≥ 0 ⟹ exchange off-diagonal re ≤ 0, im = 0), and tJEffMatrix_offdiag_nonpos (combining the kinetic −τ·(≥0) and exchange −(J/2)·(≥0): for τ,J ≥ 0, odd Ne, s' ≠ s, the entry M_{s',s} is a non-positive real — the Perron–Frobenius hypothesis). Axiom-free |
Hubbard/TJSectorMatrix.lean |
Tasaki §11.5: the real-symmetric t-J sector effective matrix (Issue #4230 PR-B8): TJSpinHalfFillingSector N Ne (sector states s with #↑ = #↓ + 1 and #↑ + #↓ = Ne, i.e. Ŝ³ = ½, N̂ = Ne), tJEffReMatrix (real part of the Hermitian tJEffMatrix), tJEffReMatrixOnSector (its submatrix Subtype.val restriction to the sector), and tJEffReMatrixOnSector_isSymm (symmetry from tJEffMatrix_isHermitian: M_{q,p} = conj M_{p,q} ⟹ equal real parts — no global realness needed). The Matrix … ℝ that feeds Theorem A.18 once −M is irreducible. Axiom-free |
Hubbard/TJStepRelation.lean |
Tasaki §11.5: the elementary connectivity step on t-J sector states (Issue #4230 PR-C1): tJSpinSwap_eq_comp_swap (tJSpinSwap s i j = s ∘ Equiv.swap i j), tJSpinSwap_count (the swap preserves the count of sites in any spin state), TJStep N s s' (one off-diagonal move: a NN/wrap hop s' = tJSiteHop s a b of an electron into an adjacent empty site, or an adjacent antiparallel exchange s' = tJSpinSwap s i j), and tJStep_up_count/tJStep_down_count/tJStep_preserves_sector (a step preserves #↑ and #↓, hence stays in the N̂=Ne, Ŝ³=½ sector). The step relation whose positive matrix entries feed matrix_pow_succ_pos_of_path for the Perron–Frobenius irreducibility. Axiom-free |
Hubbard/TJStepMatrixEntry.lean |
Tasaki §11.5: a connectivity step gives a strictly negative matrix entry (Issue #4230 PR-C1b): tJ_cycle_hop_kinetic_summand_eq_one (the moved-electron kinetic summand couplingOf b a · ⟨ĉ†_{bσ}ĉ_{aσ}⟩ = 1, via the forward/backward/wrap dispatch of cycleGraph_adj_val_cases), tJKinetic_matrixElement_re_ge_one_of_hop (a hop ⟹ ⟨Φ_{s'}\|K\|Φ_s⟩.re ≥ 1, by Finset.single_le_sum over the {0,1}-valued summands), tJInteraction_bondSum_re_ge_one_of_exchange (an exchange ⟹ the ladder bond-sum .re ≥ 1), tJInteraction_matrixElement_re_le_neg_half_of_exchange (⟹ J·interaction.re ≤ −J/2), and tJEffMatrix_re_neg_of_step (for τ,J > 0, each TJStep s s' gives M_{s',s}.re < 0 — a hop via kinetic ≤ −τ, an exchange via interaction ≤ −J/2; the strict B_{s',s} = −M_{s',s} > 0 feeding Perron–Frobenius). Axiom-free |
Hubbard/TJAdjacentSwap.lean |
Tasaki §11.5: adjacent-value swaps are connectivity steps (Issue #4230 PR-C2 bridge): AdjacentSwapStep N s s' (s' exchanges the values at an adjacent pair a,b of distinct values, = s ∘ Equiv.swap a b), adjacentSwapStep_to_TJStep (every such swap is a TJStep — a hop if one site is empty, an exchange if the two are opposite spins), AdjacentSwapReachable (ReflTransGen AdjacentSwapStep), and tjReachable_of_adjacentSwapReachable (lifts to ReflTransGen (TJStep N) via ReflTransGen.mono). The bridge from the combinatorial adjacent-swap reachability (next PR) to the physical step relation. Axiom-free |
Hubbard/TJSwapReachableBasics.lean |
Tasaki §11.5: adjacent-swap reachability basics (Issue #4230 PR-C2 combinatorics a): comp_swap_count (precomposition with a transposition preserves value-counts, a site bijection), adjacentSwapStep_count / adjacentSwapReachable_count (a step / the whole closure preserves every value-count), adjacentSwapReachable_swap (the value-swapped s ∘ Equiv.swap a b is reachable — single step if the values differ, refl if equal), and exists_needed_value_right_of_same_counts (equal value-counts + prefix [0,p) agreement + disagreement at p ⟹ the value s' p occurs in s strictly right of p). The reusable building blocks for the selection-sort same-counts ⟹ AdjacentSwapReachable. Axiom-free |
Hubbard/TJSwapReachable.lean |
Tasaki §11.5: same value-counts ⟹ adjacent-swap reachable (Issue #4230 PR-C2 combinatorics b): adj_of_val_succ (consecutive sites are cycle-adjacent), bubble_reachable (move the value at q = p + g leftward to p by g NN swaps, leaving the prefix [0,p) fixed; induction on g), reach_of_agree_aux (selection sort: induction on the number of unfixed positions — bubble the needed value into the leftmost disagreement, recurse), and adjacentSwapReachable_of_same_counts (any two Fin 3-configs with equal value-counts are connected by adjacent value-swaps). With the previous bridge, gives full TJStep-reachability within a sector. Axiom-free |
Hubbard/TJSectorShifted.lean |
Tasaki §11.5: the shifted sector matrix B = c·1 − M (Issue #4230 PR-C3a): tJSectorShifted (the Perron–Frobenius input B = c·1 − tJEffReMatrixOnSector), with tJSectorShifted_isSymm (from M’s symmetry), tJSectorShifted_nonneg (0 ≤ B entrywise: diagonal c − M_{qq} ≥ 0, off-diagonal −M_{q,p} ≥ 0 from tJEffMatrix_offdiag_nonpos), tJStep_ne (a TJStep changes the config), and tJSectorShifted_pos_of_step (a TJStep between distinct sector states gives a strictly positive off-diagonal B-entry, from tJEffMatrix_re_neg_of_step + symmetry). Axiom-free |
Hubbard/TJSectorIrreducible.lean |
Tasaki §11.5: the shifted t-J sector matrix is irreducible (Issue #4230 PR-C3b): tJ_value_count_total (#∅+#↑+#↓ = N+1), tJSector_same_counts (any two sector states have equal value-counts, via the sector equations + total), tJSectorShifted_pow_pos_of_reachable (a TJStep-reachable chain from a sector state lifts to a strictly positive matrix-power entry of B, by matrix_pow_succ_pos_of_pow_pos_step along the chain — the membership carried via tJStep_preserves_sector), and tJSectorShifted_isIrreducible (for τ,J > 0, odd Ne, shift c above the diagonal, B = c·1 − M is irreducible: diagonal positivity + connectivity via adjacentSwapReachable_of_same_counts). The Perron–Frobenius hypothesis, ready for Theorem A.18. Axiom-free |
Hubbard/TJSectorGroundState.lean |
Tasaki §11.5: the unique positive sector ground state via Perron–Frobenius (Issue #4230 PR-D): a Nonempty (TJSpinHalfFillingSector N Ne) witness instance (the Ŝ³=½ filling with ↑’s left of ↓’s, counts via card_filter_val_lt + the total) and tJEffReMatrixOnSector_perronFrobenius — applying Theorem A.18 (perronFrobenius_real_symmetric) to M = tJEffReMatrixOnSector (its shift c·1−M irreducible, PR-C3): M has a strictly positive eigenvector at its lowest eigenvalue μ (the sector ground energy), the eigenspace finrank ≤ 1 (non-degeneracy). The Perron–Frobenius ground state of the spin-charge-separated t-J sector. Axiom-free (modulo A.18, which is axiom-free) |
Hubbard/TJExpansion.lean |
Tasaki §11.5: the sector expansion and its left inverse (Issue #4230 PR-E1): tJExpansion v = Σ_s v_s • \|Φ_s⟩ (the full-space vector from a sector coefficient vector), tJExpansionCoeff u s = ⟨Φ_s, u⟩, and tJExpansionCoeff_tJExpansion (left inverse — the orthonormal sector basis gives tJExpansionCoeff (tJExpansion v) = v, so the expansion is injective). The bridge between sector coefficient vectors and full Hilbert-space vectors (mirrors Nagaoka tasakiCoeff/tasakiCoeff_expansion); the operator lift Ĥ_tJ (tJExpansion v) = μ • tJExpansion v is the next PR. Axiom-free |
Hubbard/TJCompleteness.lean |
Tasaki §11.5: completeness of the sector basis (Issue #4230 PR-E1b-A): tJ_completeness (a vector supported on the sector configurations equals its own sector expansion tJExpansion (tJExpansionCoeff v) — direct orthogonality on the plain basisVec(tJConfigOf s)), tJSiteStateOf (the inverse map config→site-state), and tJConfigOf_tJSiteStateOf_of_hardcore (tJConfigOf ∘ tJSiteStateOf = id on hard-core configs — surjectivity recognising a hard-core config as a sector basis index). The completeness counterpart of the left inverse, feeding the operator-lift closure. Axiom-free |
Hubbard/TJNumberCommute.lean |
Tasaki §11.5: [Ĥ_tJ, N̂] = 0 (Issue #4230 PR-E1b): the t-J Hamiltonian conserves total electron number (fermionTotalNumber_commute_tJHamiltonian), the charge half of the conservation laws. Each piece commutes with N̂: the kinetic sandwich (fermionTotalNumber_commute_tJKinetic, projection + hopping conserve number), n̂_x n̂_y (_commute_fermionSiteNumber, diagonal), and Ŝ_x·Ŝ_y (_commute_fermionSpinDot — its ladders Ŝ⁺_x = ĉ†_↑ĉ_↓ are number-conserving hops via fermionTotalNumber_commute_hopping, its Ŝ³-product diagonal). Needed for the operator-lift sector closure (Ĥ_tJ\|Φ_s⟩ stays in the N̂=Ne sector). Axiom-free |
Hubbard/TJHardcorePreserve.lean |
Tasaki §11.5: Ĥ_tJ preserves the hard-core subspace (Issue #4230 PR-E1b): tJHamiltonian_mulVec_mem_hardcore — a no-double-occupancy vector stays no-double-occupancy under Ĥ_tJ, via tJHamiltonian_commute_hubbardHardcoreProjection ([Ĥ_tJ, P̂hc]=0) and P̂hc(Ĥ_tJ v)=Ĥ_tJ(P̂hc v)=Ĥ_tJ v. Each piece commutes with P̂hc: the kinetic sandwich P̂hc K P̂hc by idempotency P̂hc²=P̂hc (tJKinetic_commute_hubbardHardcoreProjection), and the per-site Ŝ^±_x, Ŝ³_x, n̂_x commute with every double occupancy n̂_{i↑}n̂_{i↓} (fermionSiteSpin{Plus,Minus,Z}_commute_hubbardDoubleOccupancy, fermionSiteNumber_commute_hubbardDoubleOccupancy) — hence with every hard-core factor and with P̂hc — so the density product n̂_x n̂_y and the spin dot Ŝ_x·Ŝ_y (fermionSpinDot_commute_hubbardHardcoreProjection) commute with P̂hc. The operator-side input to the sector-matrix lift (mirrors fermionTotalSpinMinus_mulVec_mem_hardcore). Axiom-free |
Hubbard/TJOperatorLift.lean |
Tasaki §11.5: the t-J operator lift on a sector basis state (Issue #4230 PR-E1c): tJHamiltonian_mulVec_tJConfigOf — Ĥ_tJ\|Φ_s⟩ = Σ_{s'} ⟨Φ_{s'}\|Ĥ_tJ\|Φ_s⟩ \|Φ_{s'}⟩ reassembles its sector-matrix column (mirrors hubbardEffectiveHamiltonian_mulVec_tasakiState). Uses sector-basis completeness: Ĥ_tJ\|Φ_s⟩ is sector-supported because it stays hard-core (tJHamiltonian_mulVec_mem_hardcore) and keeps the N̂=Ne/Ŝ³=½ eigenvalues (tJHamiltonian_mulVec_preserves_number/_spinZ, from [Ĥ_tJ,N̂]=[Ĥ_tJ,Ŝ³]=0). Key new input: the support restriction tJ_mulVec_apply_eq_zero_of_not_sector (a hard-core N̂=Ne, Ŝ³=½ eigenstate vanishes off the sector configs — a hard-core config with electron count Ne and Ŝ³ count ½ is a sector index, via the diagonal actions fermionTotalUpNumber/DownNumber/SpinZ_mulVec_apply + mulVec_apply_eq_zero_of_spinZ_ne). Axiom-free |
Hubbard/TJEigenvectorLift.lean |
Tasaki §11.5: the t-J eigenvector lift from the sector PF eigenvector (Issue #4230 PR-E1d): tJHamiltonian_mulVec_tJExpansion_ofReal — a real Perron–Frobenius ground eigenvector c of tJEffReMatrixOnSector (eigenvalue μ) lifts to an Ĥ_tJ-eigenvector tJExpansion c at the same μ: Ĥ_tJ(tJExpansion c)=μ•tJExpansion c (mirrors hubbardEffectiveHamiltonian_mulVec_tasakiExpansion). Via tJHamiltonian_mulVec_tJExpansion (Ĥ_tJ acts on a sector expansion as the effective matrix M=tJEffMatrix, from the per-basis-state lift tJHamiltonian_mulVec_tJConfigOf' + the bridge tJExpansionCoeff(Ĥ_tJ\|Φ_s⟩)=tJEffMatrix) and the sector realness tJEffMatrix_sector_im_zero (off-diagonals by tJEffMatrix_offdiag_nonpos, diagonal by Hermiticity), upgrading the real eigen-equation to the complex one. Axiom-free |
Hubbard/TJGroundEnergy.lean |
Tasaki §11.5: variational bound on the t-J ground energy (Issue #4230 PR-E2, ≤ direction): tJHamiltonian_groundEnergyAtFilling_le_of_sectorEigen — a nonzero real sector eigenvector c of tJEffReMatrixOnSector at μ gives groundEnergyAtFilling Ĥ_tJ Ne ≤ μ, since the lifted state tJExpansion c is admissible (hard-core N̂=Ne eigenvector, tJExpansion_mem_hardcore/fermionTotalNumber_mulVec_tJExpansion/tJExpansion_ne_zero_of_ne_zero) with energy μ (#4279 lift). Built on the reusable generic groundEnergyAtFilling_le_of_eigenvector (GroundSubspaceAtFilling.lean: any nonzero N̂=Ne hard-core eigenvector at real μ bounds the ground energy, via ciInf_le_of_le + the BddBelow brick groundEnergyAtFilling_bddBelow + dotProduct_star_ofLp_self_eq_one). Axiom-free. The reverse μ ≤ groundEnergyAtFilling (A.17 + odd Ne) follows next |
Hubbard/TJGroundEnergyReverse.lean |
Tasaki §11.5: spin-½ W-eigenvalues are sector eigenvalues (Issue #4230 PR-E2, ≥ crux): tJ_spinHalf_W_eigenvector_to_sector — a nonzero Ŝ³=½, N̂=Ne, hard-core (W) eigenvector of Ĥ_tJ at real E yields a nonzero real eigenvector of tJEffReMatrixOnSector at E (it is sector-supported via the support restriction, so equals its sector expansion; the operator action becomes the complex sector matrix, real on the sector by tJEffMatrix_sector_im_zero; a complex eigenvector of a real-matrix cast at real E has a nonzero real/imag part, matrix_eigenvec_re/im_of_complex). Corollary tJ_sectorMin_le_of_spinHalf_W_eigenvalue: under the PF minimality of μ, every such E satisfies μ ≤ E. The crux for the reverse ground-energy bound; remaining for E2-≥ is a W-restricted A.17 (the global-min W-eigenvector lands in Ŝ³=½ by A.17 + odd Ne). Axiom-free |
Hubbard/TJFillingBasis.lean |
Tasaki §11.5: the full N̂=Ne filling basis + completeness (Issue #4230 PR-E2 ≥, W-compression foundation): the all-Ŝ³ analog of the Ŝ³=½ sector basis — TJFillingSector N Ne = {s : Fin(N+1)→Fin 3 // #↑+#↓=Ne} indexing the hard-core fixed-filling space W; tJFillingExpansion/tJFillingExpansionCoeff + left inverse tJFillingExpansionCoeff_tJFillingExpansion (orthonormal); support restriction tJ_mulVec_apply_eq_zero_of_not_filling (a hard-core N̂=Ne vector vanishes off the filling configs — double-occ + wrong-count killed, no Ŝ³ constraint) and completeness tJ_filling_completeness. The orthonormal W-basis in which Ĥ_tJ compresses to the filling effective matrix (toward groundEnergyAtFilling = hermitianMinEigenvalue Ĥ_W). Axiom-free |
Hubbard/TJFillingCompress.lean |
Tasaki §11.5: the W-projection + compression homomorphism (Issue #4230 PR-E2 ≥, toward the W-restricted A.17): tJFillingEmbedding (columns \|Φ_s⟩ over the filling index), tJFillingWSubmodule (= (N̂=Ne)-eigenspace ⊓ hardcore), PreservesTJFillingW B (B maps W→W, reusable). The projection identity tJFillingProjection_mulVec_eq_of_mem (T Tᴴ fixes W, via Matrix.mulVec_mulVec + tJ_filling_completeness) drives the compression homomorphism tJFillingCompress_mul_of_right_preserves (compress(A)compress(B)=compress(AB) when B preserves W, since the intermediate T Tᴴ is invisible — tJFillingProjection_mul_of_preserves). preservesTJFillingW_tJHamiltonian (Ĥ_tJ preserves W, from [Ĥ_tJ,N̂]=0 + hard-core preservation). The homomorphism will transfer the spin operators’ su(2)/Hermitian/commute relations to their W-compressions, enabling the matrix A.17 at the filling index. Axiom-free |
Hubbard/TJFillingSpinCompress.lean |
Tasaki §11.5: the A.17 operators preserve the filling space W (Issue #4230 PR-E2 ≥): preservesTJFillingW_of_commute (an operator commuting with N̂ and P̂hc preserves W) + the submodule closure preservesTJFillingW_smul/_add/_sub, giving PreservesTJFillingW for Ŝ⁽³⁾ (fermionTotalSpinZ), Ŝ⁺, Ŝ⁻, and the Cartesian Ŝ⁽¹⁾=½(Ŝ⁺+Ŝ⁻)/Ŝ⁽²⁾=−(i/2)(Ŝ⁺−Ŝ⁻) (tJTotalSpinOne/Two); plus fermionTotalSpinPlus_commute_fermionTotalNumber (Ŝ⁺ is number-conserving). With preservesTJFillingW_tJHamiltonian these are the inputs to the compression homomorphism for the W-restricted A.17. Axiom-free |
Hubbard/TJFillingCompressSpinAlgebra.lean |
Tasaki §11.5: the compressed Ĥ_W, Ŝ⁽ᵅ⁾_W satisfy the A.17 hypotheses (Issue #4230 PR-E2 ≥): via the compression homomorphism + compress linearity (tJFillingCompress_smul/_sub/_isHermitian), the W-compressions inherit Hermiticity, the su(2) relations tJFillingCompress_su2_12/_23/_31 ([Ŝ⁽¹⁾_W,Ŝ⁽²⁾_W]=iŜ³_W etc.), and Ĥ_W-commutativity tJFillingCompress_tJHamiltonian_commute_one/_two/_three. These are exactly the inputs of the matrix Theorem A.17 (exists_joint_su2_energy_eigenstate), to be applied at the filling index next. Axiom-free |
Hubbard/TJFillingRayleighBridge.lean |
Tasaki §11.5: the filling embedding is an isometry + the Rayleigh bridge (Issue #4230 PR-E2 ≥): tJFillingEmbedding_conjTranspose_mul_self (Tᴴ T = 1, orthonormal columns via tJConfigOf_basisVec_inner), the isometry tJFillingExpansion_dotProduct_self (⟨T c, T c⟩ = ⟨c, c⟩), and the Rayleigh bridge rayleighOnVec_tJFillingCompress (rayleighOnVec Ĥ_tJ (tJFillingExpansion c) = rayleighOnVec (tJFillingCompress Ĥ_tJ) c — operator Rayleigh on a lifted state = matrix Rayleigh of the compression, via the rectangular adjoint identity). These connect the operator-side groundEnergyAtFilling to the finite matrix Ĥ_W, whose minimum eigenvalue is identified with μ via the W-restricted A.17. Axiom-free |
Hubbard/TJFillingEigenLift.lean |
Tasaki §11.5: lifting compressed eigenvectors back to W-eigenvectors (Issue #4230 PR-E2 ≥): mulVec_tJFillingExpansion_of_compress_eigen — if A preserves W and Φ is an eigenvector of compress(A) at E, then tJFillingExpansion Φ is an eigenvector of A at E (via the projection identity T Tᴴ = id on W); plus tJFillingExpansion_mem_tJFillingWSubmodule. This turns the filling-index eigenstate produced by the matrix A.17 into a genuine Ĥ_tJ/Ŝ³-eigenstate inside W, the final input to groundEnergyAtFilling = μ. Axiom-free |
Hubbard/TJFillingSpinZDiag.lean |
Tasaki §11.5: Ŝ³ diagonal on filling expansions + no Ŝ³=0 state for odd Ne (Issue #4230 PR-E2 ≥): fermionTotalSpinZ_mulVec_tJFillingExpansion (Ŝ³ scales the coefficient at s by ½(#↑−#↓)) and tJFillingExpansion_eq_zero_of_spinZ_mulVec_eq_zero (for odd Ne every filling state has #↑≠#↓, so the only Ŝ³=0 filling state is 0); plus tJFillingExpansionCoeff_zero. This kills the Ŝ³=0 branch of the W-restricted A.17 for odd Ne, forcing the Ŝ³=½ sector. Axiom-free |
Hubbard/TJGroundEnergyGe.lean |
Tasaki §11.5: E2 capstone — groundEnergyAtFilling = μ (Issue #4230 PR-E2 ≥, COMPLETE): tJ_perronFrobeniusMin_le_hermitianMinEigenvalue (W-restricted A.17: applies the matrix ham_eigenstate_spin_zero_or_half to Ĥ_W’s min eigenvector with the proven compressed Hermitian/su(2)/commute hypotheses, lifts it to W, odd-Ne forces Ŝ³=½, so μ ≤ hermitianMinEigenvalue Ĥ_W); tJ_groundEnergyAtFilling_ge_of_sectorMin (μ ≤ groundEnergyAtFilling via le_ciInf + variational lower bound + Rayleigh bridge + isometry); and tJHamiltonian_groundEnergyAtFilling_eq_perronFrobeniusMin — the d=1 ferromagnetic t-J ground energy at odd filling Ne equals the Perron–Frobenius sector minimum μ (≤ from #4280, ≥ from the A.17), packaged with the strictly-positive PF eigenvector v at μ. Axiom-free: Theorem A.17 (exists_joint_su2_energy_eigenstate) now discharged §A.3.2 |
Hubbard/TJGroundSpinHalfFinrank.lean |
Tasaki §11.5: the Ŝ³=½ ground block is at most 1-dimensional (Issue #4230 PR-E3a, the SU(2) upper-bound seed): tJExpansionCoeffₗ (the sector-coefficient map tJExpansionCoeff packaged as a ℂ-linear map); tJ_spinHalf_W_complexSectorEigen (a hard-core N̂=Ne, Ŝ³=½ eigenvector of Ĥ_tJ at real E has, as its coefficient vector, a complex eigenvector of the complexified sector matrix (tJEffReMatrixOnSector).map ofReal at E — re-derives the #4279 matrix action + sector-realness, injecting via tJExpansionCoeff_tJExpansion); and tJ_groundSubmodule_spinHalf_finrank_le_one — finrank ℂ (groundSubmoduleAtFilling Ĥ_tJ Ne ⊓ (Ŝ³=½)) ≤ 1. Proof: obtain the PF data once (so groundEnergyAtFilling = μ via #4280/#4290 le_antisymm, and finrank ℝ (real sector eigenspace at μ) ≤ 1); the real↔complex bridge matrix_complex_eigenspace_finrank_le_one_of_real gives finrank ℂ (complex sector eigenspace at μ) ≤ 1; the block embeds into that eigenspace by the injective ℂ-linear Φ ↦ tJExpansionCoeff Φ (injective since block elements are sector-supported, tJ_completeness), so LinearMap.finrank_le_finrank_of_injective finishes. Axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJSectorRaise.lean |
Tasaki §11.5: the single-site spin-raising operator is sign-free on the sector basis (Issue #4230 PR-E3b PR1, toward lifting the PF vector to a highest weight): tJConfigOf_update_raise (config identity — raising s x : ↓→↑ empties orbital 2x+1, fills 2x); fermionSiteSpinPlus_mulVec_tJConfigOf_of_down — for s x = ↓, Ŝ⁺_x |Φ_s⟩ = |Φ_{s with x↦↑}⟩ with net Jordan–Wigner sign +1 (the adjacent orbitals (x↑,x↓)=(2x,2x+1) and the empty 2x collapse the two strings via jwSign_succ_cancel_high); and fermionSiteSpinPlus_mulVec_tJConfigOf_of_not_down (s x ≠ ↓ ⟹ Ŝ⁺_x|Φ_s⟩ = 0, the down-orbital being empty). The Marshall sign-freeness underpinning the positivity of the iterated (Ŝ⁺)^m; fully axiom-free |
Hubbard/TJRaisingTower.lean |
Tasaki §11.5: eigenvalue tracking along the spin-raising tower (Issue #4230 PR-E3b PR2, toward the highest weight): fermionTotalSpinZ_mulVec_spinPlusPow (Ŝ³ (Ŝ⁺)^k v = (m+k)(Ŝ⁺)^k v — each Ŝ⁺ step raises the Ŝ³ eigenvalue by one, via [Ŝ³,Ŝ⁺]=Ŝ⁺; the raising mirror of the lowering tower), tJHamiltonian_mulVec_spinPlusPow (Ĥ_tJ (Ŝ⁺)^k v = μ (Ŝ⁺)^k v, energy preserved since [Ĥ_tJ,Ŝ⁺]=0), fermionTotalNumber_mulVec_spinPlusPow (N̂ (Ŝ⁺)^k v = Ne (Ŝ⁺)^k v, number preserved since [N̂,Ŝ⁺]=0). So (Ŝ⁺)^k Φ₀, when nonzero, is a fixed-Ne, energy-μ, Ŝ³=½+k eigenvector — the building blocks for raising the PF ground vector to a nonzero highest weight; fully axiom-free |
Hubbard/TJRaisingTermination.lean |
Tasaki §11.5: the spin-raising tower terminates (Issue #4230 PR-E3b PR3, gives Ŝ⁺Ω=0 at the top): fermionTotalDownNumber_mul_fermionTotalSpinPlus ([N̂_↓,Ŝ⁺]=−Ŝ⁺, summed from the per-site relation via fermionTotalSpinPlus_eq_sum_siteSpinPlus), fermionTotalDownNumber_mulVec_spinPlusPow (N̂_↓ (Ŝ⁺)^k v = (m−k)(Ŝ⁺)^k v — each raise removes one down-spin), and spinPlusPow_succ_eq_zero_of_downNumber — a vector with N̂_↓ v = m v is annihilated by m+1 raisings ((Ŝ⁺)^(m+1) v = 0), since the would-be N̂_↓-eigenvalue −1 forces (↓count+1)·ψ(w)=0 for every config w (via the diagonal fermionTotalDownNumber_mulVec_apply, ↓count ≥ 0). Applied to a Ŝ³=½, N̂=Ne ground state (N̂_↓=(Ne−1)/2), the top Ω=(Ŝ⁺)^((Ne−1)/2)Φ is a highest weight; fully axiom-free |
Hubbard/TJHighestWeight.lean |
Tasaki §11.5: the raised sector ground state is a highest weight (Issue #4230 PR-E3b PR4): tJ_raised_highestWeight — combining the tower tracking (PR2) and termination (PR3), a sector ground state Φ with Ŝ³Φ=½Φ, N̂_↓Φ=mΦ, Ĥ_tJΦ=μΦ produces at the top Ω=(Ŝ⁺)^m Φ a highest-weight ground state: Ŝ⁺Ω=0, Ŝ³Ω=(m+½)Ω, Ĥ_tJΩ=μΩ. For the d=1 ferromagnetic t-J ground state (m=(Ne−1)/2) this gives Ŝ³Ω=(Ne/2)Ω — the maximal-spin highest weight feeding highestWeight_spinMultiplet_general; the remaining input is Ω≠0 (Marshall positivity). Fully axiom-free |
Hubbard/TJExpansionSpinEigen.lean |
Tasaki §11.5: sector eigenvalues of the lifted ground vector (Issue #4230 PR-E3b PR5a, inputs to tJ_raised_highestWeight): tJSpinHalfFillingSector_down_count (every Ŝ³=½, N̂=Ne sector state has #↓=(Ne−1)/2, by omega from #↑=#↓+1 ∧ #↑+#↓=Ne); fermionTotalSpinZ_mulVec_tJExpansion (Ŝ³ (tJExpansion v) = ½ (tJExpansion v)); fermionTotalDownNumber_mulVec_tJExpansion (N̂_↓ (tJExpansion v) = ((Ne−1)/2)(tJExpansion v)). These let the highest-weight extraction apply to the lifted PF ground vector Φ₀=tJExpansion(ℂ∘v) with m=(Ne−1)/2; fully axiom-free |
Hubbard/TJTotalRaiseAction.lean |
Tasaki §11.5: the total raising operator on a sector basis state (Issue #4230 PR-E3b PR5b-1, toward the positivity non-vanishing): fermionTotalSpinPlus_mulVec_tJConfigOf — Ŝ⁺_tot |Φ_s⟩ = Σ_{x : s x = ↓} |Φ_{s with x↦↑}⟩, the sign-free expansion (every term coefficient +1, summing the single-site fermionSiteSpinPlus_mulVec_tJConfigOf_of_down/_of_not_down over sites). The keystone for the config-nonnegativity argument that the iterated raising preserves nonnegative coefficients (so (Ŝ⁺)^((Ne−1)/2)Φ₀ ≠ 0 from v > 0); fully axiom-free |
Hubbard/TJRaiseCoeffSum.lean |
Tasaki §11.5: coefficient sum of the raising action (Issue #4230 PR-E3b PR5b-2, the positivity tracking): coeffSum_basisVec (Σ_c basisVec w c = 1) and coeffSum_fermionTotalSpinPlus_tJConfigOf (Σ_c (Ŝ⁺_tot |Φ_s⟩) c = #↓(s) — each of the #↓(s) raised basis states contributes 1, sign-free). With the uniform sector down-count #↓=(Ne−1)/2, iterating gives coeffSum ((Ŝ⁺)^((Ne−1)/2) Φ₀) = ((Ne−1)/2)! · Σ v_q > 0 from v > 0, so the raised vector is nonzero; fully axiom-free |
Hubbard/TJFillingCoeffSum.lean |
Tasaki §11.5: coefficient sum of a filling expansion (Issue #4230 PR-E3b PR5b-3a, the recursion ingredients): coeffSum_tJFillingExpansion (coeffSum (tJFillingExpansion v) = Σ_s v_s) and coeffSum_fermionTotalSpinPlus_tJFillingExpansion (coeffSum (Ŝ⁺_tot (tJFillingExpansion v)) = Σ_s v_s·#↓(s)). Together they give the recursion coeffSum (Ŝ⁺ ψ) = d·coeffSum ψ for a hard-core N̂_↓-eigenvector ψ at d (both sides equal Σ_s v_s #↓(s)), the multiplicative step for the iterated-raising positivity; fully axiom-free |
Hubbard/TJRaisePositivityStep.lean |
Tasaki §11.5: the coefficient-sum recursion step (Issue #4230 PR-E3b PR5b-3b): fermionTotalDownNumber_mulVec_tJFillingExpansion (N̂_↓ diagonal on a filling expansion, scaling each basis state by its down-count) and coeffSum_fermionTotalSpinPlus_eq_of_downEigen — a hard-core N̂=Ne vector ψ with N̂_↓ ψ = d ψ satisfies coeffSum (Ŝ⁺_tot ψ) = d · coeffSum ψ (both Ŝ⁺ψ and N̂_↓ψ have coefficient sum Σ_s coeff_s·#↓(s) via tJ_filling_completeness, and coeffSum(N̂_↓ψ)=d·coeffSum ψ by the eigen-equation). The multiplicative step driving coeffSum((Ŝ⁺)^k Φ₀) to ((Ne−1)/2)!·Σv_q > 0; fully axiom-free |
Hubbard/TJRaiseHardcore.lean |
Tasaki §11.5: the raising operator preserves the hard-core subspace (Issue #4230 PR-E3b PR5c): fermionTotalSpinPlus_mulVec_mem_hardcore (Ŝ⁺_tot maps hubbardHardcoreSubspace into itself, mirror of the Ŝ⁻_tot version via fermionTotalSpinPlus_commute_hubbardHardcoreProjection) and fermionTotalSpinPlus_pow_mulVec_mem_hardcore (the tower (Ŝ⁺)^k v stays hard-core). This keeps every state of the raising tower (Ŝ⁺)^k Φ₀ hard-core — the prerequisite for applying the coefficient-sum recursion along the tower; fully axiom-free |
Hubbard/TJRaisePositivity.lean |
Tasaki §11.5: the raised vector is nonzero — the Marshall positivity crux (Issue #4230 PR-E3b PR5d): coeffSum_tJExpansion (coeffSum (tJExpansion v) = Σ_s v_s) and spinPlusPow_ne_zero_of_coeffSum_ne_zero — a hard-core N̂=Ne vector Φ₀ with N̂_↓Φ₀ = m Φ₀ and nonzero coefficient sum has (Ŝ⁺_tot)^m Φ₀ ≠ 0. Proof: each raising step multiplies the coefficient sum by the down-count eigenvalue m−k (coeffSum_fermionTotalSpinPlus_eq_of_downEigen + the merged hard-core/N̂/N̂_↓ tower lemmas), nonzero for k < m, so coeffSum stays nonzero up to k=m. Applied to Φ₀ = tJExpansion(ℂ∘v) (coeffSum = Σ v_q > 0, m=(Ne−1)/2) this is the Marshall non-vanishing Ω ≠ 0; fully axiom-free |
Hubbard/TJMaximalSpinGroundState.lean |
Tasaki §11.5: a maximal-spin highest-weight ground state (Issue #4230 PR-E4 PR6a, assembling the E3b chain): tJ_exists_maximalSpin_highestWeight_groundState — for odd Ne < N+1 and τ,J>0 there is a nonzero Ω with Ŝ⁺Ω=0, Ŝ³Ω=(Ne/2)Ω, Ĥ_tJΩ=μΩ at μ=groundEnergyAtFilling, plus Ω∈hubbardHardcoreSubspace and N̂Ω=Ne·Ω (so Ω∈groundSubmoduleAtFilling). Here Ω = (Ŝ⁺)^((Ne−1)/2)(tJExpansion(ℂ∘v)) for the strictly-positive PF eigenvector v: non-vanishing from spinPlusPow_ne_zero_of_coeffSum_ne_zero (coeffSum=Σv_q>0), highest-weight from tJ_raised_highestWeight, and groundEnergyAtFilling=μ from the E2 bounds. Feeds highestWeight_spinMultiplet_general for the Ne+1 multiplet. Axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJGroundDegeneracyLower.lean |
Tasaki §11.5: ground degeneracy lower bound (Issue #4230 PR-E4): tJ_groundSubmodule_finrank_ge — the d=1 ferromagnetic t-J ground subspace at odd filling Ne < N+1 has Ne + 1 ≤ finrank. The maximal-spin highest weight Ω (tJ_exists_maximalSpin_highestWeight_groundState) generates via highestWeight_spinMultiplet_general the Ne+1 linearly independent tower (Ŝ⁻)^k Ω; since Ŝ⁻ commutes with Ĥ_tJ and N̂ and preserves the hard-core subspace, every tower member is again a ground state in groundSubmoduleAtFilling, so LinearIndependent.of_comp + fintype_card_le_finrank give the bound. Axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJLadderInjective.lean |
Tasaki §11.5: SU(2) ladder injectivity on weight spaces (Issue #4230 PR-E5, toward the degeneracy upper bound): fermionTotalSpin_ladder_norm — the norm identity ‖Ŝ⁻v‖² = ‖Ŝ⁺v‖² + 2sz‖v‖² for a weight vector Ŝ³v=sz•v (from [Ŝ⁺,Ŝ⁻]=2Ŝ³ + (Ŝ⁻)ᴴ=Ŝ⁺, via star w ⬝ᵥ w = ↑(∑‖w i‖²)); and the consequences fermionTotalSpinMinus_mulVec_ne_zero_of_spinZ_pos (Ŝ⁻ injective for sz>0) + fermionTotalSpinPlus_mulVec_ne_zero_of_spinZ_neg (Ŝ⁺ injective for sz<0). No representation theory — these ladder injections embed each Ŝ³-weight space of the ground subspace into Ŝ³=±½, giving (via E3a) the upper bound finrank ≤ Ne+1; fully axiom-free |
Hubbard/TJGroundWeightFinrank.lean |
Tasaki §11.5: weight-space finrank non-increasing toward Ŝ³=½ (Issue #4230 PR-E5b): fermionTotalSpinMinus_mulVec_mem_groundSubmodule (Ŝ⁻ preserves G), fermionTotalSpinZ_mulVec_fermionTotalSpinMinus_mulVec (Ŝ⁻ lowers the Ŝ³ weight by one), and tJ_ground_weight_finrank_le_succ — for sz ≥ 0, finrank (G ⊓ Ŝ³=sz+1) ≤ finrank (G ⊓ Ŝ³=sz) (the lowering operator injects the sz+1 weight space into the sz weight space, by the ladder injectivity at sz+1 > 0). Iterating to ½ and up from below bounds every weight space by the Ŝ³=½ block (≤1, E3a) — the route to finrank G ≤ Ne+1; axiom-free (A.17 now discharged §A.3.2; via G) |
Hubbard/TJGroundWeightFinrankRaise.lean |
Tasaki §11.5: weight-space finrank from below via Ŝ⁺ (Issue #4230 PR-E5b, the Ŝ⁺ mirror): fermionTotalSpinPlus_mulVec_mem_groundSubmodule (Ŝ⁺ preserves G), fermionTotalSpinZ_mulVec_fermionTotalSpinPlus_mulVec (Ŝ⁺ raises the Ŝ³ weight by one), and tJ_ground_weight_finrank_le_of_spinZ_neg — for sz < 0, finrank (G ⊓ Ŝ³=sz) ≤ finrank (G ⊓ Ŝ³=sz+1) (Ŝ⁺ injects the sz weight space into sz+1, by the ladder injectivity at sz < 0). With the Ŝ⁻ step this bounds every weight space by the Ŝ³=½ block (≤1, E3a) — the remaining input is the Ŝ³ direct-sum to assemble finrank G ≤ Ne+1; axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJGroundWeightOne.lean |
Tasaki §11.5: every Ŝ³ weight block of the ground subspace is ≤1-dim (Issue #4230 PR-E5b): tJ_ground_weight_finrank_le_one_pos (finrank (G ⊓ Ŝ³=½+k) ≤ 1, k:ℕ) and tJ_ground_weight_finrank_le_one_neg (finrank (G ⊓ Ŝ³=−½−k) ≤ 1). Iterating the weight-finrank steps (Ŝ⁻ from above #4307, Ŝ⁺ from below #4308) down to the Ŝ³=½ block (≤1, E3a) caps every half-integer weight space by 1; the half-integers ±½,±3/2,… exhaust the Ŝ³ spectrum at odd filling. The remaining input to the upper bound finrank G ≤ Ne+1 (with the Ŝ³ direct-sum); axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJGroundWeightDirectSum.lean |
Tasaki §11.5: Ŝ³ weight decomposition of the ground subspace (Issue #4230 PR-E5b): fermionTotalSpinZ_mulVec_mem_groundSubmodule (Ŝ³ preserves G, so G is an invariant submodule of Ŝ³), fermionTotalSpinZ_iSup_eigenspace_eq_top (Ŝ³ is diagonal on the computational basis, so its eigenspaces span ⊤), and tJ_groundSubmodule_eq_iSup_inf_eigenspace — G = ⨆ μ, G ⊓ eigenspace Ŝ³ μ (Submodule.eq_iSup_inf_genEigenspace for the invariant G). The decomposition feeding the degeneracy upper bound finrank G ≤ Ne+1 (each weight block ≤1 by #4309); axiom-free (A.17 now discharged §A.3.2; via G) |
Hubbard/TJGroundWeightReindex.lean |
Tasaki §11.5: finite Ŝ³ weight reindexing of the ground subspace (Issue #4230 PR-E5b): tJ_groundSubmodule_inf_eigenspace_eq_bot (off-weight blocks vanish — G ⊓ eigenspace Ŝ³ μ = ⊥ for μ outside {a − Ne/2 : a ∈ Fin (Ne+1)}, since a ground vector is an N̂=Ne and Ŝ³=μ eigenstate so every supported configuration forces μ = #↑ − Ne/2) and tJ_groundSubmodule_eq_iSup_weight — G = ⨆ a : Fin (Ne+1), G ⊓ eigenspace Ŝ³ (a − Ne/2), the finite weight decomposition (all-ℂ supremum collapses to the Ne+1 occurring half-integer weights). Feeds the degeneracy upper bound finrank G ≤ Ne+1; axiom-free (A.17 now discharged §A.3.2; via G) |
Hubbard/TJGroundDegeneracyUpper.lean |
Tasaki §11.5: ground-state degeneracy upper bound finrank G ≤ Ne+1 (Issue #4230 PR-E5b): tJ_groundSubmodule_finrank_le — assembling the finite Ŝ³ weight decomposition (tJ_groundSubmodule_eq_iSup_weight) with the per-block bound (tJ_ground_weight_finrank_le_one_pos/_neg, ≤1) gives finrank G ≤ Ne+1. The Ne+1 half-integer weight blocks are independent (Module.End.eigenspaces_iSupIndep) so they form an internal direct sum of G (DirectSum.coeLinearMap injective + Module.finrank_directSum); finrank G = ∑ finrank (block) ≤ (Ne+1)·1. Paired with the SU(2)-tower lower bound (tJ_groundSubmodule_finrank_ge, #4305) this pins finrank G = Ne+1 — the input to the maximal-spin multiplet capstone (E6); axiom-free (A.17 now discharged §A.3.2) |
Hubbard/TJHalfFillingKinetic.lean |
Tasaki §11.5.3: the t-J kinetic term vanishes at half-filling (Issue #4314 PR1, towards Theorem 11.26): tJ_hop_apply_tJConfigOf_eq_zero_of_full (a single hop ĉ†_{i,σ}ĉ_{j,σ} on a fully-occupied |Φ_s⟩, evaluated at any sector config, is 0 — the only nonzero target is doubly occupied at site i, hence not hard-core) and tJ_kinetic_sandwich_mulVec_tJConfigOf_eq_zero_of_full (P̂hc·K·P̂hc |Φ_s⟩ = 0 for ∀ k, s k ≠ 0, i.e. Ne = N+1). So at half-filling Ĥ_tJ reduces to its exchange (ferromagnetic Heisenberg) part — the first step toward the Ne = K+1 boundary case of Theorem 11.26. Axiom-free |
Hubbard/TJHalfFillingExchange.lean |
Tasaki §11.5.3: at half-filling the t-J Hamiltonian reduces to its exchange part (Issue #4314 PR2): tJExchange N G (the Heisenberg interaction Σ_{x,y}[G.Adj](n̂_x n̂_y/4 − Ŝ_x·Ŝ_y), the second summand of tJHamiltonian) and tJHamiltonian_mulVec_tJConfigOf_eq_of_full — Ĥ_tJ |Φ_s⟩ = J · tJExchange |Φ_s⟩ for a fully-occupied s (the kinetic term vanishes, #4315). At half-filling Ĥ_tJ is the ferromagnetic Heisenberg model — the boundary case Ne = K+1 of Theorem 11.26. Axiom-free |
Hubbard/TJAllUpSpinDot.lean |
Tasaki §11.5.3: the spin dot product on the all-up state (Issue #4314 PR3a): fermionSiteSpinPlus_mulVec_allUpState (Ŝ⁺_i|↑…↑⟩=0), fermionSiteSpinZ_mulVec_allUpState (Ŝ³_i|↑…↑⟩=½|↑…↑⟩), and fermionSpinDot_mulVec_allUpState (Ŝ_i·Ŝ_j|↑…↑⟩=¼|↑…↑⟩ for i≠j). The off-diagonal Ŝ⁺_iŜ⁻_j/Ŝ⁻_iŜ⁺_j annihilate |↑…↑⟩ (the latter via Ŝ⁺_j|↑…↑⟩=0, the former since ĉ_{i↓} commutes through the different-site Ŝ⁻_j to hit the down-free |↑…↑⟩), leaving the diagonal Ŝ³_iŜ³_j=¼. The maximal-spin alignment input for the half-filling ground energy (Theorem 11.26). Axiom-free |
Hubbard/TJAllUpGround.lean |
Tasaki §11.5.3: the t-J Hamiltonian annihilates the all-up state (Issue #4314 PR3b): fermionSiteNumber_mulVec_allUpState (n̂_x|↑…↑⟩=|↑…↑⟩), hubbardAllUpState_eq_tJConfigOf (|↑…↑⟩ = basisVec (tJConfigOf (fun _↦1))), tJExchange_mulVec_allUpState_eq_zero (each bond ¼n̂_xn̂_y−Ŝ_x·Ŝ_y gives ¼−¼=0), and tJHamiltonian_mulVec_allUpState_eq_zero — Ĥ_tJ|↑…↑⟩=0 at half-filling (kinetic vanishes #4315/#4316, exchange vanishes via #4317). So the maximal-spin |↑…↑⟩ is a zero-energy eigenstate of the half-filling ferromagnetic Heisenberg model. Axiom-free |
Hubbard/TJSingletAnnihilation.lean |
Tasaki §11.5.3: the singlet annihilation operator (Issue #4314 PR3c-prep): tJSingletAnnihilation x y (Δ_xy = ĉ_{y↓}ĉ_{x↑} − ĉ_{y↑}ĉ_{x↓}), tJSingletAnnihilation_conjTranspose (Δ_xy† = ĉ†_{x↑}ĉ†_{y↓} − ĉ†_{x↓}ĉ†_{y↑}), and tJSingletAnnihilation_mulVec_allUpState (Δ_xy|↑…↑⟩=0 — the singlet annihilator kills the fully aligned state, via one cross-site anticommutator). The Heisenberg bond n̂_x n̂_y/4 − Ŝ_x·Ŝ_y = ½ Δ_xy† Δ_xy (PSD, follow-up); |↑…↑⟩ then has bond energy 0. Axiom-free |
Hubbard/TJCrossSiteSpinCommute.lean |
Tasaki §11.5.3: cross-site annihilation–site-spin commutators (Issue #4314 PR3c): fermionUpAnnihilation_commute_fermionSiteSpinPlus_of_ne ([ĉ_{x↑}, Ŝ⁺_y]=0) and fermionDownAnnihilation_commute_fermionSiteSpinMinus_of_ne ([ĉ_{x↓}, Ŝ⁻_y]=0) for x≠y (disjoint JW orbitals, via the CAR anticommutators + linear_combination (norm:=noncomm_ring)). The reordering inputs for the singlet-annihilation bond identity. Axiom-free |
Hubbard/TJExchangeBondPSD.lean |
Tasaki §11.5.3: the Heisenberg-bond CAR identity (Issue #4314 PR3c): tJSingletAnnihilation_conjTranspose_mul_self — Δ_xy† Δ_xy = n̂_{x↑}n̂_{y↓} + n̂_{x↓}n̂_{y↑} − Ŝ⁺_x Ŝ⁻_y − Ŝ⁻_x Ŝ⁺_y for x≠y, by expanding the four products of Δ_xy† Δ_xy and reordering with the cross-site (anti)commutators + number commutes. This is the operator content behind n̂_x n̂_y/4 − Ŝ_x·Ŝ_y = ½ Δ_xy† Δ_xy ⇒ the bond is positive-semidefinite (follow-up). Axiom-free |
Hubbard/TJExchangeBondHalf.lean |
Tasaki §11.5.3: the Heisenberg bond is ½ Δ_xy† Δ_xy, hence PSD (Issue #4314 PR3d): tJExchangeBond_eq_half_singletNormSq (n̂_x n̂_y/4 − Ŝ_x·Ŝ_y = ½ (Δ_xy† Δ_xy) for x≠y, from the CAR identity #4320 + ℂ-smul algebra match_scalars) and tJExchangeBond_posSemidef (the bond is positive-semidefinite, via Matrix.posSemidef_conjTranspose_mul_self ½-smul). The per-bond PSD input to the half-filling ground energy =0. Axiom-free |
Hubbard/TJExchangePSD.lean |
Tasaki §11.5.3: the t-J exchange operator is positive-semidefinite (Issue #4314 PR3e): tJExchange_posSemidef — (tJExchange N G).PosSemidef, a graph sum of per-bond singlet projectors (tJExchangeBond_posSemidef, each PSD; off-bond summands 0), via Finset.sum_induction + Matrix.PosSemidef.add/.zero. The operator nonnegativity behind the half-filling ground energy =0 (all-up sits at the bottom). Axiom-free |
Hubbard/TJHalfFillingReduction.lean |
Tasaki §11.5.3: the half-filling reduction on the whole sector (Issue #4314 PR3f): tJFillingSector_full (a half-filling Ne=N+1 sector config is fully occupied — filter(=1)∪filter(=2)=univ), tJ_kinetic_sandwich_mulVec_eq_zero_of_filling (P̂hc K P̂hc v=0 for any hard-core N̂=N+1 v, by tJ_filling_completeness + per-basis #4315 + linearity), and tJHamiltonian_mulVec_eq_smul_tJExchange_of_filling (Ĥ_tJ v = J·tJExchange v for such v). So on the half-filling sector Ĥ_tJ = J·tJExchange (ferromagnetic Heisenberg) — the bridge to the ground energy =0. Axiom-free |
Hubbard/TJAllUpProperties.lean |
Tasaki §11.5.3: filling facts for the all-up state (Issue #4314 PR3g): hubbardAllUpState_ne_zero, hubbardAllUpState_mem_hardcore, fermionTotalNumber_mulVec_allUpState (N̂|↑…↑⟩=(N+1)|↑…↑⟩, via hubbardAllUpState_eq_tJConfigOf + fermionTotalNumber_mulVec_tJConfigOf_eq). Reusable for the ground energy and the SU(2) lower bound. Axiom-free |
Hubbard/TJHalfFillingGroundEnergy.lean |
Tasaki §11.5.3: the half-filling ground energy is 0 (Issue #4314 PR3g): tJ_groundEnergyAtFilling_eq_zero — groundEnergyAtFilling Ĥ_tJ (N+1) = 0. ≤0 from the all-up eigenvector at 0 (groundEnergyAtFilling_le_of_eigenvector + #4318); ≥0 from tJExchange.PosSemidef (#4323) on the filling sector (Ĥ_tJ=J·tJExchange #4324, le_ciInf, rayleigh =J·⟨φ,exchange φ⟩.re≥0, J>0; Nonempty witness = unit all-up). Axiom-free |
Hubbard/TJHalfFillingDegeneracyLower.lean |
Tasaki §11.5.3: half-filling ground degeneracy lower bound (Issue #4314 PR3h): tJ_halfFilling_groundSubmodule_finrank_ge — N+2 ≤ finrank of the half-filling (Ne=N+1) ground subspace. The all-up state is a highest-weight ground state (Ŝ⁺|↑…↑⟩=0, Ŝ³=((N+1)/2), Ĥ_tJ|↑…↑⟩=0=groundEnergy·|↑…↑⟩ #4318/#4325, N̂=N+1, hard-core), so the SU(2) tower highestWeight_spinMultiplet_general yields N+2 LI ground states (Ŝ⁻)^k|↑…↑⟩ (mirrors #4305). Axiom-free |
Hubbard/TJHalfFillingBondAction.lean |
Tasaki §11.5.3: the exchange bond is a half spin-swap on the filled sector (Issue #4314 PR3i): tJExchangeBond_mulVec_tJConfigOf_full — for x≠y and a fully occupied |Φ_s⟩, (¼ n̂_x n̂_y − Ŝ_x·Ŝ_y)|Φ_s⟩ = ½(|Φ_s⟩ − |Φ_{tJSpinSwap s x y}⟩). Diagonal ¼ n̂n̂ − Ŝ³Ŝ³ + ladder ½(Ŝ⁺Ŝ⁻+Ŝ⁻Ŝ⁺) via the sign-free spin-swap (fermionSiteSpinPlus_mul_Minus_mulVec_tJConfigOf) over the 4 spin cases; helper source/target ladder-vanishing lemmas. So a ground state of tJExchange has spin-swap-invariant bond amplitudes — input to the degeneracy upper bound. Axiom-free |
Hubbard/TJHalfFillingBondGround.lean |
Tasaki §11.5.3: a half-filling ground state is annihilated by every bond (Issue #4314 PR3i-2): tJ_ground_tJExchange_mulVec_eq_zero (tJExchange v = 0 on the half-filling ground subspace, via groundEnergy=0 #4325 + Ĥ_tJ=J·tJExchange #4324, J>0) and tJ_ground_bond_mulVec_eq_zero ((¼ n̂_x n̂_y − Ŝ_x·Ŝ_y) v = 0 for every adjacent bond): each bond inner product is a nonnegative summand of ⟨v,tJExchange v⟩=0 (tJExchangeBond_posSemidef + Finset.single_le_sum), hence 0, so Δ_xy v=0 (bond=½Δ†Δ, dotProduct_star_self_eq_zero) and bond_xy v=0. With PR3i-1 ⟹ spin-swap-invariant ground amplitudes on every bond. Axiom-free |
Hubbard/TJHalfFillingAmplitude.lean |
Tasaki §11.5.3: half-filling ground amplitudes are spin-swap invariant (Issue #4314 PR3i-3a): tJFillingSwap (the spin-swap as a sector permutation, involutive) and tJ_ground_amplitude_swap_invariant — for a ground state v and adjacent bond ⟨x,y⟩, v (tJConfigOf s) = v (tJConfigOf (tJSpinSwap s x y)). Expand v in the filling basis (tJ_filling_completeness), apply the bond (bond_xy v=0 #4328) which acts as a half spin-swap (#4327), and read off the coefficient at index tJConfigOf s (basisVec orthonormality, tJConfigOf_injective, swap involution). Toward the up-count classification of ground amplitudes. Axiom-free |
Hubbard/TJHalfFillingUpCount.lean |
Tasaki §11.5.3: half-filling ground amplitudes depend only on the up-count (Issue #4314 PR3i-3b): tJ_upDownCount_of_full (full config ⟹ #↑+#↓=N+1) + tJ_ground_amplitude_eq_of_same_upCount — for sector configs t, t' with equal up-counts, v (tJConfigOf t) = v (tJConfigOf t'). The per-bond spin-swap invariance (#4329) propagates: equal up-counts ⟹ equal value-counts ⟹ adjacent-swap reachable (adjacentSwapReachable_of_same_counts, Prop 11.24 route) ⟹ amplitudes equal (AdjacentSwapReachable induction, each step an adjacent bond swap). Ground amplitudes are constant on each of the N+2 up-count classes. Axiom-free |
Hubbard/TJHalfFillingDegeneracyUpper.lean |
Tasaki §11.5.3: half-filling ground degeneracy upper bound (Issue #4314 PR3i-3c): tJUpCountRep (representative config with j up-spins) + tJ_halfFilling_groundSubmodule_finrank_le — finrank G ≤ N+2. A ground state is determined by its amplitudes (tJ_filling_completeness), which are constant on each up-count class (#4330), so evaluation at one representative per class is an injective linear map G ↪ (Fin (N+2) → ℂ) (LinearMap.finrank_le_finrank_of_injective). With the lower bound #4326 this pins finrank G = N+2. Axiom-free |
Hubbard/TJHalfFillingMaximalSpin.lean |
Tasaki §11.5.3: the half-filling t-J ground subspace is the maximal-spin multiplet (Issue #4314 PR3-cap): tJ_halfFilling_isMaximalSpinMultiplet — IsMaximalSpinMultipletSubmodule N G (N+1) (ground S_tot=(N+1)/2, (N+2)-fold degenerate). Assembles finrank G=N+2 (le_antisymm of #4331 upper + #4326 lower) with the maximal (Ŝ_tot)² eigenvalue on the all-up SU(2) tower (which spans G since its N+2 LI members exhaust the dimension, span_eq_top_of_card_eq_finrank). The boundary (Ne=N+1) case of the t-J side of Theorem 11.26, half-filling counterpart of proposition_11_24. Axiom-free (no A.17 needed) |
Hubbard/TJMaximalSpinUnified.lean |
Tasaki §11.5: the d=1 ferromagnetic t-J ground subspace is the maximal-spin multiplet for all Ne ≤ K+1 (Issue #4314 PR-unify): tJ_isMaximalSpinMultiplet_of_le — for odd Ne ≤ K+1 and τ,J>0, IsMaximalSpinMultipletSubmodule K (groundSubmoduleAtFilling (tJHamiltonian K (cycleGraph (K+1)) τ J) Ne) Ne. Combines the metallic case Ne < K+1 (proposition_11_24) with the half-filling case Ne = K+1 (tJ_halfFilling_isMaximalSpinMultiplet). The half-filling chain was generalized to drop the 0 < N hypothesis (adjacentSwapReachable_of_same_counts_general handles N=0 by reflexivity), so the K=0 boundary is covered. The t-J input to theorem_11_26 (rests on A.17 via Prop 11.24) |
Hubbard/GroundSubspaceAtFilling.lean |
Generic fixed-electron-number hard-core ground subspace (Tasaki §11.5): fillingHardcoreStates M Ne (unit vectors at fixed N̂=Ne in the no-double-occupancy subspace H_{Ne}^hc), groundEnergyAtFilling H Ne (⨅ rayleighOnVec H over them), groundSubmoduleAtFilling H Ne (H-eigenspace at the ground energy ⊓ N̂=Ne ⊓ hubbardHardcoreSubspace). Shared by Proposition 11.24 (t-J) and Theorem 11.26 (decorated Hubbard); axiom-free |
Hubbard/MetallicFerroModel.lean |
Tasaki §11.5.3 the d=1 decorated Hubbard model + Lemma 11.25 + Theorem 11.26 (AXIOMATIZED, Issue #4198): the duplicated-internal-site lattice Λ = E ∪ (I×{1,2}) packed into Fin (3K+3) (decExternalSite/decInternalSite1/decInternalSite2); localized states decAlpha/decBeta1/decBeta2 (eqs. (11.5.7)–(11.5.9)) + fermion ops decACreation/Annihilation, decBCreation/Annihilation (eq. (11.5.10), Ĉσ(φ)); decHopping (t Σ b̂†b̂ − s Σ_{⟨p,q⟩∈E,σ} â†_pâ_q, eq. (11.5.14)) + decInteraction (U Σ n̂↑n̂↓, eq. (11.5.13)) + decHubbardHamiltonian = decHopping + decInteraction. axiom lemma_11_25 (t,U↑∞ Hubbard ≡ J↑∞ t-J at τ=(1+4ν²)s, rendered as the spin-structure transfer: in the limits the Hubbard ground subspace is the maximal-spin Ne+1-multiplet iff the t-J one is) and axiom theorem_11_26 (d=1, Ne≤K+1=|E| odd (Tasaki’s N≤L) ⇒ IsMaximalSpinMultipletSubmodule (3K+2) (groundSubmoduleAtFilling (decHubbardHamiltonian …) Ne) Ne for large t,U — ground S_tot=Ne/2, Ne+1-fold; metallic when Ne<K+1). Model axiom-free; the two limit theorems documented axioms (Issue #4198) |
Hubbard/SpinfulVectorOperator.lean |
Generic single-particle-state fermion operators: spinfulCreationFromVector M (φ : Fin(M+1)→ℂ) σ = Ĉ†_σ(φ) = Σ_x φ(x) ĉ†_{x,σ} and spinfulAnnihilationFromVector (the Ĉ_σ(φ) construction shared by all decorated-lattice models; used by the §11.5.4 Tanaka–Tasaki operators). Axiom-free |
Hubbard/TanakaTasakiModel.lean |
Tasaki §11.5.4 the Tanaka–Tasaki model + Theorem 11.27 (AXIOMATIZED, Issue #4198) — the §11.5 / Chapter 11 capstone: the heavily-decorated lattice Λ = E×{1,2,3} ∪ I×{1,2} (externals triplicated, internals duplicated), d=1 packed into Fin(5K+5) (ttExtSite/ttIntSite); special single-particle states ttAlpha/ttBeta/ttDeltaP/ttDeltaI (eqs. (11.5.19)–(11.5.22); â carries the 1/√(3+4ν²) normalisation) + fermion ops ttA/B/DeltaP/DeltaICreation/Annihilation (via spinfulCreationFromVector); ttHopping (Σ_{⟨p,q⟩}(−s â†â − t b̂†b̂) + u₁ Σ b̂†b̂ + u₂ Σ d̂†d̂, eq. (11.5.24)) + ttInteraction (U Σ n̂↑n̂↓) + ttHamiltonian (finite); plus the genuine u₂,U↑∞ limit objects ttDKernel (d̂Φ=0 finite-energy subspace, via Theorem A.12/Lemma A.11) + ttEffectiveHamiltonian (the u₂,U=∞ effective â/b̂ hopping). axiom theorem_11_27 (d=1, u₁>2(|s|+2|t|), K+1≤Ne≤2(K+1) (Tasaki’s L^d≤N≤2L^d) ⇒ in the limit every ground state in groundSubmoduleAtFilling (ttEffectiveHamiltonian …) Ne ⊓ ttDKernel has maximum total spin S_tot=Ne/2, i.e. is an (Ŝ_tot)² eigenvector at (Ne/2)(Ne/2+1); the limit is taken faithfully — not finite thresholds, since Tasaki proves it only in the limit and warns finite u₂,U is not expected to work; weaker than the full multiplet predicate since Tasaki claims only the spin; metallic when 1<Ne/L<2). Model axiom-free; theorem_11_27 documented axiom (Tasaki cites [63]). Completes §11.5 / Chapter 11 |
Hubbard/WannierExampleModel.lean |
Tasaki §11.4.1 (Wannier-perturbation example model, eq. (11.4.1)): §11.4.1 is heuristic/non-rigorous (no numbered theorems); its one formalisable object is the example model — the 1D flat-band model with the internal on-site potential shifted by γ. wannierExamplePerturbation K (internal-site, odd-index, diagonal indicator); wannierExampleModel K ν t γ U = nonsingularHubbardHamiltonian K ν t (γ·t) (wannierExamplePerturbation K) U (the γ t Σ_{u∈I} n̂_u shift as a non-singular instance); wannierExampleModel_isHermitian; wannierExampleModel_gamma_zero: γ=0 ⇒ = flatBandHamiltonian (eq. (11.4.1) reduces to (11.3.22)). Explicitly covers §11.4.1 in book order; axiom-free (Issue #4189) |
Hubbard/TranslationOperator.lean |
Tasaki §11.4.2 (lattice translation on the decorated chain, towards Theorem 11.19): the combinatorial datum for the fermionic translation operator τ̂_z (eq. (11.4.30)). modeSiteSpinEquiv K factors the spinful mode space Fin(2(2K+1)+2) = Fin((2K+2)·2) as (physical site) × (spin) (mode 2p+σ ↔ (p,σ)); siteShiftAmount K z = 2z (one cell = two physical sites); siteTranslationPerm K z = the Equiv.Perm shifting the physical site by 2z cyclically (via finCycle), spin fixed; siteTranslationPerm_zero (z=0 ⇒ identity). Step 1 of Theorem 11.19 (signed τ̂ operator + E_SW(k) + axiom to follow); axiom-free (Issue #4189) |
Hubbard/FermionicTranslation.lean |
Tasaki §11.4.2 fermionic translation operator τ̂_z (eq. (11.4.30)) — step 2 of Theorem 11.19. translationJwSign π σ = (-1)^(occupied inversions of π) (the Jordan–Wigner sign from reordering shifted creation operators; translationJwSign_sq: it is ±1); translationOperator K z = the signed permutation operator Matrix.of (fun τ σ => if τ = σ∘π⁻¹ then translationJwSign π σ else 0) (π = siteTranslationPerm K z); translationOperator_mulVec_basisVec: the defining action τ̂_z|σ⟩ = ε(π,σ)·|σ∘π⁻¹⟩ (eq. (11.4.30)); translationOperator_zero (z=0 ⇒ = 1). Axiom-free; E_SW(k) + axiom Theorem 11.19 to follow (Issue #4189) |
Hubbard/SpinWaveExcitation.lean |
Tasaki §11.4.2 Theorem 11.19 (spin-wave excitation bounds, AXIOMATIZED) — completes §11.4.2. momentumPhase K k = e^{-2πik/(K+1)}; spinWaveEnergy K H k = E_SW(k) = ⨅ rayleighOnVec H over unit EuclideanSpace states in the joint eigenspace Ŝ^z_tot=(K−1)/2 (=S_max−1) ∩ τ̂ (translationOperator K 1) =momentumPhase; axiom nonsingular_theorem_11_19: ∃ ν₁,η₁,ξ₁,ξ₂,a₁..b₃>0 (uniform, dep. d=1,R) s.t. under (11.4.31)/(11.4.32) the dispersion E_SW(k)−E_min(S_max) is two-sided bounded by F·2ν⁴U(1−cos k) (eq. (11.4.33), F₁/F₂ = (11.4.34)/(11.4.35)). Deep perturbation-theory result, deferred (Issue #4189; Theorem 11.8/11.13 policy) |
Hubbard/NagaokaBondGraph.lean |
Tasaki §11.2.2 graph predicates: the bond graph of a hopping amplitude (nagaokaBondGraph), biconnectedness (IsBiconnected), the simple-loop predicate (IsSimpleLoopGTFour), exchange bonds (E1 common length-3/4 loop + E2 deletion-connectedness, IsExchangeBond), the exchange-bond graph, and ConnectedByExchangeBonds — the vocabulary of Theorem 11.8 and Lemma 11.9, split out so the Lemma 11.9 proof machinery can use it without the Theorem 11.8 axiom (Tasaki §11.2.2) |
Hubbard/NagaokaConnectivityClassification.lean |
Tasaki Theorem 11.8 (AXIOMATIZED) + Lemma 11.9 (PROVED, axiom discharged): the connectivity classification (nagaoka_theorem_11_8: connectivity ⟺ biconnected ∧ not a simple loop >4 sites) stays an axiom — its proof is left by Tasaki to external papers (Bobrow–Stubis–Li / Wilson 15-puzzle); Theorem 11.7 does not depend on it. nagaoka_lemma_11_9 (exchange-bond-connected ⇒ connectivity) is now a proved theorem at its original path: the diagonal-zeroing transfer (tasakiEffReMatrix_zeroDiag, nagaokaBondGraph_zeroDiag — neither the matrix nor the bond graph reads diag t) reduces it to the zero-diagonal capstone of NagaokaStateQuiver.lean (Tasaki §11.2.2) |
Hubbard/NagaokaStateQuiver.lean |
Tasaki Lemma 11.9 proof machinery (the “15-puzzle” hole-motion argument): edge characterisation of the −M quiver (neg_tasakiEffReMatrix_pos_iff) + StateReach reachability; loop-trip spin swaps (length-3 transposition, length-4 once/twice Boolean trips for diagonal and adjacent pairs, Figs. 11.8–11.9 + footnote 14); controlled hole transport with exact round-trip restoration (holeWalkTransport, swap_via_landing_walk); E2 routing (exists_avoiding_walk_of_induce_connected); the exchange-bond bridge (reachSwap_of_isExchangeBond); swap generation along exchange-bond walks with avoid-set bookkeeping (ReachSwapOff.of_walk, footnote 13); the farthest-vertex parking lemma (exists_vertex_walks_avoid); the mismatch-reduction induction (StateReach.of_swaps_of_holeSpinMag_eq); sector irreducibility from reachability (nagaokaConnectivity_of_reach); and the zero-diagonal capstone nagaokaConnectivity_of_connectedByExchangeBonds powering nagaoka_lemma_11_9 — all sorry-free, axiom-clean (Tasaki §11.2.2, pp. 386–388) |
Hubbard/DoubleOccupancyProjection.lean |
site-i Commute n_↑ n_↓ + idempotent product |
Hubbard/DoubleOccupancyCommute.lean |
cross-site Commute (n_↑(i)·n_↓(i)) (n_↑(j)·n_↓(j)) |
Hubbard/SpinfulNumberHermitian.lean |
n_↑(i), n_↓(i), n_↑(i)·n_↓(i) Hermitian |
Hubbard/SitePartitionIdentity.lean |
per-site p_∅+p_↑+p_↓+p_⇈ = 1 (4-state partition) |
Hubbard/SiteProjectionsIdempotent.lean |
(p_∅)² = p_∅, (p_↑)² = p_↑, (p_↓)² = p_↓ |
Hubbard/SiteProjectionsDoublyEmpty.lean |
p_⇈ · p_∅ = 0, p_∅ · p_⇈ = 0 |
Hubbard/SiteProjectionsHermitian.lean |
p_∅, p_↑, p_↓ Hermitian (companions to PR #1007) |
Hubbard/SiteProjectionsUpDown.lean |
p_↑ · p_↓ = 0, p_↓ · p_↑ = 0 |
Hubbard/SiteProjectionsEmptySingle.lean |
p_∅ ⊥ p_↑, p_∅ ⊥ p_↓ (both orderings) |
Hubbard/SiteProjectionsSingleDoubly.lean |
p_↑ ⊥ p_⇈, p_↓ ⊥ p_⇈ (completes 6/6 ortho.) |
Hubbard/SiteProjectionsSpinResolved.lean |
p_↑+p_⇈ = n_↑, p_∅+p_↑ = 1−n_↓, etc. |
Hubbard/SiteProjectionsCommute.lean |
same-site Commute p_α p_β (all 6 pairs) |
Hubbard/SiteProjectionsPow.lean |
per-site (p_α)^(k+1) = p_α (all 4 projections) |
Hubbard/EmptyProjectionCommute.lean |
cross-site Commute (p_∅(i)) (p_∅(j)) |
Hubbard/SingleProjectionsCommute.lean |
cross-site Commute (p_↑(i)) (p_↑(j)), (p_↓) |
Hubbard/UpDownProjectionCommute.lean |
Commute (p_↑(i)) (p_↓(j)) for any i, j |
Hubbard/RemainingProjectionCommutes.lean |
remaining 5 cross-projection commutes (16/16 total) |
CPlusCDaggerSq.lean |
(c_i + c_i†)² = 1 (multi-mode σ_x-analog) |
CMinusCDaggerSq.lean |
(c_i − c_i†)² = −1 (multi-mode iσ_y-analog) |
CPlusMinusCDaggerPauli.lean |
(c_i ± c_i†) Pauli-X/iY-analog full structure |
OneSubTwoNumberSq.lean |
(1 − 2·n_i)² = 1 (σ_z analog involution) |
CPlusCDaggerAnticomm.lean |
cross-site {c_i+c_i†, c_j+c_j†} = 0 |
CMinusCDaggerAnticomm.lean |
cross-site {c_i−c_i†, c_j−c_j†}=0, {+,−}=0 |
NumberCommutePauliOfNe.lean |
Commute n_i (c_j ± c_j†) for i ≠ j |
(Refactor Phase 2 PR 14, plan v4 §3.1. JordanWigner extraction complete.)