Historical implementation record normalized from the former roadmap table. Active work is governed by tracking Issues.
Fin (2K) / 2D Fin (2K) × Fin (2L) / 3D (Fin (2K) × Fin (2L)) × Fin (2M): state definitions, magnetisation = 0, ∈ H_0, per-bond Ŝ_x · Ŝ_y · |Φ_Néel⟩ = (1/2)|swap⟩ - (1/4)|Φ_Néel⟩ for every adjacent and wrap-around bond (Tasaki §2.5 (2.5.3)), per-bond expectation ⟨Φ_Néel, Ŝ_x · Ŝ_y · Φ_Néel⟩ = -(1/4) (Tasaki §2.5 (2.5.4) ingredient), per-bond Ŝ^z · Ŝ^z correlation -(1/4) and off-diagonal correlator vanishing, parallel-bond expectation +1/4, K=1 chain Heisenberg energy J/2, time-reversal Θ̂_tot · |Φ_Néel⟩ action across all dimensions, Marshall sign machinery (generic marshallSignOf + chain / 2D / 3D specialisations + flipConfig + Marshall × time-reversal bridge), the generic graph-centric neelStateOf : (V → Bool) → ((V → Fin 2) → ℂ) primitive (Tasaki §2.5 (2.5.2) graph-centric form) of which the chain / 2D / 3D versions are 1-line corollaries via the _eq_neelConfigOf / _eq_neelStateOf bridges, the Marshall-dressed standard basis marshallDressedBasis A σ := marshallSignOf A σ • basisVec σ (Tasaki §2.5 (2.5.8)) with orthonormality and H_M-membership, the realness of dressed Heisenberg matrix elements for real coupling J (Tasaki §2.5 p. 41, Property (i): each ((spinHalfDot x y) σ σ').im = 0, hence ((heisenbergHamiltonian J) σ σ').im = 0, hence the dressed bilinear pairing has zero imaginary part), the Marshall sign trick (Tasaki §2.5 p. 41, Property (ii)): for real non-negative J supported on bipartite bonds and σ ≠ σ', the dressed off-diagonal Heisenberg pairing has non-positive real part, the swap-connectivity (Tasaki §2.5 p. 41–42, Property (iii)): for a connected graph G and any σ x ≠ σ y, the configurations σ and basisSwap σ x y are connected by a chain of single-edge swaps, and the Marshall–Lieb–Mattis Theorem 2.2 in H_0 (matrix level): assembled across PRs α-5a through α-5o, the shifted dressed Heisenberg matrix B = c · I − M (symmetric, non-negative, irreducible on H_0) admits a unique-up-to-positive-scalar strictly positive Perron–Frobenius eigenvector — equivalent to the matrix-level Tasaki (2.5.4) ground-state expansion Σ_σ c_σ \|Ψ̃^σ⟩ with c_σ > 0. This is the spin-1/2 / Néel-state predecessor of the completed general spin-S sector theorem tracked in P1m.Done
pathGraph (N+1) □ pathGraph (N+1) and cycleGraph (N+2) □ cycleGraph (N+2); Hermiticity + Gibbs state companion families (full 11-companion family per variant: _isHermitian, _commute_hamiltonian, _GibbsExpectation_zero, _im_of_isHermitian, _commutator_hamiltonian, _mul_hamiltonian_im, _hamiltonian_sq_im, _hamiltonian_pow_im, _anticommutator_im, _commutator_re, _HamiltonianVariance_im, _partitionFn_im, _ofReal_re_eq, _pow_trace) at parity with the 1D open / periodic chainDone
H_0 to general spin S (N = 2S) and arbitrary magnetization sector M via the subtype magConfigS V N M. Sector matrices: shifted dressed (shiftedDressedSReMatrixOnMagSector), dressed (dressedHeisenbergSReMatrixOnMagSector), un-dressed real-form (heisenbergHamiltonianSReMatrixOnMagSector), and un-dressed complex-form (heisenbergHamiltonianSMatrixOnMagSector). Bipartite raise/lower reachability (γ-3 connectivity for general spin) lifted to the sector subtype. PF application: IsIrreducible (#846), positive Perron eigenvector existence (#847) and uniqueness (#848) on the shifted sector matrix. Marshall sign conjugation forward (#853) + inverse (#854) gives a real-form sector eigenvector existence with Marshall sign structure. Eigenvector uniqueness (#854) at fixed μ and eigenvalue uniqueness (#856, via dressed-sector symmetry + Rayleigh identity). Bundled real-form ground-state theorems: same-μ form (#855) and forced-eigenvalue form (#859). Complex-form bridge: complex sector matrix Hermiticity + real-↔-complex eigenvector correspondence (#857, #858, #861). Complex-form existence (#860), Marshall-positive uniqueness (#862), and strongest bundled COMPLEX ground-state theorem marshallLiebMattis_spinS_heisenbergSector_complexGroundState_full (#865) — the COMPLEX-Hilbert-space form of Tasaki §2.5 Theorem 2.2 in the magnetization sector. Generic spin S, arbitrary bipartite-antiferromagnetic Heisenberg coupling supported on a connected bipartite graph, with the intermediate-existence hypothesis. The next step is the lift from the magnetization sector to the FULL Hilbert space — comparing ground-state energies across magnetization sectors.Done
\|A\| ≠ \|¬A\|) — final statement. The current Prop definition tasaki_2_5_theorem_2_3 is the structural, h_intermediate-free statement: it closes the conclusion from the physical hypotheses (1 ≤ N, 1 ≤ \|A\|, 1 ≤ \|¬A\|) rather than the older vacuous-at-N=1 intermediate-support hypothesis. The canonical proof witnesses are tasaki_2_5_theorem_2_3_bipartiteToy (PR #3891, toy coupling) and tasaki_2_5_theorem_2_3_of_bipartiteCompletePositive (PR #3893, general bipartite J positive on the complete bipartite graph). These declarations are the structurally repaired replacements for the older h_intermediate capstones removed in PR #3917. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42Truly-unconditional closure at all N ≥ 1 (PR #3891 toy, PR #3893 general)
Ŝ³_tot \|Φ_GS⟩ = 0 for the anisotropic XXZ + single-ion Hamiltonian (2.5.14) on a connected bipartite lattice with \|A\| = \|B\|, under (i) −1 < λ ≤ 1, D ≥ 0 or (ii) λ ≥ 1, D ≤ 0. The model is only U(1)-invariant (not SU(2)), so the proof uses even/odd-sector Perron–Frobenius (at most double degeneracy) + a deformation argument from the SU(2) point (λ,D)=(1,0) rather than MLM directly. Foundation laid (#3740): anisotropicHeisenbergS definition + Hermiticity + reduction to isotropic Heisenberg at λ=1, D=0. (e)-(g) chain: ground-state degeneracy ≤ 2 CONDITIONAL (#3824–#3837): (e) parity-block matrix irreducibility (#3824), (f) bridge layer giving complex dressed parity-block submatrix finrank ℂ ≤ 1 (#3825–#3831) + block-diag bridge (#3832), (g) dressed-and-bare assembly + axis-swap (#3833–#3837), giving anisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one for general N (with AxisSwapUnitaryS) and spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_of_blocks_le_one for N = 1. (h) chain: block-sum finrank EQUALITY infrastructure (#3840–#3844): (h.1) #3840 reverse block-diag bridge giving per-block submatrix-full intersection finrank equality, (h.2) #3841 strengthens involution decomposition to finrank equality, (h.3) #3842 combines (h.1)+(h.2) into finrank ℂ (eig M μ) = ∑_p finrank ℂ (eig M.submatrix_p μ) for parity-block-diagonal M commuting with P, (h.4) #3844 submatrix-based ≤ 2 wrappers. (i) chain: Hermitian spectral chain (#3846–#3855): (i.1) #3846 submatrix Hermiticity, (i.2) #3847 submatrix eigenvalue realness (μ.im = 0), (i.3) #3848 submatrix minimum eigenvalue exists, (i.4) #3849 Hermitian eigenspace = ⊥ below min, (i.5) #3850 block-diag eigenspace = ⊥ below joint per-block min, (i.6) #3851 full eig ≤ 2 at min(per-block mins) given per-block ≤ 1 at min, (i.7) #3854 bare Ĥ' specialisation, (i.8) #3855 bare anisotropic Ĥ specialisation via axis-swap (general N with AxisSwapUnitaryS + spin-1/2 instance) — the bridge to unconditional ≤ 2 modulo PF eigenvalue identification with hermitianMinEigenvalue. (j) chain: PF eigenvalue identification (#3857–#3861): (j.1) #3857 PF positive eigenvector exists for unshifted dressed submatrix, (j.2) #3858 lift to complex, (j.3) #3859 hermitianMinEigenvalue ≤ μ from eigenvector existence, (j.4) #3860 packaged form, (j.5) #3861 consumer-friendly conditional bound at hermitianMinEigenvalue (needs the ν_PF = hermitianMinEigenvalue hypothesis explicit). Target balanced-sector PF discharge (Issue #3739): off-diagonal anisotropic/Heisenberg agreement, real sector matrices, the Marshall-dressed shifted anisotropic sector matrix, structural irreducibility, and Collatz–Wielandt PF/minimum identification now provide the balanced-sector finrank ℂ ≤ 1 input at the spin-1/2 target point and in the general spin-S target sector; the PF-free target wrappers no longer take an explicit h_balanced_sector_pf callback. Strict-gap, SU(2)-uniqueness, and MLM endpoint wrappers now replace the explicit balanced/full equality input by the standard strict gap over all non-balanced non-empty magnetization sectors, derive that strict gap from SU(2)-endpoint global uniqueness, and then construct the SU(2) uniqueness input from the general Theorem 2.3 MLM/Casimir/PF endpoint. D-boundary extension: the spin-1/2 parity-block route has a dedicated D ≥ 0 version because single-ion ±2 moves are impossible for Fin (1+1). The general spin-S route now also has a bond-only parity reachability replacement for the single-ion branch, giving general D ≥ 0 parity-block irreducibility and the MLM/Casimir target wrappers anisotropicHeisenbergS_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_D_nonneg_general and aHeisS_target_zeroMag_of_MLM_casLadder_t23_pf_D_nonneg_gen. λ=1 boundary: at spin 1/2, (S^3)^2 = (1/4)I, so singleIonAnisotropyS D 1 is a scalar shift and anisotropicHeisenbergS J 1 D 1 reduces to the Heisenberg Hamiltonian plus D|Λ|/4; the SU(2) Theorem 2.3/MLM uniqueness transfers to target uniqueness and zero magnetization at λ = 1. For general spin-S, the SU(2)-point wrappers cover λ = 1, D = 0, and for 2 ≤ N the ion-only parity reachability route gives the λ = 1, D > 0 endpoint wrappers aHeisS_target_finrank_le_one_of_MLM_casLadder_t23_pf_lam1_D_pos_gen and aHeisS_target_zeroMag_of_MLM_casLadder_t23_pf_lam1_D_pos_gen. Case (ii) bridges: the case-(ii) path-region lemmas show the deformation path stays in λ ≥ 1, D ≤ 0; the first case-(ii) target wrappers reuse the balanced-sector PF bridge while leaving balanced-sector/full-ground equality plus full finrank <= 2 explicit; the strict-gap wrappers replace the direct balanced-sector/full-ground equality input by the strict sector gap; the no-full-finrank wrappers then use sector projection and Hermitian below-min exclusion to remove the full finrank <= 2 input once strict gap is supplied; the crossing-callback bridge compresses the remaining strict-gap derivation to a single target crossing contradiction callback; the path-callback bridge reduces that target callback to a contradiction for crossings along the case-(ii) path; the crossing-set bridge reduces the path callback to contradiction for non-empty perMCrossingSet M ∩ Icc 0 1; the first-crossing bridge reduces crossing-set non-emptiness to contradiction at sInf (perMCrossingSet M ∩ Icc 0 1); the argmin-first-crossing bridge reduces the target contradiction to the sector whose first crossing minimises those sInf values; the first-crossing finrank bridge proves that argmin callback from a finrank <= 2 bound at the selected first crossing; the path-global finrank bridge moves this to every t ∈ Icc 0 1; the block-path finrank bridge reduces it to full-ground-energy parity-block submatrix simplicity; and the block-PF/min bridge reduces that to pathwise bare parity-block PF simplicity plus PF/min identification; and the parity-gauge sign layer introduces the case-(ii) block gauge needed to flip exactly the ±2 parity-bond and single-ion moves; and the local sign layer proves strict shifted-entry positivity for transverse, parity-bond, and single-ion elementary moves; and the block reachability, block non-negativity, step-support, raw support-classification, and boundary move-set bridges reduce parity-block irreducibility to conditional irreducibility under the bipartite support-zero assumption on J.The public general spin-S 2 ≤ N parameter-region wrappers
anisotropicHeisenbergS_tasaki24_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_general and
aHeisS_tasaki24_target_zeroMag_of_MLM_casLadder_t23_pf_gen package the general spin-S surface. The
spin-1/2 wrappers
spinHalf_anisotropicHeisenbergS_tasaki24_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf and
spinHalf_aHeisS_tasaki24_target_zeroMag_of_MLM_casLadder_t23_pf now package the exact N = 1
surface: -1 < λ < 1, D ≥ 0; λ = 1, using the scalar-shift boundary; and strict case (ii) 1 <
λ, D ≤ 0.