Case split of the residual general peel ledger (orders m ≥ 3)

The single remaining uniform-branch obligation R324GeneralPeelLedgerFromThree demands, for every residual-refined fibre at order m ≥ 3, the bound K^m |log ε|^{m-1} on the summed fibre. This file splits that obligation along the induction strategy of paper Section 4.2:

• pure-cross fibres: every entity of the fibre carries no within-half pair (κ⁺ = κ⁻ = id); the fibre is a permutation sum of cross-covariance products handled by the multi-window estimate;
• mixed fibres: some entity retains a within-half pair, opening a parity/difference gain in that half.

The composition theorem proved here shows the two case ledgers exhaust the residual obligation at one common constant.

The two fibre classes

def Anderson4D.R324LedgerThreeAllCrossEntity {m : ℕ} (e : MomentContraction m) : Prop

An order-m contraction entity with no within-half pair at all: both partial pairings are the identity, so all m covariance legs are cross legs.

Equations

• Anderson4D.R324LedgerThreeAllCrossEntity e = (e.fst = Anderson4D.PartialPairing.id ∧ e.snd.fst = Anderson4D.PartialPairing.id)

def Anderson4D.R324LedgerThreeCrossFibre (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Prop

A residual-refined fibre all of whose entities are pure-cross.

Equations

• Anderson4D.R324LedgerThreeCrossFibre m s r = ∀ e ∈ Anderson4D.momentRefinedContractionFiber m s r, Anderson4D.R324LedgerThreeAllCrossEntity e

The two case ledgers

def Anderson4D.R324LedgerThreeCrossLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Cross-case ledger from order three: the fibre logarithmic bound restricted to pure-cross refined fibres.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.R324LedgerThreeMixedLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Mixed-case ledger from order three: the fibre logarithmic bound restricted to fibres containing an entity with a within-half pair.

Equations

• One or more equations did not get rendered due to their size.

The case ledgers exhaust the residual obligation

theorem Anderson4D.r324LedgerThree_generalPeelLedgerFromThree {ρ : SmoothCutoff} {K₁ K₂ : ℝ} (hK₁ : 0 ≤ K₁) (hK₂ : 0 ≤ K₂) (hcross : R324LedgerThreeCrossLedger ρ K₁) (hmixed : R324LedgerThreeMixedLedger ρ K₂) : R324GeneralPeelLedgerFromThree ρ (max K₁ K₂)

Composition of the two cases. Any pair of case ledgers merges into the full residual general peel ledger at the common constant max K₁ K₂.