The refined full/full versus residual branch dichotomy for R-324

For a realized refined schedule, the two within-half partial pairings have equivalent single carriers. Hence either the representative has a residual single, or both halves are full. Fullness in the second branch depends only on the fixed within-half endpoint signature and therefore propagates to every contraction in the refined fibre.

In the residual branch, the same single witness supplies nonempty active carriers in both completed certified traces. This file records only these exact structural facts; it introduces no analytic estimate.

The representative dichotomy and fibrewise propagation

theorem Anderson4D.r324RefinedScheduleRepresentative_singles_nonempty_or_isFull {m : ℕ} (p : R324RefinedScheduleIndex m) : have e₀ := r324RefinedScheduleRepresentative p; e₀.fst.singles.Nonempty ∨ e₀.fst.IsFull ∧ e₀.snd.fst.IsFull

A refined representative either has a residual single in its left half, or both of its within-half pairings are full.

theorem Anderson4D.r324RefinedContractionFiber_isFull_of_representative_isFull {m : ℕ} (p : R324RefinedScheduleIndex m) (hfull : (r324RefinedScheduleRepresentative p).fst.IsFull ∧ (r324RefinedScheduleRepresentative p).snd.fst.IsFull) {e : MomentContraction m} (he : e ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) : e.fst.IsFull ∧ e.snd.fst.IsFull

If the canonical representative of a refined schedule is full in both halves, then every contraction in that refined fibre is full in both halves. This uses only equality of the fixed within-half endpoint signature.

theorem Anderson4D.r324RefinedSchedule_branchDichotomy {m : ℕ} (p : R324RefinedScheduleIndex m) : (r324RefinedScheduleRepresentative p).fst.singles.Nonempty ∨ ∀ e ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd, e.fst.IsFull ∧ e.snd.fst.IsFull

Fibrewise form of the refined branch split used downstream: either the representative has a residual single, or the whole refined fibre is full/full.

Active-carrier witnesses in the residual branch

theorem Anderson4D.R324TwoHalfTerminalData.active_nonempty_of_refinedScheduleRepresentative_singles_nonempty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} (p : R324RefinedScheduleIndex m) (terminal : R324TwoHalfTerminalData ρ lam ε (r324RefinedScheduleRepresentative p).fst (r324RefinedScheduleRepresentative p).snd.fst) (hsingles : (r324RefinedScheduleRepresentative p).fst.singles.Nonempty) : terminal.left.state.active.Nonempty ∧ terminal.right.state.active.Nonempty

A residual single in the refined representative supplies nonempty active carriers in both completed half traces.

theorem Anderson4D.R324TwoHalfTerminalData.certifiedTraces_active_nonempty_of_refinedScheduleRepresentative {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} (p : R324RefinedScheduleIndex m) {leftRes : R324WithinHalfResidualPrefix ρ lam ε (r324RefinedScheduleRepresentative p).fst} {rightRes : R324WithinHalfResidualPrefix ρ lam ε (r324RefinedScheduleRepresentative p).snd.fst} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightScale) (hsingles : (r324RefinedScheduleRepresentative p).fst.singles.Nonempty) : have terminal := ofCertifiedTraces leftTrace rightTrace; terminal.left.state.active.Nonempty ∧ terminal.right.state.active.Nonempty

Specialization of the active-carrier witnesses to the terminal datum packaged by two certified within-half traces.