The full/full half-integrability seam, discharged

Paper: R-324 — §4.2 — the full/full half-integrability seam

R324FullFullRefinedFiberFactorization states its factorization under the named premise DeterministicFullHalfIntegrable, the integrability of one half of (4.18) — the two endpoint characters times the closed deterministic profile — on the flat half carrier T4 × (T4 × (Fin m → T4)).

That premise is not an assumption: integrable_detIntegrand_flat already proves the profile itself integrable there for every 0 < ε ≤ 1, and the characters are unimodular (norm_charT4). This module discharges it, so the full/full branch of the Steps 2--3 dichotomy carries no analytic hypothesis.

theorem Anderson4D.deterministicFullHalfIntegrable_all (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (κ : PartialPairing (Fin m)) : DeterministicFullHalfIntegrable ρ ε m α β κ

The full/full half-integrability seam, discharged.

For every mollification scale 0 < ε ≤ 1, every order, every pair of external modes and every within-half pairing, the half integrand of (4.18) is integrable on its flat carrier. The proof is the fixed-scale recipe in docs/R324_PAPER_PROOF.md: the singular part is the closed deterministic profile, already integrable, and the characters are a bounded measurable factor.

theorem Anderson4D.sum_momentRefinedContractionFiber_eq_fullHalfFiber_mul_of_isFull (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) : ∑ e ∈ momentRefinedContractionFiber m s r, deterministicMomentContractionTerm ρ ε m α β e = (∑ κp : ReductionEndpointFiberAt e₀.fst, deterministicFullHalfIntegral ρ ε m α β ↑κp) * ∑ κm : ReductionEndpointFiberAt e₀.snd.fst, deterministicFullHalfIntegral ρ ε m (-α) (-β) ↑κm

The full/full refined-fibre factorization, with its two analytic premises discharged. This is the branch of r324SinglesDichotomy on which both halves are fully paired, so the contraction carries no cross-copy covariance and the two halves of (4.18) are independent.