The full-pairing terminal schedule for the R-324 Step-1 branch

When a within-half pairing is full, its analytic R-322 schedule is nonempty and ends at the unique scheduled block containing the last ambient vertex. The terminal endpoint is therefore the global right endpoint, every preceding step is earlier in paper order, and the terminal block is exactly the carrier left after the preceding collapses. This is the combinatorial schedule package needed by the full/full branch of paper Section 4.2, without a non-splitting hypothesis.

theorem Anderson4D.r322AnalyticActiveCarrier_schedule_eq_empty_of_isFull {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : r322AnalyticActiveCarrier (r322AnalyticSchedule κ) = ∅

A full pairing exhausts the active carrier after its complete analytic schedule.

structure Anderson4D.R324FullPairingTerminalSchedule {m : ℕ} (κ : PartialPairing (Fin m)) : Type

The exact terminal data for one full within-half analytic schedule. Unlike the non-splitting terminal package, the left endpoint is not required to be zero: earlier primitive components may already have been removed.

• proper : List (R322ExtractionStep m)
• terminal : R322ExtractionStep m
• schedule_eq : r322AnalyticSchedule κ = self.proper ++ [self.terminal]
• terminal_right : ↑self.terminal.1.2 = m - 1
• proper_paperEarlier (step : R322ExtractionStep m) : step ∈ self.proper → R322PaperEarlier step.1 self.terminal.1
• terminal_block : self.terminal.2 = r322AnalyticActiveCarrier self.proper
• activeCarrier_schedule_eq_empty : r322AnalyticActiveCarrier (r322AnalyticSchedule κ) = ∅

theorem Anderson4D.R324FullPairingTerminalSchedule.sum_properBlockOrders_add_terminal {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (data : R324FullPairingTerminalSchedule κ) (hκ : κ.IsFull) : (List.map (fun (step : R322ExtractionStep (2 * q)) => residualBlockOrder step.2) data.proper).sum + residualBlockOrder data.terminal.2 = q

On an even ambient carrier, the proper-prefix orders and terminal order retain the exact global perturbative ledger.

theorem Anderson4D.exists_r324FullPairingTerminalSchedule {m : ℕ} (hm : 1 ≤ m) (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : Nonempty (R324FullPairingTerminalSchedule κ)

Every full pairing on a nonempty finite interval has a genuine last analytic step with the exact terminal-carrier properties required in the full/full R-324 branch.