S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) (part 3 of 4)Interim authority. This lossless catalogue chunk remains authoritative for formalization status and capstone identification until Issue #5228. The version 1 JSON catalogue is still a non-authoritative prototype.
Interim catalogue › Spin foundations and Tasaki Chapter 2
| Lean name | Statement |
|—|—|
| collatzWielandtFn_le_of_pos_eigenvector | (j.13.e.1) CW upper bound at PF eigenvalue (symmetric nonneg) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3876): for a symmetric nonneg matrix A : Matrix n n ℝ with strictly positive eigenvector v at eigenvalue μ, for any nonneg x ≠ 0, collatzWielandtFn A x ≤ μ. Proof: dot with v, use symmetry ∑ v_i (Ax)_i = μ ∑ v_i x_i, divide by ∑ v_i x_i > 0. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/CollatzWielandtUpperBoundSymmetric.lean) |
| abs_mulVec_le_mulVec_abs / abs_eigenvalue_mul_abs_le_mulVec_abs / abs_eigenvalue_le_collatzWielandtFn_abs (with le_collatzWielandtFn_of_all_supp_ratios_le) | (j.13.e.2-4) CW lower bound at abs eigenvector (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3877): triangle inequality |A *ᵥ w|_i ≤ (A *ᵥ |w|)_i for nonneg A + eigenvector specialization |λ| * |w_i| ≤ (A *ᵥ |w|)_i + CW lower bound |λ| ≤ collatzWielandtFn A |w| for w ≠ 0 eigenvector at λ of nonneg A. Plus a new public CW infrastructure lemma le_collatzWielandtFn_of_all_supp_ratios_le (dual to lt_of_all_ratios_gt). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/CollatzWielandtLowerBoundEigenvec.lean) |
| real_eigenvalue_le_of_pos_eigenvector | (j.13.e.5) Real eigenvalue ≤ PF eigenvalue (symmetric nonneg) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3878): combine (j.13.e.4) and (j.13.e.1) at |w|: λ ≤ |λ| ≤ CW(|w|) ≤ μ. Real-side combination preceding the complex Hermitian bridge (j.13.e.6). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/RealEigenvalueLePF.lean) |
| hermitianMaxEigenvalue_le_of_pos_eigenvector (with isHermitian_map_ofReal_of_isSymm, norm_mulVec_complex_le_mulVec_norm) | (j.13.e.6) Complex Hermitian max eigenvalue ≤ PF eigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3879): for a real symmetric nonneg B_real with positive eigenvector v at μ, hermitianMaxEigenvalue (B_real.map ofReal).IsHermitian ≤ μ. Proof via complex eigenvector → wAbs = ‖w_complex‖ (complex modulus, real vector) → triangle inequality → CW lower bound + (j.13.e.1) → |λ| ≤ μ. Completes the (j.13.e) CW max characterization HARD step. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianMaxEigenvalueLeOfPF.lean) |
| hermitianMaxEigenvalue_eq_of_pos_eigenvector | (j.13.f) Complex Hermitian max eigenvalue = PF eigenvalue (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3880): antisymmetric combination of (j.13.d) μ_PF ≤ max (via v lifted to ℂ using RingHom.map_mulVec) and (j.13.e.6) max ≤ μ_PF. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianMaxEqPF.lean) |
| hermitianMinEigenvalue_eq_sub_hermitianMaxEigenvalue_shift (with isHermitian_smul_one_sub_of_real) | (j.13.g) Spectrum shift: hermitianMinEigenvalue M = c − hermitianMaxEigenvalue (c·I − M) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3881): for any Hermitian M : Matrix n n ℂ and real c. Proof: spectrum.singleton_sub_eq gives spectrum ℝ (c·I − M) = {c} − spectrum ℝ M, so Finset.image univ B-eigenvalues = (Finset.image univ M-eigenvalues).image (c − ·). Antimonotonicity of (c − ·) then gives max = c − min. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianSpectrumShift.lean) |
| hermitianMinEigenvalue_lift_eq_sub_pf (with map_smul_one_sub) | (j.13.h.1) Generic shift identification hermitianMinEigenvalue M_complex = c − μ_PF (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3882): combine (j.13.g) + (j.13.f) + Matrix.map identity for c·I − ·. Generic version usable by (j.13.h.2) specialisations. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Math/HermitianMinEqOfShiftPF.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_submatrix_hermitianMinEigenvalue_eq_pf / axisSwappedAnisotropicHeisenbergS_submatrix_hermitianMinEigenvalue_eq_pf | (j.13.h.2) Dressed/bare submatrix ν_PF = hermitianMinEigenvalue identification (UNCONDITIONAL) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3883): specialise (j.13.h.1) to the dressed parity-block submatrix using (j.1) PF positive eigenvector + matrix-identity bridge + (j.6) spectrum-eq invariance, then transfer to the bare submatrix via Marshall similarity (j.8) #3865. Discharges the deferred hypothesis in (j.5) #3861 / (j.11) #3869 conditional bounds. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedBareSubmatrixMinEqPFStructural.lean) |
| axisSwappedAnisotropicHeisenbergS_submatrix_finrank_le_one_at_hermitianMinEigenvalue | (j.13.h.3) Bare submatrix finrank ≤ 1 at hermitianMinEigenvalue (UNCONDITIONAL on PF=min) (Tasaki §2.5 Theorem 2.4, Issue #3871, PR #3884): combines (j.13.h.2-bare) identification + inline parameterised PF finrank bound chain (Perron eigenspace_finrank_le_one_of_pos_eigenvec on shifted at c − ν + eigenspace_smul_one_sub_finrank_eq shift identity + ℝ → ℂ bridge + Marshall similarity) + (j.11) conditional wrapper. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareSubmatrixFinrankLeOneAtMinStructural.lean) |
| exists_raiseLowerReachableS_bipartite_of_over_under_eq_sublattice_alt / exists_raiseLowerReachableS_bipartite_of_over_under_structural / raiseLowerReachableS_bipartiteCompleteGraph_of_eq_magSumS_structural / parityReachableS_total_structural | (#3887.1-.3) Foundational structural fix for h_intermediate (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): the (j.1)-(j.13) chain’s h_intermediate is unsatisfiable at N = 1 (rendering (j.13.i) vacuous). Fix: in the same-sublattice over/under hard case there is an alternative path requiring σ z > 0 instead of σ z < N; at N ≥ 1 every (σ z).val satisfies at least one of the two. Structural branching variant drops h_intermediate entirely, requiring only hA_ne + hB_ne + 1 ≤ N. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (files Quantum/SpinS/BipartiteCompleteGraphAltPath.lean, Quantum/SpinS/BipartiteCompleteGraphStructural.lean) |
| shiftedDressedAxisSwappedReMatrixOnParityBlock_isIrreducible_structural | (#3887.4) Structural parity-block irreducibility (no h_intermediate) (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): structural variant of ..._isIrreducible using parityReachableS_total_structural. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedAxisSwapBlockIrreducibleStructural.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSReMatrixOnParityBlock_pos_eigenvector_exists_structural | (#3887.5) (j.1) structural PF positive eigenvector (no h_intermediate) (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): structural variant of (j.1) using (#3887.4). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/DressedSubmatrixPFEigenvectorStructural.lean) |
| dressedAxisSwappedAnisotropicHeisenbergS_submatrix_hermitianMinEigenvalue_eq_pf_structural / axisSwappedAnisotropicHeisenbergS_submatrix_hermitianMinEigenvalue_eq_pf_structural | (#3887.6) (j.13.h.2) structural dressed/bare hermitianMinEigenvalue identification (no h_intermediate) (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): structural variants using (#3887.5). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/DressedBareSubmatrixMinEqPFStructural.lean) |
| axisSwappedAnisotropicHeisenbergS_submatrix_finrank_le_one_at_hermitianMinEigenvalue_structural | (#3887.7) (j.13.h.3) structural bare submatrix finrank ≤ 1 at hermitianMinEigenvalue (no h_intermediate) (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): full chain reconstructed without h_intermediate. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/BareSubmatrixFinrankLeOneAtMinStructural.lean) |
| spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_truly_unconditional | 🎯 (#3887.8) Spin-1/2 anisotropic Ĥ eigenspace ≤ 2 (TRULY UNCONDITIONAL) (Tasaki §2.5 Theorem 2.4, Issue #3887, PR #3888): combines (#3887.7) at parity 0/1 with (j.12) #3870 spin-1/2 capstone. Non-vacuous closure of (j.13.i) — the spin-1/2 case now has a usable bound without the h_intermediate caveat. MILESTONE: this is the non-vacuous spin-1/2 closure of obligation (1) of Tasaki §2.5 Theorem 2.4. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfStructural.lean) |
| axisSwapUnitarySSpinS_anisotropic_axisSwapped_eigenspace_finrank_eq / anisotropicHeisenbergS_eigenspace_finrank_le_two_unconditional_general | General spin-S axis-swap discharge for Theorem 2.4 obligation (1) (Tasaki §2.5 Theorem 2.4, Issue #412): the concrete π/2 rotation about spin-axis 1, axisSwapUnitarySSpinS N, now instantiates the earlier AxisSwapUnitaryS N interface for every spin parameter N. The PR exposes no-argument wrappers for the axis-swap eigenspace-dimension equality, the conditional parity-block and submatrix-block ≤ 2 bounds, the min-block ≤ 2 bound, the Hermitian-minimum equality, and the structural general-N capstone anisotropicHeisenbergS_eigenspace_finrank_le_two_unconditional_general. This discharges the explicit axis-swap-unitary argument in the strict case-(i) degeneracy chain; the SU(2)-uniqueness target wrappers are handled in the later obligation-(2) row, and Tasaki case (ii) now has conditional, strict-gap, and no-full-finrank bridges recorded in the case-(ii) rows, with the strict-gap derivation still explicit. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AxisSwapUnitarySSpinS.lean) |
| anisotropicHeisenbergS_target_finrank_le_one_of_balanced_sector_pf / anisotropicHeisenbergS_target_groundState_zero_magnetization_of_balanced_sector_pf / anisotropicHeisenbergS_balanced_sector_pf_at_target / anisotropicHeisenbergS_target_finrank_le_one_of_balanced_eq_full / anisotropicHeisenbergS_target_groundState_zero_magnetization_of_balanced_eq_full | General spin-S target conditional bridge with balanced-sector PF discharged (Tasaki §2.5 Theorem 2.4, Issue #412): packages the final linear-algebra step after the general spin-S finrank ≤ 2 degeneracy capstone. If the target full ground eigenspace has finrank ≤ 2, the balanced sector attains the full ground energy, and the balanced-sector ground eigenspace has finrank ≤ 1, then the full target ground eigenspace has finrank ≤ 1; the companion wrapper then gives zero total Ŝ³ magnetization for every non-zero target ground state. The new general spin-S PF wrapper chooses a finite strict diagonal shift and applies the existing anisotropic sector PF/minimum theorem, so the PF-free target wrappers no longer take an explicit balanced-sector PF callback. The direct balanced-sector/full-ground equality input is superseded by the strict-gap wrappers in the next row; for case (ii), the conditional, strict-gap, and no-full-finrank bridges are recorded in the case-(ii) rows and the strict-gap derivation remains explicit. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSTargetConditionalBridge.lean, Quantum/SpinS/AnisotropicHeisenbergSpinSBalancedSectorPFTarget.lean) |
| anisotropicHeisenbergParametricPath_in_case_ii_region / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_balanced_eq_full / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_balanced_eq_full | General spin-S case-(ii) path and conditional target bridge (Tasaki §2.5 Theorem 2.4, Issue #412): proves that the deformation path from (1,0) to a target satisfying 1 <= lambda, D <= 0 remains in the case-(ii) region on [0,1], then repackages the balanced-sector PF target bridge under case-(ii) hypotheses. These first case-(ii) wrappers keep the remaining target inputs explicit as balanced-sector/full-ground equality plus full finrank <= 2; they do not reuse the case-(i) axis-swap sign argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIConditionalBridge.lean) |
| anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_strict_gap / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_strict_gap | General spin-S case-(ii) target bridge from strict sector gap (Tasaki §2.5 Theorem 2.4, Issue #412): composes the arbitrary-parameter strict-gap target bridge with the case-(ii) theorem surface. The direct balanced-sector/full-ground equality input from the first case-(ii) wrappers is replaced by the strict gap E_balanced < E_M over every non-balanced non-empty magnetization sector under 1 <= lambda, D <= 0; the remaining full ground eigenspace finrank <= 2 input stays explicit in this intermediate wrapper. This is a case-(ii) bridge step, not the final case-(ii) endpoint. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIStrictGapBridge.lean) |
| anisotropicHeisenbergS_groundState_mem_balanced_sector_of_strict_gap / anisotropicHeisenbergS_target_finrank_le_one_of_strict_gap_no_full_le_two / anisotropicHeisenbergS_target_groundState_zero_magnetization_of_strict_gap_no_full_le_two / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_strict_gap_no_full_le_two / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_strict_gap_no_full_le_two | General spin-S target bridge from strict sector gap without the full finrank <= 2 input (Tasaki §2.5 Theorem 2.4, Issue #412): proves that if the balanced sector attains the full ground energy and every non-balanced non-empty magnetization sector has strictly larger minimum, then every full ground vector lies in the balanced magnetization sector. This uses the sector-projection eigenvector bridge and hermitian_eigenspace_eq_bot_of_real_lt_min, not the case-(i) parity-block finrank <= 2 contradiction. Composing this containment with balanced-sector Perron–Frobenius simplicity gives full target uniqueness and zero total magnetization from strict sector gap alone; the case-(ii)-named wrappers keep only the theorem-facing 1 <= lambda, D <= 0 hypotheses plus the strict-gap input. This removes the explicit case-(ii) full finrank <= 2 input; deriving the case-(ii) strict gap remains future work. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSTargetFromStrictGapNoFullFinrank.lean) |
| anisotropicHeisenbergS_case_ii_strict_gap_all_M_of_crossing_contradiction / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_crossing_contradiction / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_crossing_contradiction | General spin-S case-(ii) strict-gap and target bridge from a crossing contradiction callback (Tasaki §2.5 Theorem 2.4, Issue #412): compresses the remaining case-(ii) strict-gap derivation to one theorem-shaped callback. If every non-balanced target crossing E_M <= E_balanced contradicts the case-(ii) hypotheses 1 <= lambda, D <= 0, then order duality gives the strict gap E_balanced < E_M for every non-balanced non-empty sector. The target wrappers feed that strict gap to the no-full-finrank bridge above, so the public endpoint surface no longer exposes either balanced/full equality, full finrank <= 2, or strict gap directly; the remaining mathematical task is proving the crossing contradiction callback. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIStrictGapFromCrossing.lean) |
| anisotropicHeisenbergS_case_ii_crossing_contradiction_of_path_crossing_contradiction / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_path_crossing_contradiction / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_path_crossing_contradiction | General spin-S case-(ii) target bridge from a path crossing contradiction callback (Tasaki §2.5 Theorem 2.4, Issue #412): evaluates the case-(ii) deformation path at t = 1. If every crossing along the path inside the region 1 <= lambda, D <= 0 contradicts the path hypotheses, then a target crossing E_M(lambda,D) <= E_balanced(lambda,D) is impossible. The target wrappers feed this contradiction to the crossing-callback bridge above. The remaining mathematical task is now the path crossing contradiction callback itself. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIICrossingFromPath.lean) |
| anisotropicHeisenbergS_case_ii_path_crossing_contradiction_of_set_contradiction / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_set_contradiction / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_set_contradiction | General spin-S case-(ii) target bridge from a crossing-set non-emptiness contradiction (Tasaki §2.5 Theorem 2.4, Issue #412): a pointwise path crossing is a witness that perMCrossingSet M ∩ Icc 0 1 is non-empty. Therefore, if every non-balanced non-empty sector has contradictory crossing-set non-emptiness, every path crossing is impossible, and the target wrappers feed that path contradiction to the path-callback bridge above. The remaining mathematical task is now the crossing-set non-emptiness contradiction callback, matching the first-crossing hne surface used by the existing scaffold. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIPathCrossingFromSet.lean) |
| anisotropicHeisenbergS_case_ii_crossing_set_contradiction_of_first_crossing / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_first_crossing / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_first_crossing | General spin-S case-(ii) target bridge from a first-crossing contradiction (Tasaki §2.5 Theorem 2.4, Issue #412): non-emptiness of perMCrossingSet M ∩ Icc 0 1 gives the achieved first crossing sInf (perMCrossingSet M ∩ Icc 0 1) by sInf_perMCrossingSet_inter_Icc_mem. Thus a contradiction at that first-crossing point rules out crossing-set non-emptiness, and the target wrappers feed the result to the crossing-set bridge above. The remaining mathematical task is now the first-crossing contradiction callback itself. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIICrossingSetFromFirst.lean) |
| caseIIArgminFirstCrossingContradiction / anisotropicHeisenbergS_case_ii_crossing_contradiction_of_argmin_first_crossing / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_argmin_first_crossing / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_argmin_first_crossing | General spin-S case-(ii) target bridge from the argmin first crossing (Tasaki §2.5 Theorem 2.4, Issue #412): a target crossing at t = 1 gives a non-empty crossing set; exists_M_chosen_argmin_per_M_first_crossing then selects a non-balanced sector whose first crossing minimises sInf (perMCrossingSet M ∩ Icc 0 1) among all non-empty crossing sectors. The named callback caseIIArgminFirstCrossingContradiction only has to contradict this selected argmin sector, with the argmin property available. The target wrappers feed the resulting target crossing contradiction to the crossing-callback bridge. The remaining mathematical task is now the argmin first-crossing contradiction callback itself. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIArgminFirstCrossingCore.lean for the crossing contradiction + Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIArgminFirstCrossing.lean for the case-(ii) target wrappers, split for build speed) |
| caseIIArgminFirstCrossingContradiction_of_first_crossing_finrank_bound / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_first_crossing_finrank_bound / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_first_crossing_finrank_bound | General spin-S case-(ii) argmin first-crossing contradiction from a first-crossing finrank <= 2 bound (Tasaki §2.5 Theorem 2.4, Issue #412): proves the argmin first-crossing callback using the established argmin-to-balanced-ground chain, the crossing equality at the selected sInf, and the embedded two-sector contradiction. The remaining explicit input is a full ground eigenspace finrank <= 2 bound at the selected first-crossing parameter, plus the standard SU(2)-point strict-gap/ground-state inputs and the centered-magnetization nonzero bookkeeping for non-balanced sectors. The target wrappers feed this callback to the argmin-first-crossing bridge above. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIArgminFinrankCore.lean for the argmin first-crossing contradiction + Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIArgminFinrank.lean for the case-(ii) target wrappers, split for build speed) |
| caseII_first_crossing_finrank_bound_of_path_global_finrank_bound / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_path_global_finrank_bound / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_path_global_finrank_bound | General spin-S case-(ii) target bridge from a path-global finrank <= 2 bound (Tasaki §2.5 Theorem 2.4, Issue #412): repackages the selected first-crossing finrank input from the previous row. Since sInf (perMCrossingSet M ∩ Icc 0 1) lies in Icc 0 1, a full ground eigenspace finrank <= 2 bound for every point on the case-(ii) deformation path supplies the exact selected-point input required by the argmin first-crossing finrank bridge. The target wrappers therefore leave the remaining case-(ii) mathematical input as a path-global finrank <= 2 theorem, rather than a selected-sector sInf hypothesis. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIPathGlobalFinrank.lean) |
| caseII_path_global_finrank_bound_of_axisSwapped_submatrix_blocks_le_one / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_axisSwapped_submatrix_blocks_path / aHeisS_case_ii_target_zeroMag_of_axisSwapped_submat_blocks_path | General spin-S case-(ii) target bridge from pathwise axis-swapped parity-block simplicity (Tasaki §2.5 Theorem 2.4, Issue #412): derives the path-global full ground eigenspace finrank <= 2 input from the standard block-sum API. At each path time t ∈ Icc 0 1, the arbitrary-eigenvalue wrapper anisotropicHeisenbergS_eigenspace_finrank_le_two_of_submatrix_blocks_le_one_general is applied with μ equal to the full Hermitian minimum, so two axis-swapped parity-block submatrix finrank <= 1 hypotheses imply the full pathwise finrank <= 2 bound. The target wrappers feed this callback to the path-global bridge above. The remaining case-(ii) mathematical input is now pathwise axis-swapped parity-block submatrix simplicity at the full ground energy. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockPathFinrankCore.lean for the path-global finrank bound + Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockPathFinrank.lean for the case-(ii) target wrappers, split for build speed) |
| axisSwappedParityBlockPFMinAt / axisSwappedParityBlockPFMinPath / axisSwappedParityBlockStrictRawSupportPath / axisSwappedParityBlockLambdaOneRawSupportPath / axisSwappedParityBlockDZeroRawSupportPath / exists_parityBlock_dressed_diag_strict_upper_bound / axisSwappedParityBlockStrictRawSupportPath_of_reachability / axisSwappedParityBlockLambdaOneRawSupportPath_of_reachability / axisSwappedParityBlockDZeroRawSupportPath_of_reachability / axisSwappedAnisotropicHeisenbergS_submatrix_finrank_le_one_at_full_min_of_pf_min / caseII_axisSwapped_submatrix_blocks_path_of_pf_min / axisSwappedAnisotropicHeisenbergS_submatrix_pf_min_path_of_caseII_raw_support / caseII_axisSwapped_parityBlockPFMinPath_of_raw_support / caseII_axisSwapped_submatrix_blocks_path_of_raw_support_pf_min / caseII_axisSwapped_parityBlockPFMinPath_of_reachability / caseII_axisSwapped_submatrix_blocks_path_of_reachability_pf_min / caseII_coupling_eq_zero_of_not_bipartiteCompleteGraph_adj / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_block_pf_min_path / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_block_pf_min_path / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_raw_support_pf_min_path / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_raw_support_pf_min_path / anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_reachability_pf_min_path / anisotropicHeisenbergS_case_ii_target_zero_magnetization_of_reachability_pf_min_path | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| parityReachableSOnBlock_of_parityReachableS / ionParityReachableSOnBlock_of_ionParityReachableS / bondParityReachableSOnBlock_of_bondParityReachableS / parityReachableSOnBlock_total_bipartiteCompleteGraph / ionParityReachableSOnBlock_total_bipartiteCompleteGraph / bondParityReachableSOnBlock_total_bipartiteCompleteGraph / caseII_axisSwapped_parityBlockPFMinPath_of_total_reachability / caseII_axisSwapped_submatrix_blocks_path_of_total_reachability_pf_min | General spin-S case-(ii) block reachability totality bridge (Tasaki §2.5 Theorem 2.4, Issue #412): lifts the existing full-configuration strict, ion-only, and bond-only reachability relations to the fixed parityConfigS block relations by using parity preservation along ReflTransGen paths. The bipartite complete graph totality wrappers then supply the block-level reachability hypotheses from hA_ne, hB_ne, and the spin-size hypotheses (1 <= N for strict and bond-only, 2 <= N for ion-only). The final wrappers feed those totality results into the case-(ii) reachability-level PF/min bridge; the later corner and total-reachability target bridges reuse this layer to close the current 2 <= N case-(ii) endpoint. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockReachabilityCore.lean for the lifts + totality reachability bridge + Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockReachability.lean for the case-(ii) wrappers, split for build speed) |
| axisSwappedParityBlockPFMinAt_of_total_reachability_noncorner / axisSwappedSubmatrix_full_min_finrank_le_one_of_total_reachability_noncorner / caseII_path_global_finrank_bound_of_total_reachability_and_corner / caseII_path_global_finrank_bound_of_total_reachability_and_su2_unique | General spin-S case-(ii) SU(2)-corner bridge (Tasaki §2.5 Theorem 2.4, Issue #412): separates the exact corner (lambda,D)=(1,0) from the non-corner case-(ii) path. Away from the corner, the pointwise selector uses the strict, ion-only, or bond-only raw-support PF/min consumer together with the total reachability bridge; at the corner, the path-global full finrank <= 2 input is supplied directly from a full SU(2)-point ground-eigenspace finrank <= 1 callback. This avoids imposing the stronger and unnecessary assertion that each whole parity block is PF-simple at its own block minimum at the SU(2) point. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIICorner.lean) |
| caseII_path_global_finrank_bound_of_total_reachability_MLM_casimir_ladder_t23_pf / aHeisS_case_ii_target_finrank_le_one_of_totReach_MLM_casLadder_t23_pf / aHeisS_case_ii_target_zeroMag_of_totReach_MLM_casLadder_t23_pf | General spin-S case-(ii) target bridge from total reachability and the MLM/Casimir endpoint (Tasaki §2.5 Theorem 2.4, Issue #412): composes the SU(2)-corner bridge with the path-global target wrappers. The MLM/Casimir/Theorem 2.3 endpoint supplies full SU(2)-point uniqueness; the same uniqueness input is reused for the exact-corner finrank <= 2 branch, for the balanced SU(2) sector/full-ground equality, and for the strict non-balanced sector gap at t = 0. Thus, for 2 <= N, total reachability on the bipartite complete graph now feeds target uniqueness and zero magnetization directly, modulo the standard balanced-sector bookkeeping and Theorem 2.3 endpoint data. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIITotalReachabilityTarget.lean) |
| anisotropicHeisenbergS_tasaki24_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_general / aHeisS_tasaki24_target_zeroMag_of_MLM_casLadder_t23_pf_gen | General spin-S Tasaki Theorem 2.4 parameter-region wrapper (Tasaki §2.5 Theorem 2.4, Issue #412): packages the already proved target endpoints for 2 <= N. The wrapper dispatches -1 < λ < 1, D >= 0 to the D_nonneg case-(i) endpoint; λ = 1, D >= 0 to the explicit SU(2) endpoint when D = 0 and to the lambda_one_D_pos endpoint when D > 0; and λ >= 1, D <= 0 to the case-(ii) total-reachability endpoint. The second theorem applies the packaged uniqueness statement and the existing uniqueness-implies-zero-magnetization theorem, yielding Ŝ^3_tot Φ = 0 for every non-zero target ground state in the covered parameter region. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSTheorem24.lean) |
| axisSwappedParityBlockPFMinAt_of_total_reachability_noncorner_lambda_gt_one / caseII_path_global_finrank_bound_of_total_reachability_and_su2_unique_lambda_gt_one / spinHalf_anisotropicHeisenbergS_case_ii_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf / spinHalf_aHeisS_case_ii_target_zeroMag_of_MLM_casLadder_t23_pf / spinHalf_anisotropicHeisenbergS_tasaki24_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf / spinHalf_aHeisS_tasaki24_target_zeroMag_of_MLM_casLadder_t23_pf | Spin-1/2 Tasaki Theorem 2.4 strict case-(ii) and exact N = 1 parameter-region wrapper (Tasaki §2.5 Theorem 2.4, Issue #412): observes that for a strict case-(ii) target 1 < λ, the linear path from (1,0) has first coordinate 1 only at t = 0. Hence the non-corner path never enters the λ = 1, D < 0 ion-only branch, whose totality requires 2 <= N; strict parity reachability and the D = 0 bond-only branch both need only 1 <= N. The new spin-1/2 target wrappers combine this strict case-(ii) route with the existing D >= 0 case-(i) endpoint and the spin-1/2 λ = 1 scalar-shift endpoint, giving the exact N = 1 region wrapper for -1 < λ < 1, D >= 0; λ = 1; and 1 < λ, D <= 0. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinHalfCaseIICore.lean for the case-(ii) path geometry + Quantum/SpinS/AnisotropicHeisenbergSpinHalfCaseII.lean for the spin-1/2 target wrappers, split for build speed) |
| caseIIParityGaugeSign / caseIIParityGaugeSign_mul_eq_one_of_magSumS_eq / caseIIParityGaugeSign_mul_eq_neg_one_of_magSumS_add_two / caseIIParityGaugeSign_mul_eq_neg_one_of_add_two_magSumS / caseIIParityGaugeDiagonalOnParity_mul_self | General spin-S case-(ii) parity-block gauge sign layer (Tasaki §2.5 Theorem 2.4, Issue #412): introduces the additional parity-block gauge (-1)^(magSumS / 2) needed for the λ >= 1, D <= 0 PF route. On a fixed parity block it agrees with Tasaki’s (-1)^((magSumS - p) / 2) convention up to a constant block sign. The gauge product is 1 when magSumS is preserved and -1 when one configuration has magSumS two larger than the other, so it preserves transverse raise-lower signs while flipping the parity-bond and single-ion ±2 signs. The diagonal gauge squares to the identity and is ready to combine with the Marshall diagonal in the next shifted PF matrix layer. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIParityGauge.lean) |
| caseIIParityGaugeSignReal / caseIIParityGaugeSignReal_mul_self / caseIICombinedGaugeSignOnParity / caseIICombinedGaugeSignOnParity_mul_self / caseIICombinedGaugeDiagonalOnParity / caseIICombinedGaugeDiagonalOnParity_mul_self / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_apply / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_apply_diag / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_isSymm_of_real / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_apply / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_apply_off_diag / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_apply_diag / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_diag_pos / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_isSymm_of_real | General spin-S case-(ii) parity-gauged shifted matrix layer (Tasaki §2.5 Theorem 2.4, Issue #412): combines the extra parity gauge with the Marshall-dressed axis-swapped real matrix on each parity block. The real combined gauge diagonal squares to the identity, the parity-gauged real block matrix has the same diagonal as the dressed matrix and is symmetric for real coupling data, and the shifted matrix c • 1 - R has the expected diagonal/off-diagonal unfoldings plus strict diagonal positivity under a strict shift. The next case-(ii) PF steps are local sign transfer, reachability/irreducibility, and PF/min identification for this shifted matrix. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIParityGaugedMatrix.lean) |
| neg_one_pow_mul_self_real / neg_one_pow_succ_mul_self_real / neg_one_pow_mul_succ_self_real / caseIIParityGaugeSignReal_mul_eq_one_of_magSumS_eq / caseIIParityGaugeSignReal_mul_eq_neg_one_of_magSumS_add_two / caseIIParityGaugeSignReal_mul_eq_neg_one_of_add_two_magSumS / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_eq_of_magSumS_eq / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_eq_neg_of_magSumS_add_two / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_eq_neg_of_add_two_magSumS / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_nonpos_of_magSumS_eq / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_nonpos_of_magSumS_add_two / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_nonpos_of_add_two_magSumS / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_nonneg / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_gauged_entry_neg / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_magSumS_eq / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_magSumS_add_two / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_add_two_magSumS | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| magSumS_add_local_eq_of_agree_off_site / magSumS_add_local_two_eq_of_agree_off_two_site / singleIonStepS_magSumS_add_two_or_add_two_magSumS / parityBondStepS_magSumS_add_two_or_add_two_magSumS / spinSDotXXZSwap_apply_re_neg_of_parityBondStepS_witness_caseII / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_neg_of_raiseLowerStepS_caseII / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_pos_of_parityBondStepS_caseII / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_pos_of_singleIonStepS_caseII / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_raiseLowerStepS / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_parityBondStepS / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_singleIonStepS | General spin-S case-(ii) local shifted-entry sign layer (Tasaki §2.5 Theorem 2.4, Issue #412): proves the local dressed signs and transfers them to strict positivity of the parity-gauged shifted matrix on the three elementary parity-block moves. Transverse raise/lower moves use the positive (1 + lambda.re) / 4 coefficient and the Marshall sign flip; parity-bond ±2 moves use 1 < lambda.re, the negative (1 - lambda.re) / 4 coefficient, and the extra parity gauge; same-site single-ion ±2 moves use D.re < 0 against the negative (S^2)^2 off-diagonal entry. The remaining case-(ii) shifted-matrix inputs are reachability/irreducibility and PF/min identification. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIILocalSignsCore.lean and Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIILocalSigns.lean) |
| parityStepSOnBlock / parityReachableSOnBlock / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pos_of_parityStepS / shiftedCaseIIParityGaugedAxisSwappedReMatrixOnParityBlock_pow_apply_pos_of_blockReachable / shiftedCaseIIParityGaugedBlock_isIrreducible_of_blockReachable_total | General spin-S case-(ii) shifted block reachability and conditional irreducibility (Tasaki §2.5 Theorem 2.4, Issue #412): lifts the case-(ii) local shifted-entry signs to a block-level PF irreducibility input. The block relation is the reflexive-transitive closure of ParityStepS on parityConfigS; in the strict interior (-1 < lambda.re, 1 < lambda.re, and D.re < 0) every elementary parity step gives a strictly positive shifted block entry. Entrywise non-negativity plus block reachability therefore gives a positive matrix-power entry, and reachability totality plus strict diagonal shift gives Matrix.IsIrreducible. The following support and boundary rows lower its remaining shifted-matrix inputs; the following PF/min row supplies the fixed-block conversion, including the zero-coefficient boundary consumers. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockIrreducible.lean) |
| caseIIParityGaugedBlock_offdiag_nonpos_of_magSum_support / shiftedCaseIIParityGaugedBlock_nonneg_of_magSum_support / shiftedCaseIIParityGaugedBlock_irreducible_of_magSum_support | General spin-S case-(ii) shifted block non-negativity bridge from a magSumS support split (Tasaki §2.5 Theorem 2.4, Issue #412): lowers the explicit entrywise non-negativity hypothesis in the block irreducibility layer to an off-diagonal sign/support decomposition. Equal-magSumS off-diagonal block pairs use dressed non-positivity; target/source magSumS raised by two use dressed non-negativity plus the parity-gauge sign flip; all other off-diagonal block pairs are supplied as zero-support. A diagonal shift bound then gives entrywise non-negativity of the shifted parity-gauged block matrix, and the final wrapper feeds that non-negativity into conditional irreducibility. The following step-support, raw-support, and boundary rows supply the total-Hamiltonian support/sign split; the following PF/min row supplies the fixed-block conversion, including the zero-coefficient boundary consumers. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIBlockNonneg.lean) |
| dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_nonpos_of_raiseLowerStepS_caseII / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_nonneg_of_parityBondStepS_caseII / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_nonneg_of_singleIonStepS_caseII / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_eq_zero_of_dressed_zero / shiftedCaseIIParityGaugedBlock_nonneg_of_step_support / shiftedCaseIIParityGaugedBlock_irreducible_of_step_support | General spin-S case-(ii) shifted block step-support bridge (Tasaki §2.5 Theorem 2.4, Issue #412): turns a step-or-zero support split into the magSumS support/sign hypotheses required by the block non-negativity bridge. Equal-magSumS off-diagonal pairs are supplied by transverse RaiseLowerStepS or zero support; target/source magSumS raised by two are supplied by ParityBondStepS, SingleIonStepS, or zero support. The wrapper reuses the strict local signs as non-positive/non-negative dressed entries, transfers dressed zero support through the parity gauge, and then feeds the result into shifted entrywise non-negativity and conditional irreducibility. The following raw-support and boundary rows supply the raw total-Hamiltonian witness/zero classification and zero-coefficient boundary move-set variants; the following PF/min row supplies the fixed-block conversion, including the lambda = 1 ion-only and D = 0 bond-only consumers. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIStepSupport.lean) |
| singleIonAnisotropyS2_apply_eq_zero_of_not_singleIonStepS / spinSDotXXZSwap_apply_eq_zero_of_not_raiseLowerStepS_not_parityBondStepS / dressedAxisSwappedReMatrix_raiseLower_or_zero_of_magSum_eq / dressedAxisSwappedReMatrix_parity_or_single_or_zero_of_magSum_add_two / dressedAxisSwappedAnisotropicHeisenbergSReMatrix_apply_eq_zero_of_not_magSum_step / shiftedCaseIIParityGaugedBlock_nonneg_of_raw_support / shiftedCaseIIParityGaugedBlock_irreducible_of_raw_support | General spin-S case-(ii) raw total-Hamiltonian support classification (Tasaki §2.5 Theorem 2.4, Issue #412): proves the step-or-zero support split required by the preceding step-support bridge from raw axis-swapped Hamiltonian entries. Under the bipartite support-zero assumption on J, nonzero equal-magSumS off-diagonal entries yield a transverse RaiseLowerStepS; nonzero target/source magSumS changes by two yield a ParityBondStepS or SingleIonStepS; and all other off-diagonal entries vanish. The block wrappers feed this raw classification into shifted entrywise non-negativity and conditional irreducibility. The following boundary row handles zero-coefficient move-set variants, and the following PF/min row supplies the fixed-block conversion for the strict and boundary consumers. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIRawSupportCore.lean for the local/total-entry zero tests singleIonAnisotropyS2_apply_eq_zero_of_not_singleIonStepS / spinSDotXXZSwap_apply_eq_zero_of_not_raiseLowerStepS_not_parityBondStepS + Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIRawSupport.lean for the step-or-zero split and the block-level raw-support wrappers, split for build speed) |
| ionParityStepSOnBlock / ionParityReachableSOnBlock / bondParityStepSOnBlock / bondParityReachableSOnBlock / shiftedCaseIIBlock_pos_of_ion_step_lambda_one / shiftedCaseIIBlock_pos_of_bond_step_D_zero / shiftedCaseIIBlock_pow_pos_of_ion_reachable_lambda_one / shiftedCaseIIBlock_pow_pos_of_bond_reachable_D_zero / spinSDotXXZSwap_apply_eq_zero_of_parityBondStepS_witness_lambda_one / dressedAxisSwappedReMatrix_zero_of_parityBondStep_lambda_one / dressedAxisSwappedReMatrix_single_or_zero_of_magSum_add_two_lambda_one / dressedAxisSwappedReMatrix_single_or_zero_of_add_two_magSum_lambda_one / dressedAxisSwappedReMatrix_zero_of_singleIonStep_D_zero / dressedAxisSwappedReMatrix_bond_or_zero_of_magSum_add_two_D_zero / dressedAxisSwappedReMatrix_bond_or_zero_of_add_two_magSum_D_zero / shiftedCaseIIBlock_nonneg_of_ion_step_support_lambda_one / shiftedCaseIIBlock_nonneg_of_bond_step_support_D_zero / shiftedCaseIIBlock_nonneg_of_raw_support_lambda_one / shiftedCaseIIBlock_nonneg_of_raw_support_D_zero / shiftedCaseIIBlock_irreducible_of_ion_step_support_lambda_one / shiftedCaseIIBlock_irreducible_of_bond_step_support_D_zero / shiftedCaseIIBlock_irreducible_of_raw_support_lambda_one / shiftedCaseIIBlock_irreducible_of_raw_support_D_zero | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| caseIIParityGaugeSign_eq_ofReal_real / caseIICombinedGaugeDiagonalOnParity_map_eq / caseIICombinedGaugeDiagonalOnParity_map_mul_self / caseIIParityGaugedAxisSwappedReMatrixOnParityBlock_map_eq_combinedGauge_conj_bare / axisSwappedAnisotropicHeisenbergS_submatrix_pf_min_of_caseII_shifted_block / axisSwappedAnisotropicHeisenbergS_submatrix_pf_min_of_caseII_raw_support / axisSwappedAnisotropicHeisenbergS_submatrix_pf_min_of_caseII_raw_support_lambda_one / axisSwappedAnisotropicHeisenbergS_submatrix_pf_min_of_caseII_raw_support_D_zero | General spin-S case-(ii) parity-block PF/min bridge (Tasaki §2.5 Theorem 2.4, Issue #412): converts the shifted case-(ii) parity-gauged real block into the bare axis-swapped complex parity-block PF/min callback. The combined parity/Marshall gauge diagonal is complexified and shown to square to the identity; the complexified parity-gauged block is similar to the bare axis-swapped block. Perron–Frobenius gives a one-dimensional positive eigenspace for the shifted non-negative irreducible real block, the shift changes the eigenvalue from r to c - r, Collatz–Wielandt identifies c - r with the Hermitian minimum, and similarity transfers the finrank <= 1 bound to the bare block. Raw-support consumers cover the strict case-(ii) region, the lambda = 1 ion-only boundary, and the D = 0 bond-only boundary. The remaining pathwise task is to select and supply the appropriate strict or zero-coefficient reachability inputs along the case-(ii) deformation path. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSCaseIIParityBlockPFMin.lean) |
| anisotropicHeisenbergS_target_finrank_le_one_of_strict_gap / anisotropicHeisenbergS_target_groundState_zero_magnetization_of_strict_gap | General spin-S target wrappers from strict sector gap (Tasaki §2.5 Theorem 2.4, Issue #412): composes the existing general-N theorem hermitianMinEigenvalue_balanced_eq_full_of_strict_gap with the balanced-sector PF target wrappers. The remaining target energy input is now the strict gap E_balanced < E_M over every non-balanced non-empty magnetization sector, rather than a direct balanced/full equality hypothesis. The next row supplies that strict-gap callback from SU(2)-endpoint global uniqueness; for case (ii), the adjacent no-full-finrank row removes the full finrank <= 2 input once strict gap is supplied. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSTargetFromStrictGap.lean) |
| anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min_general / anisotropicHeisenbergS_obligation_2_of_SU2_global_unique_only_general / anisotropicHeisenbergS_strict_gap_all_M_of_SU2_global_unique_general / anisotropicHeisenbergS_target_finrank_le_one_of_SU2_global_unique_general / anisotropicHeisenbergS_target_groundState_zero_magnetization_of_SU2_global_unique_general | General spin-S obligation (2) and target wrappers from SU(2) global uniqueness (Tasaki §2.5 Theorem 2.4, Issue #412): lifts the first-crossing deformation capstone from the spin-1/2 boundary to arbitrary spin parameter N. The concrete axisSwapUnitarySSpinS N capstone gives finrank ≤ 2 at the anisotropic global minimum and along the path γ(t). The first-crossing contradiction then turns SU(2)-endpoint full ground eigenspace uniqueness into the strict target sector gap over every non-balanced non-empty sector, and the strict-gap target wrappers give finrank ≤ 1 plus zero total magnetization at the target point. This remains conditional on proving the SU(2)-endpoint global uniqueness input and does not address Tasaki case (ii). Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinSObligation2FromSU2UniqueCore.lean and Quantum/SpinS/AnisotropicHeisenbergSpinSObligation2FromSU2Unique.lean) |
| anisotropicHeisenbergS_SU2_ground_eigenspace_finrank_le_one_of_heisenberg_general / anisotropicHeisenbergS_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_general / anisotropicHeisenbergS_target_zero_magnetization_of_MLM_casimir_ladder_t23_pf_general | General spin-S target endpoint from the MLM/Casimir SU(2) endpoint (Tasaki §2.5 Theorem 2.4, Issue #412): transports the Heisenberg Hermitian-minimum finrank ≤ 1 conclusion produced by exists_t23_commonE_and_heisHamS_fullEig_finrank_le_one_of_casLadder_t23_pf to anisotropicHeisenbergS J 1 0 N, then feeds that SU(2)-point uniqueness into the general spin-S SU(2)-global-uniqueness target wrappers. This removes the abstract SU(2)-endpoint uniqueness callback from the general spin-S strict case-(i) target uniqueness and zero-magnetization boundary. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSMLMEndpoint.lean) |
| aHeisS_target_finrank_le_one_of_MLM_casLadder_t23_pf_lam1_D_zero_gen / aHeisS_target_zeroMag_of_MLM_casLadder_t23_pf_lam1_D_zero_gen | General spin-S case-(i) SU(2)-point target endpoint from the MLM/Casimir SU(2) endpoint (Tasaki §2.5 Theorem 2.4, Issue #412): exposes the direct public wrapper at (λ,D)=(1,0). The proof reuses the Heisenberg-to-anisotropic SU(2) transport already used by the deformation endpoints and needs no parity-block or path argument. Together with the λ = 1, D > 0, 2 ≤ N ion-only route, this closes the advertised general spin-S λ = 1, D ≥ 0 case-(i) boundary; for case (ii), the conditional, strict-gap, and no-full-finrank bridges are recorded in the case-(ii) rows and the strict-gap derivation remains explicit. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSSU2Boundary.lean) |
| anisotropicHeisenbergS_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_D_nonneg_general / aHeisS_target_zeroMag_of_MLM_casLadder_t23_pf_D_nonneg_gen | General spin-S case-(i) D >= 0 target endpoint from the MLM/Casimir SU(2) endpoint (Tasaki §2.5 Theorem 2.4, Issue #412): replaces the strict single-ion parity branch by bond-only parity reachability, giving parity-block irreducibility and the first-crossing/target wrappers under D' >= 0. The final target uniqueness and zero-magnetization statements now cover -1 < λ < 1, D >= 0 for general spin S; the λ = 1 boundary is handled by the adjacent SU(2)-point and ion-only rows, and case (ii) now has conditional, strict-gap, and no-full-finrank bridges recorded in the case-(ii) rows, with the strict-gap derivation still explicit. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinSDNonnegBoundary.lean) |
| IonParityStepS / IonParityReachableS / ionParityReachableS_total / shiftedDressedAxisSwappedReMatrixOnParityBlock_isIrreducible_lambda_one_D_pos | General spin-S case-(i) λ = 1, D > 0 ion-only parity-block irreducibility (Tasaki §2.5 Theorem 2.4, Issue #412): introduces the parity reachability relation generated only by transverse raise/lower steps and single-ion ±2 steps, proves bipartite-complete totality for configurations with the same magSumS parity when 2 ≤ N, and packages shifted dressed parity-block irreducibility at lambda = 1, D.re > 0. This avoids the parity-bond branch, whose coefficient vanishes at lambda = 1, and provides the PF capstone used by the general spin-S λ = 1 target wrappers. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/ParityReachableNoParityBond.lean, Quantum/SpinS/ParityReachableNoParityBondTotal.lean, Quantum/SpinS/DressedAxisSwapIonParityLambdaOne.lean, Quantum/SpinS/DressedAxisSwapIonParityBlockIrreducibleLambdaOne.lean) |
| anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min_lambda_one_D_pos_general / aHeisS_target_finrank_le_one_of_MLM_casLadder_t23_pf_lam1_D_pos_gen / aHeisS_target_zeroMag_of_MLM_casLadder_t23_pf_lam1_D_pos_gen | General spin-S case-(i) λ = 1, D > 0 target endpoint from the MLM/Casimir SU(2) endpoint (Tasaki §2.5 Theorem 2.4, Issue #412): composes the ion-only parity-block Perron-Frobenius capstone with the same first-crossing deformation argument along the path whose first coordinate is constantly 1. The SU(2)-endpoint global uniqueness input is again supplied by the general Theorem 2.3 MLM/Casimir/PF endpoint, giving target uniqueness and zero total magnetization for 2 ≤ N, λ = 1, D > 0. The D = 0 edge is the SU(2) point and remains handled separately. Tasaki, Springer 2020, §2.5 Theorems 2.3–2.4, pp. 42–44 (the anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min_lambda_one_D_pos_general lemma in Quantum/SpinS/AnisotropicHeisenbergSpinSLambdaOneBoundaryCore.lean; the target endpoints in Quantum/SpinS/AnisotropicHeisenbergSpinSLambdaOneBoundary.lean) |
| anisotropicHeisenbergParametricPath (with continuous_anisotropicHeisenbergParametricPath, continuous_anisotropicHeisenbergS_magSector_minEigenvalue_along_parametricPath) | (2-IVT-a)(b) Parametric path + composed sector-min continuity (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3959): the linear path γ(t) := ((1 - t) + t λ', t D') from the SU(2) point (1, 0) to (λ', D'), with continuity in t and the composed continuity of t ↦ hermitianMinEigenvalue (Ĥ_M(γ(t))) on ℝ via PR #3957. Sets up the parametric variable for the IVT crossing argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergParametricPath.lean) |
| anisotropicHeisenbergS_mulVec_magSectorEmbedding | Anisotropic sector → full eigenvector lift via magSectorEmbedding (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3961): a sector eigenvector Φ : magConfigS Λ N M → ℂ of anisotropicHeisenbergS_magSector_submatrix at eigenvalue μ lifts via magSectorEmbedding to a full eigenvector of anisotropicHeisenbergS J λ D N at the same μ. Anisotropic analogue of heisenbergHamiltonianS_mulVec_magSectorEmbedding; proof uses the sector-crossing matrix-element vanishing (PR #3898). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergMagSectorEmbeddingLift.lean) |
| exists_unit_eigenvector_hermitianMinEigenvalue / exists_nonzero_eigenvector_hermitianMinEigenvalue | Eigenvector existence at hermitianMinEigenvalue (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3962): for a Hermitian matrix M, there is a unit (resp. nonzero) eigenvector v with M.mulVec v = (hermitianMinEigenvalue hM : ℂ) • v. Packages Matrix.IsHermitian.mulVec_eigenvectorBasis at the minimising index. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/HermitianMinEigenvalueEigenvector.lean) |
| exists_sectorGround_full_eigenvector_anisotropicHeisenbergS | Sector ground full-eigenvector existence (bridge) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3963): for real-coupling J and real (λ, D), on a non-empty sector M, there exists a nonzero sector vector Φ whose embedding is a full-Hilbert-space eigenvector of Ĥ(λ, D) at the per-sector minimum eigenvalue E_M, with embedding membership in magSubspaceS Λ N (|V|·N/2 − M). Composes PR #3962 (sector eigenvec existence) + PR #3961 (sector → full lift) + magSectorEmbedding_mem_magSubspaceS. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergMagSectorGroundEigenvector.lean) |
| anisotropicHeisenbergS_magSector_minEigenvalue_alongParametricPath (with continuous_...alongParametricPath) | Named parametric per-sector min eigenvalue along path (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3965): abbreviation E_M(γ(t)) := hermitianMinEigenvalue (Ĥ_M(γ(t))) with continuity in t. Engineering helper: collapses the heavy nested expression to a single opaque symbol so downstream conditional capstones stay within whnf heartbeat budget. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergParametricMinEigenvalue.lean) |
| anisotropicHeisenbergS_embedded_two_sector_contradiction_finrank_le_two | Embedded two-sector contradiction at finrank ≤ 2 (magSectorEmbedding-bridge) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3966): given nonzero sector vectors Φ_admis and Φ_nonadmis whose embeddings are both eigenvectors of Ĥ(λ, D) at the same energy μ (with |V|·N/2 - M_admis = 0 and |V|·N/2 - M_nonadmis ≠ 0), an obligation (1) finrank ≤ 2 bound at μ produces False. Wraps PR #3903 (magSubspaceS-level reflection contradiction) in the magSectorEmbedding form needed by the obligation (2) chain. Final algebraic step of the IVT crossing argument modulo (i) strict gap at (1, 0) (deferred) and (ii) obligation (1) bound at the crossing point (axis-swap spectrum-matching bridge needed). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergCrossingContradictionConditional.lean) |
| AxisSwapUnitaryS.anisotropic_axisSwapped_spectrum_real_eq / AxisSwapUnitaryS.hermitianMinEigenvalue_anisotropic_eq_axisSwapped | Axis-swap bridge: hermitianMinEigenvalue Ĥ = hermitianMinEigenvalue Ĥ' (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3968): under the gauge equivalence Ĥ' = U · Ĥ · U⁻¹ (PR #3752), the real spectra of Ĥ and Ĥ' coincide via matrix_similar_spectrum_real_eq; combined with hermitianMinEigenvalue_eq_of_spectrum_eq (PR #3863), the min eigenvalues match. Lets PR #3888’s obligation (1) bound — stated at the axis-swapped Ĥ'’s per-parity min — be transferred to the original Ĥ’s global min. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergAxisSwapMinEigenvalue.lean) |
| hermitianMinEigenvalue_axisSwapped_eq_min_block_mins (with _ge_min_block_mins, _le_parity_block_min) | axisSwap block-min equality: hermitianMinEigenvalue Ĥ' = min(block-0, block-1) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3969): for Ĥ' at real (J, λ, D) with both parity sectors non-empty, the global minimum eigenvalue equals the minimum of the two parity-block min eigenvalues. Proven in two directions via the joint-min ⊥-below lemma + block-sum finrank ≥ 1 ⟺ HasEigenvalue. Combined with PR #3968, transfers the obligation (1) bound from axis-swapped per-parity to the original Ĥ’s global min. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AxisSwappedBlockMinEq.lean) |
| spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min | Spin-1/2 Ĥ eigenspace finrank ≤ 2 at hermitianMinEigenvalue Ĥ (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3970): combines PR #3888’s obligation (1) bound at the axis-swap block-min energy with the energy-identification bridges (PRs #3968 + #3969). Yields the form needed by the obligation (2) IVT crossing argument: at the crossing point’s global min energy, the eigenspace has ≤ 2 eigenvectors, contradicting the ≥ 3 forced by the M ↔ -M reflection. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergGlobalMinFinrankLeTwo.lean) |
| anisotropicHeisenbergS_parametric_gap_crossing_generic | Generic-M_0 IVT crossing for the parametric gap (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3971): generalisation of PR #3959’s IVT crossing (specialised to M_0 = 0) to an arbitrary ground sector M_0. Needed by the actual Tasaki §2.5 Theorem 2.4 application with M_0 = balanced = |Λ|·N/2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergParametricGapCrossingGeneric.lean) |
| anisotropicHeisenbergParametricPath_in_strict_region (with _fst_lt_one, _neg_one_lt_fst, _snd_pos) | Parametric path stays in strict obligation (1) region for t ∈ (0, 1] (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3975): for target (λ', D') in strict region (i) (-1 < λ' < 1, D' > 0), the path γ(t) = ((1-t) + t·λ', t·D') satisfies the strict obligation (1) hypotheses for every t ∈ (0, 1]. At t = 0 the path is at the SU(2) point (1, 0) itself, which violates strict obligation (1) — expected since obligation (1) is the punctured region. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergParametricPathStaysInRegion.lean) |
| spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min_path | Spin-1/2 Ĥ(γ(t)) eigenspace finrank ≤ 2 at global min for t ∈ (0, 1] (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3976): parametric-path version of PR #3970, applying the spin-1/2 obligation (1) bound at each path point γ(t). Composes PR #3970 with PR #3975 (path stays in strict region). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfFinrankLeTwoAtPath.lean) |
| anisotropicHeisenbergS_crossing_dual_sector_ground_eigenvectors_explicit | Explicit-μ dual sector ground at IVT crossing (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3977): variant of PR #3972 whose conclusion replaces the inner ∃ μ : ℝ with the explicit value hermitianMinEigenvalue (Ĥ_M_0(γ(t*))). Eliminates the opaque-existential-μ issue, enabling clean downstream chaining with the spin-1/2 finrank-≤-2 brick. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergCrossingDualSectorGroundExplicit.lean) |
| continuous_anisotropicHeisenbergS_full_minEigenvalue_real (with _alongParametricPath, anisotropicHeisenbergS_full_isHermitian_real) | Full-Ĥ hermitianMinEigenvalue continuous in (λ, D) and along path (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3982): parallel of PR #3957 (sector min continuity), applied to the FULL Ĥ. Input for the first-crossing argument’s sup analysis: t ↦ global Ĥ min energy must be continuous. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergFullMinEigenvalueContinuous.lean) |
| balancedGSSet / isClosed_balancedGSSet | Balanced-GS set is closed in ℝ (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3983): defines balancedGSSet := { t | E_M_balanced(γ(t)) = global Ĥ min(γ(t)) } and proves it closed (preimage of diagonal in ℝ × ℝ under continuous map). Building block for the first-crossing argument’s sup analysis. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedGSSetClosed.lean) |
| hermitianMinEigenvalue_anisotropicHeisenbergS_full_le_sector | Global Ĥ min ≤ each sector min (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3984): sector ground full-eigenvector (PR #3963) → eigenvalue in spectrum → hermitian_min_eigenvalue_le. Easy direction of the global-min-over-sector-mins identity. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergFullMinLeSectorMin.lean) |
| zero_mem_balancedGSSet_of_strict_GS_at_SU2 (with _inter_Icc) | 0 ∈ balancedGSSet (∩ Icc 0 1) from strict-GS axiom at (1, 0) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3986): non-emptiness witness for PR #3985’s sup analysis; supplies the first-crossing argument’s non-emptiness hypothesis. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedGSSetZeroMem.lean) |
| anisotropicHeisenbergS_magSector_submatrix_mulVec_magSectorRestriction_of_full_eigen | Anisotropic sector inverse lift: full → sector eigenvector restriction (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3988): a full-Ĥ eigvec Ψ at energy μ restricts to a sector-M eigvec at the same μ. Anisotropic analog of the Heisenberg version in MagSectorEmbedding.lean. Used by the first-crossing argument’s hard direction. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergMagSectorInverseLift.lean) |
| exists_sector_hermitianMinEigenvalue_le_full (with exists_magSectorRestriction_ne_zero) | Global Ĥ min ≥ some sector min (block-min identity hard direction) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3989): there is a non-empty sector M with hermitianMinEigenvalue Ĥ_M ≤ hermitianMinEigenvalue Ĥ. Combined with PR #3984’s easy direction, gives existence of M with sector-M min = global Ĥ min. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergFullMinGeSectorMin.lean) |
| hermitianMinEigenvalue_balanced_eq_full_of_strict_gap | Balanced sector IS the GS at (λ, D) from strict gap (discharges 1 of 2 axioms at single point) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3990): under E_M_balanced(λ, D) < E_M(λ, D) for M ≠ M_balanced (non-empty), hermitianMinEigenvalue Ĥ_M_balanced(λ, D) = hermitianMinEigenvalue Ĥ(λ, D). Discharges the strict-GS axiom at any specific (λ, D) from the strict-gap axiom there. Combined with the first-crossing scaffolding (PRs #3982-#3986), reduces the obligation (2) capstone’s first-crossing axiom to the strict-gap axiom at the SU(2) point alone (the latter still requires SU(2) Casimir-based MLM ordering). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedIsGSAtSU2.lean) |
| perMCrossingSet / isClosed_perMCrossingSet | Per-M crossing set is closed in ℝ (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3993): { t | E_M(γ(t)) ≤ E_balanced(γ(t)) } is closed (preimage of Iic 0 under continuous gap). Building block for per-M first crossing inf extraction. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergPerMCrossingSet.lean) |
| sInf_perMCrossingSet_inter_Icc_mem (with isClosed_perMCrossingSet_inter_Icc, bddBelow_perMCrossingSet_inter_Icc) | sInf (perMCrossingSet ∩ Icc 0 1) ∈ set (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3994): closed + bounded below + non-empty → IsClosed.csInf_mem. The per-M first crossing t_first_M is achieved in the set. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergPerMCrossingSInfMem.lean) |
| strict_per_M_gap_of_lt_sInf_perMCrossingSet | Strict per-M gap holds below first crossing (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3995): for t < sInf (perMCrossingSet M ∩ Icc 0 1), E_balanced(γ(t)) < E_M(γ(t)). Direct contrapositive of inf definition; the per-M analog of “strict gap holds before the M-crossing”. Combined with PR #3990, gives balanced IS GS at γ(t) for t < t_first_M. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergPerMStrictGapBelowFirstCrossing.lean) |
| balanced_GS_at_first_crossing_of_argmin | Balanced IS GS at γ(t_first) via closure of Ico (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3997): closure of Ico 0 t_first ⊆ balancedGSSet (closed) gives t_first ∈ Icc 0 t_first = closure ⊆ balancedGSSet. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedGSAtMinFirstCrossing.lean) |
| anisotropicHeisenbergS_per_M_crossing_equality_at_sInf | Per-M crossing equality at sInf (continuity) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3998): E_M(γ(sInf)) = E_balanced(γ(sInf)). Uses closure of { t | f ≤ g } and Ico 0 sInf ⊆ this set; t_first = 0 case ruled out by strict gap at (1, 0). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergPerMCrossingEqualityAtSInf.lean) |
| balanced_min_eq_full_at_sInf | E_balanced(γ(sInf)) = global Ĥ min(γ(sInf)) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #3999): composes PR #3997 with balancedGSSet def to unpack the membership into the explicit energy equality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedMinEqFullAtSInf.lean) |
| balanced_GS_below_sInf_of_argmin | Balanced IS GS below sInf from argmin (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4002): under argmin + strict-gap-at-t’ hypotheses, t' < sInf M_chosen ⟹ t' ∈ balancedGSSet. Intermediate bridge between argmin packaging and balanced-GS conclusion. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedBelowFromArgmin.lean) |
| strict_gap_all_M_below_sInf_of_argmin | Strict gap for all M' at t' < sInf M_chosen (case split) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4003): case-splits on whether perMCrossingSet M' ∩ Icc 0 1 is non-empty (argmin gives sInf M_chosen ≤ sInf M') or empty (no t ∈ Icc 0 1 has E_M' ≤ E_balanced). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergStrictGapAllMFromArgmin.lean) |
| anisotropicHeisenbergS_magSector_minEigenvalue_alongParametricPath_total (with _eq) | Total parametric per-sector min eigenvalue (with empty fallback) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4006): returns the named def value on non-empty sectors, 0 otherwise (no [Nonempty] typeclass required). Engineering prep for Finset-iteration arguments. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergParametricMinEigenvalueTotal.lean) |
| exists_M_chosen_argmin_per_M_first_crossing (with perMCrossingSet_total, perMCrossingSet_total_eq_perMCrossingSet) | Argmin extraction via Finset.exists_min_image (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4007): from any violation M_orig (≠ M_balanced, non-empty crossing set), extracts M_chosen minimising sInf perMCrossingSet over all valid M. Uses the total version (PR #4006) to handle [Nonempty] gating in the Finset filter, plus classical decidability + Finset.exists_min_image. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergArgminExtraction.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_axiomatic_sup_crossing_hne | Capstone v3’ takes hne directly (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4009): variant of PR #4001’s capstone v3 parameterised by non-emptiness hypothesis hne instead of deriving from h_violation at γ(1). Enables composition with argmin extraction (PR #4007), where M_chosen has a non-empty crossing set but the crossing may be at any t' ∈ [0, 1]. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2AxiomaticV3Hne.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_final | ★★★ FINAL CAPSTONE: Spin-1/2 Tasaki §2.5 Theorem 2.4 obligation (2) reduced to 2 axioms (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4010): complete composed capstone via argmin extraction (PR #4007) + below-from-argmin (PR #4002) + strict-gap-all-M (PR #4003) + capstone v3’ hne (PR #4009). Two explicit axioms remain: (1) strict gap at (1, 0) path-wide for all M ≠ M_balanced, (2) strict-GS at (1, 0) (derivable from (1) via PR #3990 — mathematically a single axiom). The remaining work for unconditional Tasaki §2.5 Theorem 2.4 spin-1/2 is to formalise the SU(2) Casimir-based MLM strict gap at (1, 0). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2AxiomaticFinal.lean) |
| strict_GS_at_path_zero_from_strict_gap_at_SU2 | Strict-GS at (1, 0) from strict-gap axiom (axiom 2 from axiom 1) (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4013): under strict gap at (1, 0) for all M ≠ M_balanced, balanced IS GS at (1, 0) via PR #3990 at γ(0) = (1, 0). Discharges axiom 2 of capstone v5 from axiom 1. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergStrictGSAtSU2FromStrictGap.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_single_axiom | ★★★★ ULTIMATE CAPSTONE: spin-1/2 obligation (2) reduced to a SINGLE axiom (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4014): composes PR #4010 (2-axiom final) with PR #4013 (axiom 2 from axiom 1). ★ THE ONLY remaining axiom: strict gap at (1, 0) for all M ≠ M_balanced (the SU(2) Casimir-based MLM ordering for bipartite isotropic Heisenberg AFM with |A| = |B|). Removing this single axiom — by formalising the classical MLM theorem — yields unconditional Tasaki §2.5 Theorem 2.4 spin-1/2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44; Marshall (1955); Lieb-Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2SingleAxiom.lean) |
| strict_gap_at_SU2_of_global_unique (with strict_gap_at_path_zero_of_global_unique) | Strict gap at (1, 0) from SU(2) global uniqueness (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4018): if the full SU(2)-point ground eigenspace has finrank ≤ 1, the balanced sector attains the full minimum, and non-balanced sectors have non-zero centered magnetization, then E_balanced(1,0) < E_M(1,0). Uses the sector-ground full eigenvector construction plus the existing two-sector/reflection finrank ≤ 2 contradiction. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergStrictGapFromGlobalUniqueness.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_of_SU2_global_unique | Spin-1/2 obligation (2) from SU(2) global uniqueness (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4018): derives the strict-gap axiom required by the single-axiom capstone from SU(2) global ground-state uniqueness plus balanced-sector GS equality, then applies spinHalf_anisotropicHeisenbergS_obligation_2_single_axiom. The remaining mathematical target is now the SU(2) uniqueness/balanced-GS input from the MLM/Casimir chain. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2SU2Unique.lean) |
| hermitianMinEigenvalue_balanced_eq_full_at_SU2_of_global_unique | Balanced SU(2) sector attains the full ground energy from global uniqueness (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4019): a full ground eigenvector at (1,0) has zero Ŝ^3_tot magnetization by global uniqueness, so if M_balanced has zero centered magnetization its sector restriction is a nonzero sector eigenvector at the full minimum. This gives E_balanced(1,0) ≤ E_full(1,0), while the existing full-min lower bound gives the reverse inequality. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergBalancedFromGlobalUniqueness.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_of_SU2_global_unique_only | Spin-1/2 obligation (2) from only SU(2) global uniqueness (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4019): composes hermitianMinEigenvalue_balanced_eq_full_at_SU2_of_global_unique with the PR #4018 capstone, removing the separate balanced-sector equality hypothesis. The remaining mathematical target is now the full SU(2)-point ground eigenspace finrank ≤ 1 from the MLM/Perron-Frobenius and Casimir chain. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2SU2UniqueOnly.lean) |
| tasaki23GroundStateSectors_mem_iff_eq_of_card_eq / tasaki23GroundStateSectors_eq_singleton_of_card_eq / tasaki23PredictedTotalSpin_eq_zero_of_card_eq / tasaki23PredictedCasimirValue_eq_zero_of_card_eq / tasaki23_sector_lift_and_casimir_zero_of_card_eq / hermitianMinEigenvalue_eq_common_of_eigenvector_and_global_lower / exists_tasaki23_common_energy_eq_hermitianMinEigenvalue / heisenbergHamiltonianS_full_eigenspace_finrank_le_one_of_sector_support / heisenbergHamiltonianS_full_eigenspace_finrank_le_one_of_outside_projection_zero / heisenbergHamiltonianS_outside_projection_zero_of_strict_sector_lower / heisenbergHamiltonianS_full_eigenspace_finrank_le_one_of_strict_sector_lower / exists_tasaki23_common_energy_and_heisenbergHamiltonianS_full_eigenspace_finrank_le_one | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| heisenbergHamiltonianS_totalSpinSSquared_mulVec_eq_zero_of_sector_pf_zero_casimir | Zero-Casimir transfer along a one-dimensional sector ground line (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4021): if the full Heisenberg μ-eigenspace restricted to a sector has finrank ≤ 1 and contains a non-zero sector-supported vector with total-Casimir image 0, then every sector-supported full eigenvector at the same μ also has total-Casimir image 0. This is the equality-case bridge needed for the MLM/Casimir strict outside-sector proof: once the outside-sector ladder lands in the singleton balanced sector at the common energy, sector PF simplicity pins the landed vector to the zero-Casimir balanced PF line. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (foundational lemmas in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLMCoreSectors.lean; packaged endpoints in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean) |
| heisenbergHamiltonianS_totalSpinSSquared_mulVec_lower_landed_eq_zero_of_sector_pf / heisenbergHamiltonianS_totalSpinSSquared_mulVec_raise_landed_eq_zero_of_sector_pf | Lowering/raising landed-vector zero-Casimir bridges (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4022): if the inward total-ladder iterate from a non-zero full Heisenberg eigenvector reaches a sector whose μ-eigenspace is pinned by sector PF simplicity to a non-zero zero-Casimir vector, then the landed vector is non-zero and has total-Casimir image 0. These are the exact left/right equality-case inputs for the remaining strict outside-sector proof after tasaki23_general_hOutside moves a non-admissible sector eigenvector into the singleton balanced sector. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (foundational lemmas in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLMCoreSectors.lean; packaged endpoints in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean) |
| totalSpinSOpPlus_mulVec_eq_zero_of_totalSpinSSquared_mulVec_eq_zero_of_mem_zero_magSubspaceS / totSpinSOpMinus_mulVecZero_of_totSpinS2_mulVecZero_of_mem_zero_magSubS / not_exists_totalSpinSOpMinus_image_of_zero_casimir_zero_magSubspaceS / not_exists_totalSpinSOpPlus_image_of_zero_casimir_zero_magSubspaceS / not_totalSpinSOpMinus_pow_mulVec_ne_zero_of_zero_casimir_zero_magSubspaceS / not_totalSpinSOpPlus_pow_mulVec_ne_zero_of_zero_casimir_zero_magSubspaceS | Zero-Casimir singlet image obstruction for total ladders (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4023): a zero-total-Casimir vector in the zero magnetization sector is killed by both total ladder operators. Since a non-zero vector in range Ŝ^-_tot cannot also lie in ker Ŝ^+_tot (and similarly with signs reversed), no positive total-lowering or total-raising iterate can land as a non-zero zero-Casimir vector in the zero magnetization sector. This is the representation-theoretic contradiction consumed after PR #4022 pins an outside-sector landed vector to the balanced zero-Casimir line. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (foundational lemmas in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLMCoreSectors.lean; packaged endpoints in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean) |
| tasaki23_strict_hOutside_of_card_eq_zero_casimir_ladder_obstruction | Strict outside-sector ordering from the zero-Casimir total-ladder obstruction (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4024): strengthens the Theorem 2.3 non-admissible-sector lower bound μ ≤ μ_M to μ < μ_M in the balanced |A| = |¬A| case. If equality held, the outside-sector eigenvector would lift to a full eigenvector at μ, a positive total-lowering/raising iterate would land in the singleton balanced sector, PR #4022 would pin that landed vector to zero total Casimir, and PR #4023 would forbid it as a non-zero positive-step ladder image in the zero magnetization sector. This is the strict outside-sector callback needed by the PR #4020 full SU(2) uniqueness endpoint. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (foundational lemmas in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLMCoreSectors.lean; packaged endpoints in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean) |
| exists_t23_commonE_and_heisHamS_fullEig_finrank_le_one_of_casLadder | SU(2)-endpoint global-uniqueness bridge with strict outside ordering discharged (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4025): composes the PR #4020 endpoint with the PR #4024 strict outside-sector theorem. The structural Theorem 2.3 data provide the common energy and balanced PF vector; the balanced PF/Casimir lift makes that vector a non-zero zero-Casimir full eigenvector; PR #4024 constructs the strict outside-sector callback from the zero-Casimir total-ladder obstruction; and the endpoint concludes full SU(2)-point ground eigenspace finrank ≤ 1. The remaining callback is balanced-sector PF simplicity at the common Hermitian minimum. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (foundational lemmas in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLMCore.lean; packaged endpoints in Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_of_MLM_casimir_ladder | Spin-1/2 obligation (2) from the MLM/Casimir SU(2) endpoint (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4026): composes the PR #4025 Heisenberg SU(2)-endpoint uniqueness theorem with spinHalf_anisotropicHeisenbergS_obligation_2_of_SU2_global_unique_only. The proof transports the Heisenberg Hermitian-minimum finrank ≤ 1 bound to anisotropicHeisenbergS J 1 0 1 via the SU(2)-point reduction anisotropicHeisenbergS_one_zero, then invokes the existing deformation contradiction. This removes the abstract full-SU(2)-point uniqueness input from the spin-half obligation boundary; the remaining callback is balanced-sector PF simplicity at the Theorem 2.3 common Hermitian minimum. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2FromMLM.lean) |
← Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) · Catalogue · Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) →