Clebsch-Gordan total-spin lower bound for the toy ground state (Tasaki §2.5 Theorem 2.3 core) -- #3658

[phasetr]

Tracked sub-effort of #3658 (and #3542).

Purpose

Discharge the single hard analytical core remaining in the toy-ground-state
predicted-Casimir witness (Issue #3658 PR 4): the angular-momentum total-spin
lower bound

γ_tot ≥ predicted = (s_A − s_B)(s_A − s_B + 1) (WLOG s_A ≥ s_B)

for the toy ground state, equivalently the variational lower bound that no
sector-M state has toy energy below predicted − s_A(s_A+1) − s_B(s_B+1).

The three Casimirs (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² mutually commute, so they are
simultaneously diagonalizable; the joint spectrum obeys the Clebsch–Gordan
constraint |j_A − j_B| ≤ j_tot ≤ j_A + j_B. The lower bound j_tot ≥ |j_A−j_B|
is the missing piece. Chosen approach (user, 2026-05-26): abstract variational
lower bound (not an explicit min-total-spin construction).

What is already in place

• heisenbergToyHamiltonianS_eq_casimir_diff: Ĥ_toy = (Ŝ_tot)²−(Ŝ_A)²−(Ŝ_¬A)².
• heisenbergToyHamiltonianS_mulVec_of_joint_casimir_eigenvector (Add toy energy on a joint Casimir eigenvector -- #3658 #3673): toy
  energy μ = γ_tot − γ_A − γ_B on a joint Casimir eigenvector.
• Casimir spectral max bounds: γ_A ≤ s_A(s_A+1), γ_B ≤ s_B(s_B+1) (Add total-Casimir spectral max bound (Ŝtot)² ≤ s_max(s_max+1) -- #3658 #3662/Add sublattice Casimir spectral max bound -- #3658 #3672).
• Toy ground state is a joint Casimir eigenvector -- #3542 #3657: toy PF GS is Marshall-positive and a joint Casimir eigenvector.
• bipartiteToyGroundStateSubspacePredicted = the predicted joint eigenspace;
  bipartiteToyMinEnergyPredicted = predicted − maxA − maxB (value only — the
  variational lower bound is NOT yet proved).
• γ_tot ≤ predicted is derivable from the upper bounds + a nonempty predicted
  joint eigenspace in sector M; the hard direction is γ_tot ≥ predicted.

Definition of done

• A theorem: every joint eigenvalue triple (γ_tot, γ_A, γ_B) of the three
  commuting Casimirs satisfies the Clebsch–Gordan lower bound, hence the toy GS
  has γ_tot = predicted, γ_A = s_A(s_A+1), γ_B = s_B(s_B+1).
• Fed into Casimir spectral max bound + predicted-spin Marshall-positive witness (final obligation of Tasaki §2.5 Theorem 2.3) -- #3542 #3658 PR 4/5 ⟹ the Pin ground-state Casimir value to predicted via overlap -- #3542 #3656 witness ⟹ tasaki_2_5_theorem_2_3 sorry-free.

Planned PRs (each codex-checked, sorry-free; decomposition WIP)

• Mutual commutativity / simultaneous structure of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)²
  (much may already exist) and the (Ŝ_tot)² = (Ŝ_A)² + (Ŝ_¬A)² + 2 Ŝ_A·Ŝ_¬A
  decomposition.
• Operator/expectation Cauchy–Schwarz for the cross term Ŝ_A·Ŝ_¬A, or the
  lowest-weight argument bounding j_tot from below.
• The total-spin lower bound γ_tot ≥ (s_A−s_B)(s_A−s_B+1) on max-sublattice
  joint eigenvectors; the variational lower bound on Ĥ_toy.
• Toy GS lies in bipartiteToyGroundStateSubspacePredicted; γ_tot = predicted.
• Package as the Pin ground-state Casimir value to predicted via overlap -- #3542 #3656 witness; discharge tasaki_2_5_theorem_2_3.

References

• Tasaki, Physics and Mathematics of Quantum Many-Body Systems, Springer 2020,
  §2.5 Theorem 2.3, p. 42 (eqs. 2.5.10–2.5.12).
• Plan: .self-local/tex/3673-tasaki-2-5-toy-gs-predicted-casimir.tex.

Non-goals

• No explicit Clebsch–Gordan min-total-spin state construction (deferred alternative).
• No per-lemma PRs outside this critical path.

[phasetr]

Key de-risking finding (2026-05-26): the abstract Clebsch–Gordan triangle inequality is likely AVOIDABLE.

The total spin always dominates its z-projection: a (Ŝ_tot)²-eigenvector in a magnetization sector with magnetization m ≥ 0 has γ_tot = j(j+1) with j ≥ m, hence γ_tot ≥ m(m+1). This is the magnetization lower bound, and it reuses the existing highest-weight machinery built in #3661–#3672: raising with Ŝ⁺_tot only increases magnetization, so the highest weight M' reached satisfies M' ≥ m, giving γ_tot = M'(M'+1) ≥ m(m+1).

If the witness is constructed in the extremal magnetization sector m = S_tot = s_A − s_B (i.e. the sector whose magnetization equals the predicted total spin), then:

• lower bound: γ_tot ≥ m(m+1) = (s_A−s_B)(s_A−s_B+1) = predicted (magnetization lower bound, EASY);
• upper bound: γ_tot ≤ predicted (from γ_A ≤ maxA, γ_B ≤ maxB (Add sublattice Casimir spectral max bound -- #3658 #3672) + toy energy formula Add toy energy on a joint Casimir eigenvector -- #3658 #3673 + a nonempty predicted joint eigenspace in that sector);
• ⟹ γ_tot = predicted, with no Clebsch–Gordan triangle inequality.

Revised first PRs:

• Magnetization lower bound γ_tot ≥ m(m+1) (lower-bound companion of totalSpinSSquared_eigenvalue_re_le_sMax; track M' ≥ m through the highest-weight induction).
• Pin the toy GS (extremal sector) total Casimir to predicted via lower+upper bounds + Add toy energy on a joint Casimir eigenvector -- #3658 #3673 + nonempty predicted eigenspace.
• Package as the Pin ground-state Casimir value to predicted via overlap -- #3542 #3656 witness; discharge the final theorem.

This stays within the user-chosen "abstract variational/spectral lower bound" direction (it IS a spectral lower bound), just realized via the magnetization/highest-weight route already in the repo rather than a from-scratch angular-momentum-addition theory.

[phasetr]

Progress (2026-05-26): PRs 1–2 merged; the route is now reduced to a SINGLE construction obligation.

• PR 1 (Add total-Casimir magnetization lower bound -- #3674 #3675) totalSpinSSquared_eigenvalue_re_ge_of_mem_magSubspaceS: the magnetization lower bound (Ŝ_tot)² ≥ m(m+1) (highest-weight machinery, magnetization-tracking).
• PR 2 (Pin toy total Casimir to predicted in the extremal sector -- #3674 #3676) tasaki23_total_casimir_re_eq_predicted_of_bounds: the two-sided squeeze pinning γ_tot.re = predicted in the extremal sector m = |s_A − s_B|, modulo two isolated hypotheses.

The single remaining mathematical obligation is the reference energy bound μ ≤ predicted − s_A(s_A+1) − s_B(s_B+1) (equivalently, via μ = γ_tot − γ_A − γ_B, the upper bound γ_tot ≤ predicted). This is NOT derivable from the bounds already proved — it genuinely requires an independent reference state, i.e. a nonempty predicted joint eigenspace bipartiteToyGroundStateSubspacePredicted in the extremal sector (a member has toy energy exactly predicted − maxA − maxB, and the toy PF GS being the minimum gives μ ≤ that).

Plus the easy/mechanical residuals: the extremal-sector identification M.re = |s_A − s_B| for the toy GS sector, and discharging γ_A ≤ maxA, γ_B ≤ maxB for the toy GS (compose #3657 joint eigenvector + #3672 bound + nonzero embedding).

Next sub-effort (construction): the general-case (|A|,|B| both nonzero) nonemptiness of bipartiteToyGroundStateSubspacePredicted in the extremal sector. Existing infra has only the saturated cardA/cardNotA=0 members + the Ŝ⁻_tot-ladder closure (tasaki23_totalSpinSOpMinus_mulVec_mem_bipartiteToyGroundStateSubspacePredicted). Candidate routes: (a) a Néel/explicit-state Rayleigh-quotient bound on μ via a Hermitian min-eigenvalue ≤ Rayleigh-quotient variational principle (needs that principle); (b) explicit minimal-total-spin state via the §2.4 saturated-ferromagnet sublattice span/ladder machinery. Decompose in .self-local/tex/ before Lean.

[phasetr]

Progress (2026-05-26): PRs 1–4 merged; the pin's discharges are nearly complete.

• PR 1 (Add total-Casimir magnetization lower bound -- #3674 #3675): magnetization lower bound (Ŝ_tot)² ≥ m(m+1).
• PR 2 (Pin toy total Casimir to predicted in the extremal sector -- #3674 #3676): the two-sided squeeze pin γ_tot.re = predicted, modulo hypotheses hA_le, hB_le, hM, hμ.
• PR 3 (Add sublattice Casimir bounds for the toy ground state -- #3674 #3677): tasaki23_toy_groundState_sublattice_casimir_re_le — discharges hA_le (γ_A ≤ s_A(s_A+1)) and hB_le (γ_B ≤ s_B(s_B+1)) for the toy GS.
• PR 4 (Identify the extremal magnetization sector with the predicted total spin -- #3674 #3678): tasaki23_extremal_sector_magnetization_re_eq_predicted — discharges hM (M.re = |s_A − s_B|) for the extremal sector M = min(|A|,|¬A|)·N.

The single remaining mathematical obligation is the reference energy bound hμ: μ ≤ predicted − s_A(s_A+1) − s_B(s_B+1) (≡ γ_tot ≤ predicted). This needs an independent reference state in the predicted joint eigenspace bipartiteToyGroundStateSubspacePredicted in the extremal sector (general |A|,|B| ≠ 0). Existing infra has only saturated cardA/cardNotA=0 nonemptiness + the Ŝ⁻_tot-ladder closure.

Next: construct/prove the general-case reference state. Routes: (a) Néel/explicit-state Rayleigh-quotient bound on the toy PF ground energy via a Hermitian min-eigenvalue ≤ Rayleigh-quotient variational principle; (b) explicit minimal-total-spin state via the §2.4 saturated-ferromagnet sublattice span/ladder machinery. Then: final assembly = pin (#3676) + the discharges (#3677, #3678) + hμ ⟹ toy GS γ_tot = predicted ⟹ #3656 witness ⟹ tasaki_2_5_theorem_2_3.