Interim authority. This lossless catalogue chunk remains authoritative for formalization status and capstone identification until Issue #5228. The version 1 JSON catalogue is still a non-authoritative prototype.
Interim catalogue › Fermions and Hubbard models
| Lean name | Statement | File |
|—|—|—|
| exists_eq_hubbardOneHoleConfig_of_isOneHoleHardcore | surjectivity: every one-hole hard-core configuration equals hubbardOneHoleConfig N x σ for some (x, σ) | Fermion/JordanWigner/Hubbard/HardcoreSpan.lean |
| hubbardOneHoleHardcoreSector N | the one-hole hard-core sector H_hc^N (span of the one-hole hard-core basis configurations) | Fermion/JordanWigner/Hubbard/HardcoreSpan.lean |
| hubbardOneHoleHardcoreSector_eq_span_basisState | Tasaki §11.2 footnote 8: H_hc^N is spanned by the basis states \|Φ_{x,σ}⟩ | Fermion/JordanWigner/Hubbard/HardcoreSpan.lean |
| hubbardHardcoreBasisState_mem_sector | each basis state lies in the one-hole hard-core sector | Fermion/JordanWigner/Hubbard/HardcoreSpan.lean |
| Lean name | Statement | File |
|---|---|---|
hubbardSpinMove N σ x y |
σ_{y→x}: σ with the spin at x set to σ y (the electron moved from y to the hole x) |
Fermion/JordanWigner/Hubbard/HopConfig.lean |
hubbardOneHoleConfig_hop |
filling the hole x with an electron of spin s hopped from y turns the configuration of \|Φ_{x,σ}⟩ into that of \|Φ_{y, σ_{y→x}}⟩ |
Fermion/JordanWigner/Hubbard/HopConfig.lean |
hubbardHop_mulVec_hardcoreBasisState |
operator content of (11.2.4): c†_{(x,s)} c_{(y,s)} \|Φ_{x,σ}⟩ = (jwSign·jwSign) • \|Φ_{y, σ_{y→x}}⟩ (create at hole x, annihilate at occupied y) |
Fermion/JordanWigner/Hubbard/HopAction.lean |
hubbardHopTerm_inner_hardcoreBasisState |
per-term content of (11.2.5): the matrix element ⟨Φ_{y,τ}\| c†_{(x,s)} c_{(y,s)} \|Φ_{x,σ}⟩ is the JW sign product times the indicator τ = σ_{y→x} |
Fermion/JordanWigner/Hubbard/HopMatrixElement.lean |
| Lean name | Statement | File |
|---|---|---|
hoppingSupportGraph / hubbardOnSiteInteractionSite / attractiveHubbardInteraction / attractiveHubbardHamiltonian |
the attractive Hubbard model Ĥ = Ĥhop + Ĥatt-int (eqs. (10.2.1)/(10.2.2)): general real symmetric hopping T (via hubbardKinetic) + site-dependent attraction −Σ_x U_x n̂_{x,↑} n̂_{x,↓}; the support graph encodes the connectivity hypothesis |
Fermion/JordanWigner/Hubbard/LiebAttractive.lean |
electronNumberSectorEuclidean / hubbardPairCorrelationOp / euclideanExpectation |
the N-electron sector (number eigenspace), the pair-transfer operator ĉ†_{x↑}ĉ†_{x↓}ĉ_{y↓}ĉ_{y↑}, and Euclidean expectation values |
Fermion/JordanWigner/Hubbard/LiebAttractive.lean |
theorem_10_2_lieb_attractive_unique_singlet |
Theorem 10.2 (Tasaki §10.2.1, p. 348, PROVED, axiom-free): for an even electron number N with 0 < N ≤ 2\|Λ\|, connected real symmetric hopping, and site-dependent attraction U_x > 0, the ground state of Ĥ in the N-electron sector is unique and a spin singlet ((Ŝ_tot)² = 0). Discharged from the plain-space full-sector singlet-uniqueness milestone via Lieb’s spin-space reflection positivity on the balanced block lifted through the SU(2) multiplet engine; assembled into the Euclidean IsUniqueGroundStateOn predicate. |
Fermion/JordanWigner/Hubbard/LiebAttractiveTheorem102.lean |
theorem_10_3_tian_pair_correlation_positive |
Theorem 10.3 (Tian; Tasaki §10.2.1–§10.2.4, p. 349, eq. (10.2.4) + p. 367, eqs. (10.2.50)/(10.2.51), PROVED, axiom-free, PR #4949): under the Theorem 10.2 hypotheses (with the non-full guard N < 2\|Λ\|), the unique ground state of the attractive Hubbard model has strictly positive on-site pair-transfer correlation ⟨ΦGS\| ĉ†_{x↑}ĉ†_{x↓}ĉ_{y↓}ĉ_{y↑} \|ΦGS⟩ > 0 for all x, y (off-diagonal long-range order / pair condensation). Tian’s extension of Lieb’s reflection positivity → the pair-hopping transfer matrix S on the balanced-sector configuration space factorizes the matrix element through the sector compression (hubbardCountSectorEmbedding), yielding ⟨φ| P |φ⟩ = Tr(W·S·W·Sᴴ) with W = blockWCoeff φ the unique ground’s coefficient matrix (Euclidean IsUniqueGroundStateOn lifted from Theorem 10.2); the balanced compression S_c = Jᴴ·S·J is nonzero (hubbardCountSectorEmbedding_pairFixed_compress_ne_zero), and with W = c⁻¹·W_bal (collinearity via uniqueness) where W_bal = J·R·Jᴴ and R is positive definite (exists_posDefCompress_ground_in_balanced_sector), the trace reduces to |c⁻¹|²·Tr(R·(S_cᴴ·R·S_c)), which is strictly positive by the positive-definite/positive-semidefinite trace lemma (trace_mul_posSemidef_pos). With symmetric T, U(x) > 0, kinetic-graph connectivity. |
Fermion/JordanWigner/Hubbard/LiebAttractiveTheorem103.lean |
The finite-dimensional spin-reflection-positivity (SRP) coefficient-matrix language in which Lieb’s proof is stated (the first layer toward discharging theorem_10_2_lieb_attractive_unique_singlet; the Hamiltonian positivity / Perron–Frobenius uniqueness / singlet argument are later layers). All axiom-free.
| Lean name | Statement | File | |
|---|---|---|---|
hubbardSpinConfig / hubbardUpConfig / hubbardDownConfig / hubbardMergeConfig / hubbardSpinConfigEquiv |
the basis-level factorization H = H↑ ⊗ H↓: a spin-orbital configuration Fin (2N+2) → Fin 2 is the same data as a pair of single-species configurations (up, down) (via spinfulIndex), packaged as an Equiv |
Fermion/JordanWigner/Hubbard/LiebAttractiveReflection.lean |
|
hubbardSpinCoeffLinearEquiv |
the induced linear isomorphism of a state vector with its coefficient matrix M_{u,d} = ψ (merge u d) indexed by up/down configurations |
Fermion/JordanWigner/Hubbard/LiebAttractiveReflection.lean |
|
flipOccupation / particleHoleConfig / spinReflectionConfig / spinReflectionThetaVec |
the spin reflection θ (antiunitary spin-flip ∘ particle–hole, (n↑,n↓) ↦ (1−n↓,1−n↑)) at the configuration and state-vector level; particleHoleConfig_involutive, spinReflectionConfig_involutive, spinReflectionThetaVec_smul (conjugate-linear), spinReflectionThetaVec_dotProduct (⟨θψ,θφ⟩ = conj⟨ψ,φ⟩, antiunitarity) |
Fermion/JordanWigner/Hubbard/LiebAttractiveReflection.lean |
|
spinReflectionCoeff / SpinReflectionPositive / spinReflectionCoeff_thetaVec / spinReflection_gramMatrix_nonneg |
the SRP coefficient matrix (down index read as a hole), its positive-semidefiniteness predicate, the θ-on-coefficients = conjugate-transpose law, and the reusable nonnegativity 0 ≤ Re tr (C A C Aᴴ) for C positive-semidefinite (the algebraic heart of SRP, via C = B² and tr (C A C Aᴴ) = tr (M Mᴴ)) |
Fermion/JordanWigner/Hubbard/LiebAttractiveReflection.lean |
|
hubbardConfigInteractionWeight / hubbardOnSiteInteractionSite_mulVec_basisVec / hubbardOnSiteInteractionSite_mulVec_apply |
(PR2) the on-site interaction Σ_x V_x n̂_{x↑} n̂_{x↓} is diagonal on the computational basis with eigenvalue Σ_x V_x n_{x↑}(c) n_{x↓}(c), and its pointwise action on a general state |
Fermion/JordanWigner/Hubbard/LiebAttractiveCoeffAction.lean |
|
hubbardOnSiteInteractionSiteReflectionCoeffWeight / …CoeffAction / spinReflectionCoeff_hubbardOnSiteInteractionSite / spinReflectionCoeff_attractiveHubbardInteraction |
(PR2) the induced entrywise (Hadamard) action of the on-site / attractive interaction on the SRP coefficient matrix: spinReflectionCoeff (Ĥ_int ψ) u h = (Σ_x V_x u_x (1−h_x)) · spinReflectionCoeff ψ u h |
Fermion/JordanWigner/Hubbard/LiebAttractiveCoeffAction.lean |
|
hubbardBlockIndex / hubbardBlockMergeConfig |
(PR3) the block (species-separated) order — all up orbitals 0…N, then all down N+1…2N+1 — and the block merge of an up/down configuration pair (needed because the interleaved spinfulIndex entangles same-species hopping signs with the opposite spin) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockOrder.lean |
|
hubbardBlock_betweenSum_up / …_down / hubbardBlock_upHop_jwSign_forward / …_backward / hubbardBlock_downHop_jwSign_forward / …_backward |
(PR3) Jordan–Wigner sign separation in block order: the combined hopping sign of an up-spin hop depends only on the up configuration (the occupation of the up sites strictly between the two endpoints), = (−1)^(Σ_{j<k<i} u_k), and the down-spin hop only on the down configuration (forward and backward variants; backward requires an empty target) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockOrder.lean |
|
exists_hubbardBlockIndex / hubbardSpinHopConfig / hubbardBlockMergeConfig_update_up / …_down |
(PR4) block-index surjectivity, the single-particle hop j → i on a configuration, and the fact that updating the block merge at an up (resp. down) orbital updates only the up (resp. down) configuration |
Fermion/JordanWigner/Hubbard/LiebAttractiveHopAction.lean |
|
hubbardBlock_upHop_forward_mulVec / …_backward / hubbardBlock_downHop_forward_mulVec / …_backward |
(PR4) a single same-species hop in block order acts on a single spin species: ĉ†_{block i σ} ĉ_{block j σ} \|merge u d⟩ = (PR3 sign) · \|merge (hop on σ's config) …⟩, hopping only the up (σ=0) or down (σ=1) configuration — the basis-level form of the kinetic left/right action |
Fermion/JordanWigner/Hubbard/LiebAttractiveHopAction.lean |
|
hubbardBlockFixedDownSubmodule / hubbardBlockFixedUpSubmodule / hubbardBlockKineticUp / hubbardBlockKineticDown |
(PR5) the span of block-merge basis states with a fixed down (resp. up) configuration, and the block-order single-species kinetic operators Σ_{i,j} T_{i,j} ĉ†_{i,σ} ĉ_{j,σ} |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockKinetic.lean |
|
hubbardBlock_upHop_mulVec_mem_fixedDown / …downHop…_mem_fixedUp / hubbardBlockKineticUp_mulVec_basisVec_mem_fixedDown / hubbardBlockKineticDown_mulVec_basisVec_mem_fixedUp |
(PR5) the species kinetic operators keep the opposite species’ configuration fixed: the up kinetic operator maps a block-merge basis state into the fixed-down fiber (dually for down) — the Ĥ↑ ⊗ 1 + 1 ⊗ Ĥ↓ species factorization at the fiber level |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockKinetic.lean |
|
hubbardBlockUpConfig / hubbardBlockDownConfig / hubbardBlockSpinConfigEquiv / hubbardBlockCoeffLinearEquiv / hubbardBlockCoeff |
(PR6) the block-order up/down factorization and the block (down-hole-gauged) coefficient matrix hubbardBlockCoeff ψ u h = ψ (merge u (1−h)) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockCoeff.lean |
|
hubbardBlockFixedDownSubmodule_apply_eq_zero_of_ne / hubbardBlockKineticUp_apply_eq_zero_of_down_ne / hubbardBlockKineticUpCoeffMatrix / hubbardBlockKineticUpCoeffAction / hubbardBlockCoeff_hubbardBlockKineticUp_mulVec |
(PR6) the up kinetic operator acts on the block coefficient matrix as a row-local (left) action: down-block off-diagonal entries vanish, so each column h is transformed by the fixed per-column matrix with no mixing between columns |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockCoeff.lean |
|
particleHoleConfigEquiv / hubbardBlockFixedUpSubmodule_apply_eq_zero_of_ne / hubbardBlockKineticDown_apply_eq_zero_of_up_ne / hubbardBlockKineticDownCoeffMatrix / hubbardBlockKineticDownCoeffAction / hubbardBlockCoeff_hubbardBlockKineticDown_mulVec |
(PR7) the down-spin dual: the down kinetic operator acts on the block coefficient matrix as a column-local action through the particle-hole-gauged column index (up-block off-diagonal entries vanish; each row is transformed by a fixed per-row matrix in the hole labels) | Fermion/JordanWigner/Hubbard/LiebAttractiveBlockCoeffDown.lean |
|
basisVec_hubbardBlockMerge_same_down_eq / jwSign_blockZero_congr_of_eq_below / hubbardBlock_upHop_apply_merge_indep_down / hubbardBlockKineticUp_apply_merge_indep_down / hubbardBlockKineticUpCoeffMatrix_indep_down |
(PR8) gauge independence of the up-kinetic coefficient matrix: in block order all up orbitals lie below all down orbitals, so the up-hop JW string sees only the up configuration; hence the up-kinetic matrix entry between configs with a common down part is independent of that down part, and the per-column matrix is independent of the hole label (left multiplication by a single fixed Fock kinetic matrix) | Fermion/JordanWigner/Hubbard/LiebAttractiveFockUp.lean |
|
basisVec_hubbardBlockMerge_same_up_eq / hubbardBlock_downHop_apply_merge_indep_up / hubbardBlockKineticDown_apply_merge_indep_up / hubbardBlockKineticDownCoeffMatrix_indep_up |
(PR9) the down-spin dual: gauge independence of the down-kinetic coefficient matrix (per-row matrix independent of the up label). Since an individual down-position JW sign depends on the total up occupation, only the combined hop sign is up-independent, so this reuses the PR4 single-hop lemmas via a lt_trichotomy case split (with the i=j number-operator case handled separately) |
Fermion/JordanWigner/Hubbard/LiebAttractiveFockDown.lean |
|
hubbardBlockKineticUpFixedMatrix / hubbardBlockKineticDownFixedRightMatrix / hubbardBlockKinetic / hubbardBlockKineticCoeffAction / hubbardBlockKineticUpCoeffAction_eq_mul_fixed / hubbardBlockKineticDownCoeffAction_eq_mul_fixedRight / hubbardBlockCoeff_hubbardBlockKinetic_mulVec |
(PR10) packaging the gauge-independent kinetic actions as honest matrix multiplications: the spin-symmetric block kinetic operator acts on the block coefficient matrix as C ↦ A·C + C·Bᵣ (left multiplication by the fixed up matrix, right multiplication by the fixed transposed down matrix) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBlockKineticMatrix.lean |
|
hubbardSpinfulSiteSpinEquiv / hubbardBlockSiteSpinEquiv / hubbardBlockToSpinfulOrbitalEquiv / hubbardBlockToSpinfulConfigEquiv / hubbardBlockToSpinfulConfigEquiv_apply_spinfulIndex / hubbardBlockToSpinfulConfigEquiv_hubbardBlockMergeConfig |
(PR11) the block ↔ interleaved orbital relabeling: the orbital permutation sending a block index i + σ(N+1) to the interleaved index 2i+σ, the induced configuration relabeling, and its compatibility with the merge maps (carries the block merge to the interleaved merge). The combinatorial first layer of connecting the kinetic factorization to the actual interleaved Hamiltonian |
Fermion/JordanWigner/Hubbard/LiebAttractiveInterleave.lean |
|
permutationOperator / permutationOperator_mulVec_basisVec / permutationOperator_conjTranspose_mul / permutationOperator_mul_conjTranspose / hubbardBlockToSpinfulPermutationOperator (+ basis action, unitarity) |
(PR12) the signed permutation operator \|σ⟩ ↦ ε(π,σ)\|σ∘π⁻¹⟩ for an arbitrary orbital permutation (generalizing the cyclic translationOperator of §11.4, reusing the already-general translationJwSign), proved unitary, and specialized to the block ↔ interleaved permutation; the second-quantized transport operator for connecting the two orderings |
Fermion/JordanWigner/Hubbard/LiebAttractivePermutation.lean |
|
permutationOperator_conjTranspose_mulVec_basisVec / permutationHopConjSign / permutationOperator_hopping_conj_mulVec_basisVec |
(PR13) the conjugated single-hop basis action: Uᴴ\|σ⟩ = ε(π,σ∘π)\|σ∘π⟩, and the basis action of U (ĉ†_p ĉ_q) Uᴴ (chaining the Uᴴ, bare-hop, and U basis actions) with the explicit composite Jordan–Wigner/permutation sign kept as a def. Reducing this to the operator equality U Ĥ_block Uᴴ = Ĥ_interleaved needs the JW sign cocycle identities (a later layer) |
Fermion/JordanWigner/Hubbard/LiebAttractiveConjHop.lean |
|
update_comp_perm / translationJwSign_mul_update_zero_comp_eq_jwSign_mul / translationJwSign_mul_update_one_comp_eq_jwSign_mul |
(PR14) the JW sign cocycle, one-mode-update parity law: updating a permuted configuration commutes with π (update (σ∘π) a v = (update σ (π a) v) ∘ π), and the product of translationJwSign π before and after toggling one mode q of σ∘π equals the bare Jordan–Wigner string signs jwSign q (σ∘π) · jwSign (π q) σ (remove-occupied and add-empty forms). Proved via the A/B/C partition of occupied modes by (k<q?)×(πk<πq?): zeroing q drops exactly the inversions through q (#B+#C), while E_q=#A+#B and E_{πq}=#A+#C, so both exponents agree mod 2 |
Fermion/JordanWigner/Hubbard/LiebAttractiveJwCocycle.lean |
|
permutationHopConjSign_eq / permutationOperator_hop_conj_mulVec_basisVec / permutationOperator_hop_conj_eq |
(PR15) the conjugated single-hop operator equality U (ĉ†_p ĉ_q) Uᴴ = ĉ†_{π p} ĉ_{π q}. The cocycle (permutationHopConjSign_eq) collapses the PR13 composite sign to the single permuted bare hop sign jwSign (π q) σ · jwSign (π p) (update σ (π q) 0) (multiply the PR14 zero/one parity laws and use jwSign²=1); the PR13 target state update²(σ∘π)∘π.symm relabels to update² σ at the permuted orbitals (update_comp_perm twice), so the conjugated hop and the bare hop ĉ†_{π p} ĉ_{π q} agree on every basis column, giving the operator identity |
Fermion/JordanWigner/Hubbard/LiebAttractiveCocycleOperator.lean |
|
hubbardBlockKineticSpecies_conj_eq / hubbardBlockKinetic_conj_eq |
(PR16) the block ↔ interleaved kinetic operator equality U · hubbardBlockKinetic · Uᴴ = hubbardKinetic (with U = permutationOperator (hubbardBlockToSpinfulOrbitalEquiv N)). Summing the PR15 single-hop identity over (i,j) (distributing the conjugation over the kinetic sum via mul_sum/sum_mul/mul_smul/smul_mul) sends each block hop ĉ†_{block i s} ĉ_{block j s} to the interleaved hop ĉ†_{spinful i s} ĉ_{spinful j s}; combining the two spin species (Fin.sum_univ_two) gives the full kinetic operator equality — the operator-level statement that the block and interleaved orderings are unitarily equivalent |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticConj.lean |
|
permutationOperator_mulVec_apply / spinReflectionCoeff_hubbardBlockToSpinfulPermutationOperator_mulVec |
(PR17) the SRP ↔ block coefficient bridge: the value of the signed permutation operator on an arbitrary vector (U ψ) τ = ε(π, τ∘π) · ψ (τ∘π), and the entrywise bridge spinReflectionCoeff (U ψ) u h = ε(π, block-merge u h) · hubbardBlockCoeff ψ u h (with ε = translationJwSign (hubbardBlockToSpinfulOrbitalEquiv N)). Since spinReflectionCoeff (the SRP/PSD matrix) and hubbardBlockCoeff (on which the kinetic acts as A·C+C·Bᵣ) share the particle-hole hole gauge and differ only by interleaved↔block merge, the bridge is a per-configuration JW sign — not a row/column gauge — so the RP energy form is carried on the raw hubbardBlockCoeff |
Fermion/JordanWigner/Hubbard/LiebAttractiveCoeffBridge.lean |
|
hubbardBlock_kineticDown_entry_eq_kineticUp_entry / hubbardBlockKineticDownFixedRightMatrix_eq_up |
(PR18) the down/up kinetic adjoint relation Bᵣ = P·Aᵀ·P (fixed before the RP energy trace so the correct adjoint enters). The kinetic matrix entry between two block-merge configurations is independent of the spectator species and symmetric under the up↔down species swap: hubbardBlockKineticDown N T (merge w a) (merge w b) = hubbardBlockKineticUp N T (merge a v) (merge b v) for all spectators w, v, because the Jordan–Wigner between-occupation sign only sees the active species (PR3 hubbardBlock_betweenSum_up/_down), the firing condition only depends on the active column configuration, and the diagonal i = j term is the same number-operator value n̂_i. Specializing gives hubbardBlockKineticDownFixedRightMatrix N T h h' = hubbardBlockKineticUpFixedMatrix N T (P h') (P h) with P = particleHoleConfig (no symmetry hypothesis on T) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBrRelation.lean |
|
trace_conjTranspose_mul_eq_sum / hubbardBlockKinetic_dotProduct_eq_trace |
(PR19) the first step of the RP energy assembly: the block-order kinetic energy as a coefficient-matrix trace. Reindexing the energy dot-product sum over configurations by the bijection (u,h) ↦ merge u (P h) (hubbardBlockSpinConfigEquiv + particleHoleConfigEquiv) and inserting the PR10 coefficient action gives dotProduct (star ψ) ((hubbardBlockKinetic N T).mulVec ψ) = trace (Cᴴ · (A·C + C·Bᵣ)) with C = hubbardBlockCoeff ψ (where trace_conjTranspose_mul_eq_sum is the entrywise expansion tr(Cᴴ·M) = ∑_{u,h} conj(C u h)·M u h). Holds for every ψ (no half-filling restriction — that enters later at the Perron–Frobenius/polar step); the bridge from the operator energy to the SRP Gram form 0 ≤ Re tr(C·A·C·Aᴴ) (PR1) |
Fermion/JordanWigner/Hubbard/LiebAttractiveEnergyTrace.lean |
|
particleHoleConfigPermMatrix / particleHoleConfigEquiv_symm / hubbardBlockKineticDownFixedRightMatrix_eq_permConj |
(PR20) the PR18 adjoint relation repackaged as a matrix identity Bᵣ = Pmat·Aᵀ·Pmat, where Pmat = particleHoleConfigPermMatrix is the permutation matrix ((particleHoleConfigEquiv N).toPEquiv.toMatrix) of the particle–hole involution (which is its own inverse, particleHoleConfigEquiv_symm). Proved from the entrywise PR18 form via toMatrix_toPEquiv_mul/mul_toMatrix_toPEquiv; having the relation as matrix algebra keeps the subsequent reflection-positive trace manipulations free of entrywise rewriting |
Fermion/JordanWigner/Hubbard/LiebAttractivePermConj.lean |
|
hubbardBlockKineticUp_isHermitian / hubbardBlockKineticUpFixedMatrix_isHermitian |
(PR21) the Hermitian half of the SRP Gram input: for a Hermitian hopping matrix T (star (T i j) = T j i, in particular any real symmetric T) the block up-kinetic operator hubbardBlockKineticUp is Hermitian (same argument as fermionHopping_isHermitian, with block indices), hence its gauge-fixed left-multiplier matrix A is Hermitian (Aᴴ = A) — its entries are matrix elements of the Hermitian operator between block-merge configurations. Combined with the entrywise reality (Aᵀ = A, a later layer) this gives Aᴴ = Aᵀ and Bᵣ = P·Aᴴ·P, consumed by spinReflection_gramMatrix_nonneg |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticHermitian.lean |
|
jwSign_star / fermionHoppingTerm_entry_real / hubbardBlockKineticUpFixedMatrix_conjTranspose_eq_transpose / hubbardBlockKineticDownFixedRightMatrix_eq_permConj_conjTranspose |
(PR22) the reality half upgrading PR20 to the adjoint form Bᵣ = Pmat·Aᴴ·Pmat. The Gram bound 0 ≤ Re tr(C·A·C·Aᴴ) consumes the adjoint Aᴴ, while PR20 gives the transpose Aᵀ; these differ for a Hermitian operator (σ_y), so the bridge needs the entrywise reality of A. For a real hopping matrix T (star (T i j) = T i j), A’s entries are sums of T_{ij} times hopping matrix elements (products of Jordan–Wigner signs ±1, real via jwSign_star/fermionHoppingTerm_entry_real), so Aᴴ = Aᵀ, hence Bᵣ = Pmat·Aᴴ·Pmat |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticReal.lean |
|
dotProduct_conj_mul_conjTranspose / hubbardKinetic_dotProduct_eq_block_trace_of_interleaved |
(PR23) the interleaved kinetic energy as a block-coefficient trace. The attractive Hamiltonian uses the interleaved hubbardKinetic, while PR19’s trace is for the block hubbardBlockKinetic; PR16 (U·hubbardBlockKinetic·Uᴴ = hubbardKinetic) plus the elementary quadratic-form conjugation identity dotProduct_conj_mul_conjTranspose ((star v)·((U·M·Uᴴ)·v) = (star (Uᴴ·v))·(M·(Uᴴ·v)), pure matrix algebra, no unitarity) give ⟨ψ\|Ĥkin\|ψ⟩ = tr(C'ᴴ·(A·C' + C'·Bᵣ)) with C' = hubbardBlockCoeff (Uᴴ·ψ), U = permutationOperator (hubbardBlockToSpinfulOrbitalEquiv N). The kinetic half of the full energy functional; the interaction (Hadamard-diagonal on spinReflectionCoeff, which carries the PSD/PF structure) is reconciled through the PR17 sign bridge in a later layer |
Fermion/JordanWigner/Hubbard/LiebAttractiveInterleavedEnergy.lean |
|
particleHoleConfig_val_eq_one_sub / dotProduct_eq_sum_spinReflectionCoeff / attractiveHubbardInteraction_dotProduct_eq_spinReflectionCoeff_normSq |
(PR24) the attractive interaction energy as a diagonal normSq sum. Lifting the PR2 Hadamard-diagonal action to the energy quadratic form (reindexing the inner product over the interleaved up/down factorization hubbardSpinConfigEquiv + particle–hole, mirror of PR19): ⟨ψ\|Ĥint\|ψ⟩ = Σ_{u,h} (Σ_x −U_x·u_x·(1−h_x))·\|C_{u,h}\|² with C = spinReflectionCoeff ψ. For attractive U_x>0 the weight Σ_x −U_x·u_x·(1−h_x) ≤ 0 is non-positive (the sign that lowers the energy under the spin-reflection variational replacement); the PSD/PF structure lives on spinReflectionCoeff, so the interaction energy is naturally expressed there |
Fermion/JordanWigner/Hubbard/LiebAttractiveInteractionEnergy.lean |
|
translationJwSign_normSq / normSq_translationJwSign_mul / spinReflectionCoeff_normSq_eq_hubbardBlockCoeff |
(PR25) the two coefficient matrices have equal entry magnitudes. The energy lives in two coordinate systems — kinetic trace on hubbardBlockCoeff (Uᴴψ) (PR23), interaction + PSD on spinReflectionCoeff ψ (PR24/PR1) — related entrywise by the PR17 Jordan–Wigner sign ε (spinReflectionCoeff (Uψ) = ε ⊙ hubbardBlockCoeff ψ). Since ε = ±1 is a root of unity (normSq ε = 1, from translationJwSign_sq/translationJwSign_star), \|spinReflectionCoeff ψ (u,h)\|² = \|hubbardBlockCoeff (Uᴴψ) (u,h)\|² (PR17 at φ=Uᴴψ, U·Uᴴ=1). This lets the variational replacement C ↦ \|C\| (run on the PSD spinReflectionCoeff) control the interaction energy without transporting positive-semidefiniteness through the non-gauge sign ε |
Fermion/JordanWigner/Hubbard/LiebAttractiveCoeffNormSq.lean |
|
attractiveHubbardHamiltonian_dotProduct_eq_block |
(PR26) the full attractive-Hubbard energy functional on the block coefficient matrix: assembling the kinetic trace (PR23) and the attractive interaction’s diagonal normSq sum (PR24), bridged by the equal-magnitude relation (PR25), ⟨ψ\|Ĥ\|ψ⟩ = tr(C'ᴴ·(A·C' + C'·Bᵣ)) + Σ_{u,h} (Σ_x −U_x·u_x·(1−h_x))·\|C'_{u,h}\|² with C' = hubbardBlockCoeff (Uᴴψ). The energy functional whose spin-reflection variational minimization (matrix polar replacement C ↦ \|C\| = (CᴴC)^{1/2}, the Lieb trace inequality, Perron–Frobenius uniqueness, spin-flip singlet) is the remaining endgame |
Fermion/JordanWigner/Hubbard/LiebAttractiveFullEnergy.lean |
|
hubbardUpOccupationDiag / hubbardHoleOccupationDiag / trace_conjTranspose_mul_diagonal_mul_diagonal_eq_sum_normSq / attractiveInteraction_normSq_sum_eq_trace_form |
(PR27) the attractive interaction’s diagonal normSq sum as a diagonal-sandwich trace form −Σ_x U_x · tr(Cᴴ·D_x·C·E_x), with D_x = diag(u ↦ u_x) the up-occupation diagonal and E_x = diag(h ↦ 1−h_x) the hole-occupation diagonal (both positive-semidefinite, entries 0/1). The generic helper trace_conjTranspose_mul_diagonal_mul_diagonal_eq_sum_normSq expands tr(Cᴴ·diag d·C·diag e) = Σ_{i,j} d_i e_j \|C_{i,j}\|². This is the form on which the spin-reflection variational replacement C ↦ \|C\| acts via the Lieb trace inequality tr(Cᴴ D C E) ≤ tr(\|C\| D \|C\| E) (next layer): with −U_x ≤ 0, replacing C by \|C\| does not raise the interaction energy |
Fermion/JordanWigner/Hubbard/LiebAttractiveInteractionTrace.lean |
|
spinReflectionCoeff_injective / spinReflectionCoeff_isHermitian_iff_thetaFixed |
(PR28; first layer of the corrected spin-reflection endgame — the earlier polar-replacement route was unsound) Lieb’s SRP argument (Tasaki §10.2.4) works with the coefficient matrix in Hermitian form W (the \|Γ(W)⟩ representation). The Hermitian condition is exactly θ-symmetry of the state: since PR1 gives spinReflectionCoeff (θψ) = (spinReflectionCoeff ψ)ᴴ and the coefficient map is injective, spinReflectionCoeff ψ is Hermitian iff θψ = ψ (θ = spin-flip ∘ particle-hole) |
Fermion/JordanWigner/Hubbard/LiebAttractiveHermitianCoeff.lean |
|
lieb_srp_rearrangement |
(PR29; corrected endgame) the elementary eigenvalue rearrangement at the heart of Lieb’s SRP inequality E(W) ≥ E(\|W\|) (Tasaki eq. (10.2.41)→(10.2.43)). For real eigenvalues λ_j and nonnegative weights a_{j,k} ≥ 0, Σ_{j,k} λ_j λ_k a_{j,k} ≤ Σ_{j,k} \|λ_j\|\|λ_k\| a_{j,k} (termwise, λ_jλ_k ≤ \|λ_j\|\|λ_k\|). Writing Hermitian W = Σ_j λ_j v_jv_j†, \|W\| = Σ_j\|λ_j\|v_jv_j†: the kinetic Σ_j λ_j²(v_j†Tv_j) is invariant (λ_j²=\|λ_j\|²) and the attractive interaction −Σ U_x Σ_{j,k} λ_jλ_k\|v_j†I^(x)v_k\|² does not increase under λ_j↦\|λ_j\| |
Fermion/JordanWigner/Hubbard/LiebAttractiveSRPRearrangement.lean |
|
hermitianAbs / hermitianAbs_posSemidef / hermitianAbs_isHermitian / hermitianAbs_mul_self |
(PR30; corrected endgame) the spectral absolute value \|W\| = U·\|D\|·Uᴴ of a Hermitian matrix W = U·D·Uᴴ (U = eigenvectorUnitary, D = diagonal eigenvalues), via the mathlib spectral theorem. Established structural facts: \|W\| is positive-semidefinite (PosSemidef.diagonal + unitary conjugation), hence Hermitian, and squares to W² (\|W\|² = W², the kinetic invariance Tr(W²T) = Tr(\|W\|²T) under W ↦ \|W\|) |
Fermion/JordanWigner/Hubbard/LiebAttractiveHermitianAbs.lean |
|
trace_conj_diag_interaction_re_eq_spectral_sum / trace_hermitian_interaction_re_le_abs |
(PR31; corrected endgame) the abstract SRP interaction inequality Re tr(W·I·W·I) ≤ Re tr(\|W\|·I·\|W\|·I) (Hermitian W,I). Diagonalizing W = U·D·Uᴴ (spectral theorem) and setting M = Uᴴ·I·U, the trace expands to the spectral double sum Re tr(W·I·W·I) = Σ_{j,k} λ_j λ_k \|M_{j,k}\|² (via trace_mul_comm cyclic + the PR27 diagonal-sandwich expansion); \|W\| gives the same with \|λ\|, and the elementary rearrangement lieb_srp_rearrangement (PR29) closes the inequality |
Fermion/JordanWigner/Hubbard/LiebAttractiveInteractionIneq.lean |
|
liebSRPEnergy / liebSRPEnergy_abs_le |
(PR32; corrected endgame) the abstract SRP energy monotonicity E(\|W\|) ≤ E(W) (i.e. E(W) ≥ E(\|W\|), Tasaki eq. (10.2.43)). The Lieb energy functional E(W) = 2·Re tr(W²·T) − 2·Σ_x U_x·Re tr(W·I_x·W·I_x) (U_x ≥ 0): the kinetic term is unchanged under W ↦ \|W\| (\|W\|² = W², PR30), and the attractive interaction does not increase (each Re tr(W·I_x·W·I_x) ≤ Re tr(\|W\|·I_x·\|W\|·I_x), PR31; the −U_x ≤ 0 sign flips it). The heart of spin-space reflection positivity |
Fermion/JordanWigner/Hubbard/LiebAttractiveEnergyMonotone.lean |
|
trace_conj_kinetic_eq_two_trace_W_sq |
(PR33a; corrected endgame, the Hubbard reconciliation crux) the kinetic reconciliation identity. The half-filled energy is expressed as the abstract liebSRPEnergy on the block coefficient C with a particle-hole column reindex W := C·P (P = the particle-hole permutation matrix, a Hermitian involution) — NOT the raw spinReflectionCoeff (whose ε-bridge to the block coeff is non-gauge). Since Bᵣ = P·Aᴴ·P (PR22), for Hermitian W the block kinetic quadratic form is clean: tr(Cᴴ·(A·C + C·(P·Aᴴ·P))) = 2·tr(W²·A) (cyclic trace + P²=1). Identifies T_S = A for the energy reconciliation |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticW.lean |
|
trace_conj_interaction_eq_trace_W |
(PR33b; corrected endgame) the interaction reconciliation identity, companion to PR33a. The attractive interaction is the diagonal sandwich −Σ_x U_x·tr(Cᴴ·D_x·C·E_x) (PR27); under the same reindex W := C·P the hole diagonal is the particle-hole conjugate E_x = P·D_x·P, so for Hermitian W the trace collapses cleanly: tr(Cᴴ·D·C·(P·D·P)) = tr(W·D·W·D) (cyclic trace + P²=1). Identifies I_S = D_x for the energy reconciliation; with PR33a the half-filled energy is 2·tr(W²·A) − Σ_x U_x·tr(W·D_x·W·D_x) = liebSRPEnergy A D (U/2) W |
Fermion/JordanWigner/Hubbard/LiebAttractiveInteractionW.lean |
|
particleHoleConfigPermMatrix_mul_self / particleHoleConfigPermMatrix_isHermitian / particleHoleConfigPermMatrix_conj_diagonal / hubbardHoleOccupationDiag_eq_permConj |
(PR33c; corrected endgame) the particle-hole conjugation facts for the reconciliation W := C·P. P = particleHoleConfigPermMatrix is a Hermitian involution (P·P = 1, Pᴴ = P); conjugating a diagonal by P reindexes it by the involution φ (P·diagonal d·P = diagonal (d∘φ)); hence the hole-occupation diagonal is the particle-hole conjugate of the up-occupation diagonal, E_x = P·D_x·P (the I_x = P·D_x·P input that turns PR27’s interaction trace tr(Cᴴ·D_x·C·E_x) into PR33b’s tr(W·D_x·W·D_x)). hubbardUpOccupationDiag_isHermitian records D_x Hermitian |
Fermion/JordanWigner/Hubbard/LiebAttractivePHConjDiag.lean |
|
attractiveHubbardHamiltonian_energy_eq_liebSRP_trace_of_blockW_isHermitian / attractiveHubbardHamiltonian_energy_re_eq_liebSRPEnergy_of_blockW_isHermitian |
(PR33d; corrected endgame — the assembly) the full energy reconciliation. Combining PR26 (energy decomposition), PR33a (kinetic), PR27 (interaction trace form), PR33c (E_x = P·D_x·P), PR33b (interaction): for symmetric hopping T and a state ψ whose block coefficient gives a Hermitian W := C·P, the half-filled energy is ⟨ψ\|Ĥ\|ψ⟩ = 2·tr(W²·A) − Σ_x U_x·tr(W·D_x·W·D_x) (ℂ form), hence Re⟨ψ\|Ĥ\|ψ⟩ = liebSRPEnergy A D (U/2) W — the consumer feeding liebSRPEnergy_abs_le. The (C·P).IsHermitian hypothesis is not automatic (Lieb parametrizes trial states by Hermitian W); a later layer identifies the ground energy with a Hermitian-W state |
Fermion/JordanWigner/Hubbard/LiebAttractiveEnergyReconcile.lean |
|
hubbardBlockCoeff_mul_permMatrix / gammaWState / blockWCoeff_gammaWState |
(PR34; Γ-family layer 1) the Γ-coordinate picture of the reconciliation’s W. The gauge-cancellation hubbardBlockCoeff ψ · P = hubbardBlockCoeffLinearEquiv ψ shows the particle-hole column reindex P exactly undoes the gauge in hubbardBlockCoeff, so W = hubbardBlockCoeffLinearEquiv (Uᴴψ) is a composition of linear isomorphisms — hence surjective with explicit inverse gammaWState W := U·(LE⁻¹ W) satisfying hubbardBlockCoeff (Uᴴ Γ(W))·P = W. This is the coordinate backbone for parametrizing trial states by a Hermitian W |
Fermion/JordanWigner/Hubbard/LiebAttractiveGammaCoords.lean |
|
blockWCoeff / blockWCoeff_injective / gammaThetaVec / blockWCoeff_gammaThetaVec / blockWCoeff_isHermitian_iff_gammaThetaFixed |
(PR35; Γ-family layer 2) the Γ-reflection Θ ψ := Γ((blockWCoeff ψ)ᴴ) (conjugate-transposes the coefficient W ↦ Wᴴ in Γ coordinates) and the criterion (blockWCoeff ψ).IsHermitian ↔ Θ ψ = ψ. blockWCoeff (= hubbardBlockCoeff (Uᴴψ)·P) is injective (PR34 gauge cancellation + unitary Uᴴ); blockWCoeff (Θ ψ) = (blockWCoeff ψ)ᴴ (via Γ-surjectivity), so the criterion follows by injectivity. This is the ε-bridge-free analogue of spinReflectionCoeff_isHermitian_iff_thetaFixed for the matrix W the reconciliation uses |
Fermion/JordanWigner/Hubbard/LiebAttractiveGammaReflection.lean |
|
blockWCoeff_hubbardKinetic_mulVec |
(PR36a; Γ-family — kinetic intertwiner) how the kinetic Hamiltonian acts in the W-coordinate: blockWCoeff (hubbardKinetic T ψ) = A·W + W·Aᴴ (W = blockWCoeff ψ, A = hubbardBlockKineticUpFixedMatrix T), for entrywise-real T. Via Uᴴ·Ĥ_kin·U = hubbardBlockKinetic + block coefficient action C ↦ A·C + C·Bᵣ (Bᵣ = P·Aᴴ·P), the ·P reindex collapses the gauge. Manifestly equivariant under W ↦ Wᴴ — the kinetic half of the Ĥ–Θ commutation |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticIntertwiner.lean |
|
blockWCoeff_attractiveHubbardInteraction_mulVec |
(PR36b; Γ-family — interaction intertwiner) how the attractive interaction acts in the W-coordinate: blockWCoeff (Ĥ_int ψ) = Σ_x (−U_x)·D_x·W·D_x (D_x = hubbardUpOccupationDiag x). The interaction is diagonal, so its action transports through the Jordan-Wigner ε-bridge (ε²=1 cancels — no Hermiticity obstruction); written as a diagonal sandwich Σ_x V_x·D_x·C·E_x and collapsing ·P (E_x·P = P·D_x). Manifestly equivariant under W ↦ Wᴴ — the interaction half of the Ĥ–Θ commutation |
Fermion/JordanWigner/Hubbard/LiebAttractiveInteractionIntertwiner.lean |
|
blockWCoeff_add / blockWCoeff_attractiveHubbardHamiltonian_mulVec / attractiveHubbardHamiltonian_gammaThetaVec_commute |
(PR36c; Γ-family — commutation) assembles the kinetic (PR36a) and interaction (PR36b) intertwiners into the full W-coordinate action blockWCoeff (Ĥψ) = G(W) := A·W + W·Aᴴ + Σ_x (−U_x)·D_x·W·D_x. G is equivariant under conjugate transpose (G(Wᴴ) = (G W)ᴴ; needs D_x Hermitian + U real), and Θ acts as W ↦ Wᴴ in the injective W-coordinate, so Ĥ (Θ ψ) = Θ (Ĥ ψ) — Θ commutes with Ĥ and preserves every eigenspace (key input for PR37) |
Fermion/JordanWigner/Hubbard/LiebAttractiveHamiltonianCommute.lean |
|
gammaThetaVec_smul / gammaThetaVec_gammaThetaVec / gammaThetaVec_preserves_eigenvector |
(PR36d; Γ-family — anti-linearity) the Γ-reflection Θ is anti-linear (Θ(c•ψ) = (conj c)•Θψ, since it conjugate-transposes W) and an involution (Θ²=id). With the commutation (PR36c), anti-linearity gives eigenvector preservation at real eigenvalues: Ĥψ = E·ψ (E∈ℝ) ⟹ Ĥ(Θψ) = E·(Θψ). Since ground energies are real, Θ maps ground vectors to ground vectors — the input for the Hermitian-W ground representative (PR37). Helpers blockWCoeff_smul/gammaWState_smul/hubbardBlockCoeff_smul |
Fermion/JordanWigner/Hubbard/LiebAttractiveGammaAntilinear.lean |
|
gammaThetaSymm_fixed / gammaThetaSymm_eigenvector / exists_hermitianW_ground |
(PR37; Γ-family — Hermitian-W ground representative) the ground energy is attained by a Θ-fixed (Hermitian-W) state: given any nonzero ground vector ψ₀, the symmetrization ψ₀ + Θψ₀ is Θ-fixed and again a ground vector; if it vanishes (Θψ₀ = −ψ₀), the rotated i·ψ₀ + Θ(i·ψ₀) = 2i·ψ₀ is nonzero and Θ-fixed (Θ anti-linear). Hence exists_hermitianW_ground: a nonzero Ĥ-eigenvector at the same real eigenvalue with Hermitian blockWCoeff — the input to which the energy reconciliation + SRP monotonicity apply (PR38). Helpers gammaWState_add/gammaThetaVec_add |
Fermion/JordanWigner/Hubbard/LiebAttractiveHermitianGround.lean |
|
blockWCoeff_dotProduct_eq / gammaWState_dotProduct_eq / hermitianAbs_sum_normSq_eq |
(PR38a; norm/isometry foundation for the PSD ground representative) the coordinate map ψ ↦ blockWCoeff ψ is an isometry: ⟨ψ,ψ⟩ = Σ_{u,h} \|W_{u,h}\|² (config reshape ∘ unitary Uᴴ), and ⟨Γ(W),Γ(W)⟩ = Σ_{u,h} \|W_{u,h}\|². The spectral absolute value preserves the Frobenius norm: Σ_{u,h} \|\|W\|_{u,h}\|² = Σ_{u,h} \|W_{u,h}\|² (via \|W\|²=W², tr(\|W\|ᴴ\|W\|)=tr(W²)=tr(WᴴW)). Helper dotProduct_star_self_eq_sum_normSq. These match the norms so SRP monotonicity transfers to states (PR38c) |
Fermion/JordanWigner/Hubbard/LiebAttractiveNormFoundation.lean |
|
attractiveHubbardInteraction_isHermitian / attractiveHubbardHamiltonian_isHermitian |
(PR38b) Ĥ = attractiveHubbardHamiltonian is Hermitian for symmetric real hopping T: the kinetic part via hubbardKinetic_isHermitian, the attractive interaction −Σ_x U_x n̂↑n̂↓ as a real combination of Hermitian double-occupancy operators. Required by the variational/PF arguments in the PSD ground-representative step |
Fermion/JordanWigner/Hubbard/LiebAttractiveHamiltonianHermitian.lean |
|
exists_posSemidefW_ground |
(PR38c; the SRP variational step) the ground energy is attained by a state whose reconciliation coefficient W = blockWCoeff is positive semidefinite. From a unit minimum-eigenvector (eigenvalue μ), the Hermitian-W representative φ (PR37) gives W Hermitian with Ĥφ = μφ; the state φ' := Γ(\|W\|) satisfies the squeeze μ‖φ'‖² ≤ ⟨φ'\|Ĥ\|φ'⟩ = E(\|W\|) ≤ E(W) = ⟨φ\|Ĥ\|φ⟩ = μ‖φ‖² = μ‖φ'‖² (reconciliation PR33d + liebSRPEnergy_abs_le + isometry PR38a), so all are equalities and mulVec_eq_smul_of_rayleighOnVec_eq_min makes φ' a ground vector; ‖φ'‖=‖φ‖>0 and blockWCoeff φ' = \|W\| PSD. For symmetric T, U≥0 |
Fermion/JordanWigner/Hubbard/LiebAttractivePosSemidefGround.lean |
|
posSemidef_ground_kernel_propagation |
(PR39a; analytic heart of Tasaki Lemma 10.10) a PSD R solving the ground-state Lyapunov equation A·R + R·Aᴴ − Σ_x U_x·(I_x·R·I_x) = E·R (U_x>0, A/I_x Hermitian) has a kernel invariant under each I_x and under A: R v = 0 ⟹ (∀ x, R(I_x v) = 0) ∧ R(A v) = 0. Purely a PSD argument — sandwiching by v kills the kinetic part, leaving Σ_x U_x⟨I_x v, R I_x v⟩ = 0; each summand nonneg + U_x>0 ⟹ each R(I_x v)=0 (Lemma A.11), then the vector equation gives R(Aᴴv)=0. The key invariance feeding the connectivity propagation |
Math/PosSemidef/GroundKernelPropagation.lean |
|
basis_mem_ker_of_separating_projections |
(PR39b; Lemma 10.10 basis extraction) if ker R is invariant under each of a family of 0/1-diagonal projections diagonal (d x) whose diagonals separate points, then ker R is spanned by standard basis vectors: R v = 0, v a ≠ 0 ⟹ R(δ_a) = 0. Proof avoids matrix products — a Finset induction peels one projection (or its complement) at a time on the partial-projection vector fun s => if (∀ x∈T, d x s = d x a) then v s else 0, collapsing at T=univ (by separation) to v a • δ_a. The “kernel is a coordinate subspace” input for the connectivity dichotomy |
Math/PosSemidef/SeparatingProjectionKernel.lean |
|
posDef_or_eq_zero_of_connected_support |
(PR39c; abstract Lemma 10.10) the connected-support dichotomy: a PSD R with kernel invariant under A and a coordinate subspace, where a connected graph G has every edge b~a witnessing A b a ≠ 0, is positive definite or zero. A single δ_a ∈ ker R propagates along every walk (R δ_a=0 ⟹ R(A δ_a)=0, basis extraction puts neighbours in the kernel); connectivity forces all-or-nothing. Combined with PR39a (kernel invariance) + PR39b (coordinate subspace), this is the abstract Tasaki Lemma 10.10 |
Math/PosSemidef/ConnectedSupportDichotomy.lean |
|
blockWCoeff_lyapunov_of_eigenvector |
(PR39d) the W-space Lyapunov (Schrödinger) equation: a Ĥ-eigenvector ψ at eigenvalue E gives, via the intertwiner (PR36c) + blockWCoeff_smul, A·R + R·Aᴴ − Σ_x U_x·(D_x·R·D_x) = E·R for R = blockWCoeff ψ (A = hubbardBlockKineticUpFixedMatrix T, D_x = hubbardUpOccupationDiag x). This is exactly the hypothesis form feeding the abstract Lemma 10.10 (posSemidef_ground_kernel_propagation / posDef_or_eq_zero_of_connected_support) |
Fermion/JordanWigner/Hubbard/LiebAttractiveGroundLyapunov.lean |
|
permutationOperator_conjTranspose_mulVec_apply / hubbardBlockIndexEquiv / hubbardBlockMergeConfig_count / blockWCoeff_apply_eq_zero_of_count_ne |
(PR40a; sector support) for a state ψ in the Ne-electron sector (N̂ ψ = Ne·ψ), blockWCoeff ψ is supported on the anti-diagonal band \|u\|+\|h\| = Ne: blockWCoeff ψ u h = (Uᴴψ)(blockMerge u h), count(blockMerge u h) = \|u\|+\|h\|, and the orbital relabel Uᴴ preserves the count, so the entry vanishes off the band (via mulVec_apply_eq_zero_of_number_ne). The genuine invariant square block is the balanced sector \|u\|=\|h\|=Ne/2 (Even Ne), handled next |
Fermion/JordanWigner/Hubbard/LiebAttractiveSectorSupport.lean |
|
hubbardSpinHopConfig_inj_of_hop |
(PR40b; single-hop uniqueness) for the config-graph connectivity of A = hubbardBlockKineticUpFixedMatrix: from a fixed u (u j=1, u i=0), the single hop q→p reaches hop u j i only for (p,q)=(i,j). This term-selection collapses the kinetic double sum Σ_{p,q} T_{p,q}ĉ†_pĉ_q to the surviving (i,j) entry (= ±T_{i,j} ≠ 0) in the connectivity step |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticHopEntry.lean |
|
hubbardBlockKineticUpFixedMatrix_apply_hop_ne |
(PR40c; kinetic single-hop entry nonzero) the up-kinetic matrix entry between a single-hop configuration and its source is nonzero: A (hop u j i) u ≠ 0 (= ±T_{i,j}) for u j=1, u i=0, i≠j, T_{i,j}≠0. Expanding the entry ((Ĥ↑)·|u⟩)(hop u j i) over the kinetic double sum Σ_{p,q} T_{p,q}ĉ†_pĉ_q (via opEntry_eq_mulVec + sum_mulVec), only the (p,q)=(i,j) term reaches the hopped config (PR40b uniqueness kills the rest), leaving ±T_{i,j} (hubbardBlock_upHop_forward/backward_mulVec). The edge-weight-nonzero input for the config-graph connectivity |
Fermion/JordanWigner/Hubbard/LiebAttractiveKineticEntry.lean |
|
hubbardKineticSectorGraph_preconnected |
(PR40d; fixed-count sector kinetic graph connectivity) on the fixed up-count sector {u // Σ_x u_x = k}, the kinetic support graph hubbardKineticSectorGraph (adjacency = both off-diagonal entries A p q, A q p nonzero) is preconnected whenever the hopping graph hoppingSupportGraph T is (real-symmetric T). Two equal-count configs share magnetization, hence are linked by configuration swaps along hopping edges (swapReachable_of_eq_magnetization); each swap is a sector-graph edge (PR40c forward entry + Hermitian reverse entry, sectorGraph_adj_of_hop). Supplies the connected-support hypothesis of the abstract Lemma 10.10 (posDef_or_eq_zero_of_connected_support) |
Fermion/JordanWigner/Hubbard/LiebAttractiveSectorConnectivity.lean |
|
exists_attractive_sector_ground |
(PR40e-pre1; Ne-sector ground vector) for symmetric real hopping T and any site attraction U, there is a nonzero vector φ in the Ne-electron sector (N̂ φ = Ne·φ) that is an eigenvector of attractiveHubbardHamiltonian N T U at the sector-compression minimum eigenvalue. Built from charge conservation (attractiveHubbardHamiltonian_commute_fermionTotalNumber ⟸ hubbardOnSiteInteractionSite_commute_fermionTotalNumber) giving preservesHubbardSectorW_attractive, then the generic eigenvector lift configSectorExpansion_of_compress_eigen. The fixed-Ne membership the Lieb SRP sector argument requires |
Fermion/JordanWigner/Hubbard/LiebAttractiveSectorGround.lean |
|
configSector_minEnergy_mul_le_rayleighOnVec_of_isHermitian / mulVec_eq_smul_of_configSector_rayleighOnVec_eq_min |
(PR40e-pre2a; generic sector variational tools) for any Hermitian A : ManyBodyOp and any fixed-sector vector v (supported on predicate P, generically replacing the Ne-electron sector): (lower bound) E_P · ‖v‖² ≤ rayleigh A v where E_P = min eigenvalue of the sector compression configSectorCompress; (converse) if rayleigh A v = E_P·‖v‖² then A v = E_P·v. Generalize the uniform-Hubbard sector variational to arbitrary A and sector predicate (only configSector_completeness + rayleighOnVec_configSectorCompress used). Instantiate at hubbardNumberSectorPred (number sector) or hubbardBalancedSectorPred (balanced Ŝ³=0 sector) as needed. The SRP squeeze infrastructure against the sector minimum |
Fermion/JordanWigner/Hubbard/LiebAttractiveSectorVariational.lean |
|
gammaThetaVec_preserves_fermionTotalNumber / exists_hermitianW_ground_in_sector |
(PR40e-pre2a2; Γ-reflection sector preservation) the Γ-reflection Θ = gammaWState ∘ conjTranspose ∘ blockWCoeff preserves the Ne-electron sector (N̂ ψ = Ne·ψ ⟹ N̂(Θψ) = Ne·Θψ): conjugate transpose preserves the blockWCoeff band support \|u\|+\|h\|=Ne (swaps (u,h)↦(h,u)), and a band-supported W gives a sector gammaWState (gammaWState_mem_numberSector_of_band_supported, via the converse mulVec_eq_smul_number_of_apply_eq_zero of PR40a’s band support). Hence the Hermitian-W ground representative exists_hermitianW_ground strengthens to stay in the Ne-sector (exists_hermitianW_ground_in_sector) |
Fermion/JordanWigner/Hubbard/LiebAttractiveThetaSector.lean |
|
hubbardBalancedSectorPred / hubbardBalancedConfig / mulVec_apply_eq_zero_of_upNumber_ne / mulVec_apply_eq_zero_of_downNumber_ne / exists_attractive_balanced_ground |
(PR40e-pre2b; balanced-sector ground vector) the per-spin balanced sector N̂_↑ = N̂_↓ = k (Ŝ³ = 0, electron number 2k) extends the number-sector ground to the balanced predicate P c := (Σ_i c_{i↑} = k) ∧ (Σ_i c_{i↓} = k) via the generic configSector* compression Core. For symmetric real hopping T and any site attraction U, there is a nonzero vector φ in the balanced sector (N̂_↑ φ = k·φ and N̂_↓ φ = k·φ) that is an eigenvector of attractiveHubbardHamiltonian N T U at the balanced sector-compression minimum eigenvalue. Built from per-spin commutation (attractiveHubbardHamiltonian_commute_fermionTotal{Up,Down}Number) giving sector preservation, then the generic eigenvector lift configSectorExpansion_of_compress_eigen. The balanced support restriction is crucial for the SRP Hermitian-W ground’s principal-block structure |
Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedSectorGround.lean |
|
mulVec_eq_smul_upNumber_of_apply_eq_zero / blockWCoeff_apply_eq_zero_of_updowncount_ne / gammaWState_mem_balancedSector_of_block_supported / gammaThetaVec_preserves_balanced / exists_hermitianW_ground_in_balanced_sector |
(PR40e-pre2b; Γ-reflection preserves balanced Ŝ³=0 sector) the Γ-reflection Θ = gammaWState ∘ conjTranspose ∘ blockWCoeff preserves the balanced per-spin sector (N̂_↑ ψ = k·ψ and N̂_↓ ψ = k·ψ ⟹ N̂_↑(Θψ) = k·Θψ and N̂_↓(Θψ) = k·Θψ): conjugate transpose swaps (u, h) ↦ (h, u) and hence preserves the balanced block \|u\| = \|h\| = k (it swaps N̂_↑ ↔ N̂_↓), and a balanced-block-supported W gives a balanced gammaWState (gammaWState_mem_balancedSector_of_block_supported). The balanced Hermitian-W ground representative exists_hermitianW_ground_in_balanced_sector (obtained by Θ-symmetrizing the balanced ground exists_attractive_balanced_ground) stays in the balanced sector; its blockWCoeff is supported on the principal S_k × S_k block that the SRP endgame consumes. This is the per-spin refinement of exists_hermitianW_ground_in_sector (PR40e-pre2a2; eq. (10.2.41)–(10.2.43), Lemma 10.9, pp. 363–367) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedThetaSector.lean (PR #4937) |
|
hubbardCountSectorEmbedding / hubbardCountSectorEmbedding_conjTranspose_mul_self / blockWCoeff_eq_embed_compress_of_balanced / liebSRPEnergy_conj_isometry / frobenius_conj_isometry / configSector_minEnergy_mul_le_rayleighOnVec_of_isHermitian / mulVec_eq_smul_of_configSector_rayleighOnVec_eq_min / exists_posSemidefW_ground_in_balanced_sector |
(PR40f; balanced PSD-W ground state, Tasaki §10.2.4 Lemma 10.9, p. 363–367) the terminal positive-semidefinite-W ground state in the balanced Ŝ³=0 sector. The Lieb spin-reflection-positivity squeeze is run against the compressed balanced block W_S = Jᴴ·W·J (J = hubbardCountSectorEmbedding, the fixed up-count sector embedding; Jᴴ J = 1), yielding the PSD state φ' := Γ(J·\|W_S\|·Jᴴ) that satisfies the squeeze E(φ') ≤ E(φ) = μ·‖φ‖² where φ is the Hermitian-W ground from PR40e-pre2b and μ is the balanced-sector minimum (by isometry invariance liebSRPEnergy_conj_isometry, PSD conjugation Matrix.PosSemidef.mul_mul_conjTranspose_same, the monotonicity liebSRPEnergy_abs_le, and the balanced variational lower bound configSector_minEnergy_mul_le_rayleighOnVec_of_isHermitian), so φ' is itself a balanced ground vector at μ. For symmetric T, U ≥ 0 |
Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosSemidefGround.lean (PR #4938) |
|
lyapunov_conjugate_isometry / hubbardCountSectorEmbedding_conjTranspose_mul_mul_apply / hubbardCountSectorEmbedding_conjTranspose_mul_upOccupationDiag_mul / blockWCoeff_sectorCompress_ne_zero_of_ne_zero / exists_posDefCompress_ground_in_balanced_sector |
(PR #4939; balanced PosDef-R_k compressed-coefficient capstone, Tasaki §10.2.4 Lemma 10.10, p. 363–367) the compressed balanced-sector coefficient matrix R_k := Jᴴ·blockWCoeff(φ)·J is positive-definite (for strict 0 < U(x) and kinetic connectivity). Starting from the PSD-W balanced ground φ (PR40f), the full-space Lyapunov/Schrödinger equation of W compresses through the isometry J (lyapunov_conjugate_isometry) to the sector equation for R_k (Math/PosSemidef/LyapunovIsometryCompress.lean); the kernel of the PSD solution R_k is invariant under the compressed kinetic matrix and each compressed occupation projection (via posSemidef_ground_kernel_propagation), reading off as sector occupation diagonals (hubbardCountSectorEmbedding_conjTranspose_mul_upOccupationDiag_mul); separation of site occupations forces basis vectors into ker R_k (basis_mem_ker_of_separating_projections); connectivity of the kinetic sector graph (edges witnessing nonzero compressed entries via hubbardCountSectorEmbedding_conjTranspose_mul_mul_apply and hubbardKineticSectorGraph_adj_entry_ne) yields the dichotomy R_k.PosDef ∨ R_k = 0 (posDef_or_eq_zero_of_connected_support); nonvanishing of R_k (blockWCoeff_sectorCompress_ne_zero_of_ne_zero) resolves the dichotomy to R_k.PosDef. This kernel-dichotomy argument is the endgame of discharging Theorem 10.2’s spin-reflection-positivity axiom. With symmetric T, U > 0 |
with Math/PosSemidef/LyapunovIsometryCompress.lean (PR #4939) and Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosDefCompress.lean (PR #4939) |
|
exists_signDefiniteCompress_ground_in_balanced_sector |
(PR #4940; sign-definite W_S compressed coefficient, Tasaki §10.2.4 Lemma 10.9, p. 363–367) the compressed balanced-sector coefficient matrix W_S := Jᴴ·blockWCoeff(φ)·J is sign-definite (either W_S.PosDef or (−W_S).PosDef) for the balanced Hermitian-W ground φ from PR40e-pre2b. The reusable dichotomy posDefCompress_dichotomy (extracted from the Lemma 10.10 capstone’s proof in PR #4939) shows that the absolute value P := |W_S| satisfies P.PosDef ∨ P = 0; the difference R' := P − W_S is PSD (hermitianAbs_sub_posSemidef) and solves the same Lyapunov equation (lyapunovEq_sub), yielding the dichotomy R'.PosDef ∨ R' = 0. The commutativity P · W_S = W_S · P (hermitianAbs_commute) and the cancellation (P − W_S)·(P + W_S) = 0 force either P = W_S (sign-definite positive) or P = −W_S (sign-definite negative), resolving W_S.PosDef ∨ (−W_S).PosDef — the sign-definiteness dichotomy that crystallizes Tasaki §10.2.4 Lemma 10.9. The witness state Γ(J·|W_S|·Jᴴ) is produced via gammaWState_hermitianAbs_isEigenvector as the balanced ground closing the Hermitian-W to PSD-W to sign-definite-W chain. With symmetric T, U > 0 |
with Fermion/JordanWigner/Hubbard/LiebAttractiveHermitianAbs.lean, Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosSemidefGround.lean, Math/PosSemidef/LyapunovIsometryCompress.lean (PR #4939), and Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosDefCompress.lean (PR #4940) |
|
blockWCoeff_trace_reduce_to_sector / balanced_signDefinite_ground_dotProduct_ne_zero |
(PR #4941; overlap-positivity endgame core, Tasaki §10.2.4 Theorem 10.2 uniqueness, p. 363–367) the balanced ground-state overlap is nonzero (non-orthogonality core). For two balanced ground states φ, φ' (each satisfying N̂_↑ = N̂_↓ = k) whose compressed sector coefficient matrices W_S := Jᴴ·blockWCoeff(φ)·J and W'_S := Jᴴ·blockWCoeff(φ')·J (with J = hubbardCountSectorEmbedding N k) are each sign-definite (the conclusion of PR #4940, Lemma 10.9), the overlap ⟨Γ(φ'), Γ(φ)⟩ = dotProduct (star φ') φ is nonzero. The full-space Frobenius pairing tr((blockWCoeff φ')ᴴ · blockWCoeff φ) reduces to the compressed-sector trace tr(W'_Sᴴ · W_S) via trace cyclicity and the balanced-support embedding property (blockWCoeff_trace_reduce_to_sector); both compressions are Hermitian by sign-definiteness, so this equals tr(W'_S · W_S). Splitting on the four sign combinations, the trace is nonzero by Matrix.PosDef.trace_mul_pos (trace of a product of two positive-definite matrices is strictly positive) and its negation variants. This is the reusable pairwise non-orthogonality step at the heart of Lieb’s uniqueness (Theorem 10.2); the passage to finrank ≤ 1 / singlet uniqueness is deferred to the capstone. With symmetric T, U > 0, kinetic-graph connectivity |
with supporting decls blockWCoeff_dotProduct_cross_eq (reducing overlap to Frobenius trace), and Matrix.PosDef.trace_mul_pos (Math/PosSemidef/TraceProductPos.lean) |
Fermion/JordanWigner/Hubbard/LiebAttractiveOverlapPositive.lean (PR #4941) |
balancedGroundEigenspace / balanced_ground_eigenspace_finrank_le_one / hermitianW_balanced_ground_signDefinite |
(PR #4942; ground-state uniqueness capstone, Tasaki, Springer 2020, §10.2.4 Theorem 10.2 (uniqueness), p. 363–367) the balanced ground eigenspace of the attractive Hubbard Hamiltonian has finrank ℂ ≤ 1 (unique ground state up to scalar multiple, per-spin N̂_↑ = N̂_↓ = k, strict 0 < U, connected hopping). The uniqueness combines the pairwise non-orthogonality (balanced_signDefinite_ground_dotProduct_ne_zero, PR #4941) with a real-form dimension count: the Γ-reflection antilinear involution (Θ² = id, a real involution — its Θ-fixed vectors form a real structure) decomposes the ground eigenspace via that real form. Every sign-definite (either PosDef or negation thereof) balanced Hermitian-W ground is Θ-invariant via hermitianW_balanced_ground_signDefinite (reusable forall form, existence corollary). Since finrank_ℂ(ground eig) ≤ finrank_ℝ(Θ-fixed) and pairwise non-orthogonality of the Θ-fixed grounds (overlap ≠ 0, real) forces finrank_ℝ(Θ-fixed) ≤ 1, we get finrank_ℂ ≤ 1 over ℂ (via finrank_complex_le_finrank_real_antilinearFixed + finrank_le_one_of_pairwise_bilinForm_ne_zero + antilinearInvolutionFixed, Math/RealForm/AntilinearFixedFinrank.lean). With symmetric T, U(x) > 0, connected kinetic sector graph |
with supporting generic toolkit Math/RealForm/AntilinearFixedFinrank.lean + Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosDefCompress.lean (PR #4939) and Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedPosSemidefGround.lean (PR #4938) |
Fermion/JordanWigner/Hubbard/LiebAttractiveBalancedUniqueness.lean (PR #4942) |
fermionTotalSpinPlus_commute_hubbardOnSiteInteractionSite / fermionTotalSpin{Plus,Minus,Z}_commute_attractiveHubbardHamiltonian / fermionTotalSpinSquared_commute_attractiveHubbardHamiltonian |
SU(2) invariance of the attractive Hubbard Hamiltonian (Tasaki §10.2.1 / §9.3.3 eq. (9.3.35)): the site-dependent-U interaction Σ_x U_x n̂_{x↑} n̂_{x↓} commutes with Ŝ⁺_tot, N̂_↑, N̂_↓ (per-site clone of the §9.3.3 scalar-U commutators), hence the three generators Ŝ⁺_tot, Ŝ⁻_tot (adjoint route via attractiveHubbardHamiltonian_isHermitian), Ŝ³_tot and the Casimir (Ŝ_tot)² all commute with Ĥ = attractiveHubbardHamiltonian N T U. Consumed by the eventual uniqueness→singlet step (unique GS + commuting Casimir ⟹ (Ŝ_tot)²-eigenstate). Axiom-free. |
Fermion/JordanWigner/Hubbard/LiebAttractiveSU2Invariance.lean (PR #4943) |
|
fermionTotalSpinSquared_commute_fermionTotalSpin{Plus,Z} / fermionTotalSpinSquared_commute_fermionTotal{Number,UpNumber,DownNumber} / balancedGround_totalSpinSquared_eigenvector |
The balanced ground state is a (Ŝ_tot)²-eigenstate (Tasaki §10.2.1 Theorem 10.2 eigenstate step / §9.3.3): the Casimir commutes with Ŝ⁺_tot (adjoint of the Ŝ⁻_tot commute via Hermiticity), with the total number N̂, with Ŝ³_tot, and hence (via N̂_↑ = ½N̂ + Ŝ³_tot, N̂_↓ = ½N̂ − Ŝ³_tot) with N̂_↑, N̂_↓; so (Ŝ_tot)² preserves balancedGroundEigenspace. Since that eigenspace has finrank ℂ ≤ 1 (balanced_ground_eigenspace_finrank_le_one), any nonzero balanced ground state ψ satisfies (Ŝ_tot)² ψ = μ • ψ for some real μ (real via the Hermitian bridge isHermitian_mulVec_eigenvalue_eq_ofReal; the scalar dependence via the generic exists_smul_of_mem_of_finrank_le_one). The identification μ = S(S+1) (singlet S = 0) is deferred to the step that finishes Theorem 10.2. Axiom-free. |
Fermion/JordanWigner/Hubbard/FermionTotalSpinCasimirCharges.lean, Fermion/JordanWigner/Hubbard/LiebAttractiveTotalSpinEigenstate.lean, Math/SubmoduleFinrankLeOne.lean, Math/CommutingHermitianEigenvector.lean (PR #4944) |
|
gammaWState_single_diag / fermionTotalSpinSquared_mulVec_basisVec_merge_self / balancedGround_totalSpinSquared_eigenvalue_zero |
The balanced ground state is a spin singlet (Ŝ_tot)² ψ = 0 (Tasaki §10.2.4 Theorem 10.2 singlet step, p. 365 / §9.3.3): identifies the eigenvalue μ of the eigenstate step as 0 (S_tot = 0). For a fixed count-k sector index u = s.val, the explicit reference ref := Γ(E_{u,u}) = gammaWState N (single u u 1) equals (up to a Jordan–Wigner ±1) the doubly-occupied basis configuration basisVec (merge u u) (gammaWState_single_diag), which is a singlet: Ŝ⁺ annihilates it (each occupied-down site has an occupied up, so c†_↑ c_↓ vanishes) and Ŝ³ = 0 (balanced), hence (Ŝ_tot)² ref = 0 (fermionTotalSpinSquared_mulVec_basisVec_merge_self). Taking the Hermitian-W ground representative φ of Lemma 10.9 (exists_signDefiniteCompress_ground_in_balanced_sector), the overlap ⟨ref, φ⟩ = (blockWCoeff φ)_{u,u} (via the coordinate isometry blockWCoeff_dotProduct_cross_eq) is nonzero because the compressed coefficient Jᴴ (blockWCoeff φ) J is sign-definite, so its diagonal is nonzero (Matrix.PosDef.diag_pos); with finrank ≤ 1 giving φ = c • ψ (same eigenvalue μ), Hermiticity of (Ŝ_tot)² forces μ ⟨ref, φ⟩ = ⟨(Ŝ_tot)² ref, φ⟩ = 0, hence μ = 0 and (Ŝ_tot)² ψ = 0. With symmetric T, U(x) > 0, connected hopping. Axiom-free. |
Fermion/JordanWigner/Hubbard/LiebAttractiveSingletGround.lean (PR #4945) |
|
configSectorNumberCompress_su2_{12,23,31} / configSectorNumberCompress_attractive_commute_{one,two,three} / attractiveHubbard_balanced_energy_eq_number_sector |
E_bal = E_full full-Ne-sector lift (Tasaki §10.2.1 Theorem 10.2, full-sector lift, PR-D’ #4852): the balanced-block (Ŝ³ = 0, per-spin N̂_↑ = N̂_↓ = k) compression minimum energy E_bal equals the full Ne = 2k-electron sector compression minimum E_full. E_full ≤ E_bal is the balanced-into-full variational inclusion (N̂ φ = (N̂_↑ + N̂_↓) φ = Ne φ). E_bal ≤ E_full feeds the Ne-sector compression to the generic Theorem A.17 engine ham_eigenstate_spin_zero_or_half, whose hypotheses are the number-sector compressed Hermitian/su(2)/commute relations of Ĥ and the Cartesian generators Ŝ⁽¹⁾ = ½(Ŝ⁺+Ŝ⁻), Ŝ⁽²⁾ = −(i/2)(Ŝ⁺−Ŝ⁻), Ŝ³ (LiebAttractiveFullSectorSU2Algebra.lean, the number-sector analogue of TJFillingCompressSpinAlgebra.lean); the engine’s compressed eigenstate Φ has Ŝ³_W Φ = 0 or = ½ Φ, and for even Ne the ½ branch is killed (N̂_↑ = (Ne+1)/2 is a half-integer, attractiveHubbard_number_even_spinZ_half_eq_zero), so the lift of Φ is a nonzero balanced state at E_full. Even-Ne parity mirror of the odd-Ne t-J route tJ_perronFrobeniusMin_le_hermitianMinEigenvalue. Axiom-free. The remaining full-sector singlet-uniqueness lift (a commuting-Hermitian joint-eigenbasis argument) is deferred to the consuming discharge. |
Fermion/JordanWigner/Hubbard/LiebAttractiveFullSectorSU2Algebra.lean + Fermion/JordanWigner/Hubbard/LiebAttractiveFullSectorEnergy.lean (PR #4946) |
|
fermionTotalSpinSquared_eq_cartesianSqSum / attractiveHubbardFullSectorGround / attractiveHubbardFullSectorGround_le_balanced / attractiveHubbardFullSectorGround_unique_singlet |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Fermion/JordanWigner/Hubbard/LiebAttractiveFullSectorUnique.lean, Math/AngularMomentum/Multiplet.lean, Math/CommutingHermitianEigenvector.lean (PR #4946) |
| Lean name | Statement | File |
|—|—|—|
| bipartitionComplement / HoppingRespectsBipartition / sublatticeImbalance | the bipartition Λ = A ⊔ Aᶜ, the “hops only across sublattices” predicate, and \|\|A\|−\|B\|\| | Fermion/JordanWigner/Hubbard/LiebRepulsive.lean |
| repulsiveHubbardHamiltonian / symmetricRepulsiveHubbardInteraction / symmetricRepulsiveHubbardHamiltonian | the uniform repulsive model Ĥhop + U Σ n̂↑n̂↓ (eq. (10.2.5)) and the symmetric form Σ_x U_x (n̂↑−½)(n̂↓−½) (eq. (10.2.6)) | Fermion/JordanWigner/Hubbard/LiebRepulsive.lean |
| hubbardGroundSubmoduleAtElectronNumber / IsLiebRepulsiveHamiltonian / IsLiebRepulsiveModel | non-hard-core fixed-N ground subspace (energy eigenspace ⊓ number sector); the two allowed interaction forms; the packaged model hypotheses (bipartite + symmetric + connected hopping) | Fermion/JordanWigner/Hubbard/LiebRepulsive.lean |
← Multi-mode fermion via Jordan–Wigner (P2 backbone) · Catalogue · Multi-mode fermion via Jordan–Wigner (P2 backbone) →