The terminal carrier of the R-322 analytic schedule

The proper-prefix/terminal decomposition ends with the whole endpoint interval. Relative to the carrier left after the proper prefix, the terminal concrete block is therefore the entire remaining carrier. These identities are the structural terminal case needed by the analytic iteration.

theorem Anderson4D.r322AnalyticTerminal_block_eq_activeCarrier {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (proper : List (R322ExtractionStep (2 * q))) (terminal : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = proper ++ [terminal]) (hterminal : terminal.1 = r322WholeEndpoint q hq) : terminal.2 = r322AnalyticActiveCarrier proper

A scheduled whole-interval step occupies precisely the carrier which remains after its prefix.

theorem Anderson4D.r322AnalyticActiveCarrier_after_terminal_eq_empty {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (proper : List (R322ExtractionStep (2 * q))) (terminal : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = proper ++ [terminal]) (hterminal : terminal.1 = r322WholeEndpoint q hq) : r322AnalyticActiveCarrier (proper ++ [terminal]) = ∅

Processing the terminal whole-interval block exhausts the active carrier.

theorem Anderson4D.exists_r322AnalyticTerminalCarrier_of_isNonSplit {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : IsNonSplit κ) : ∃ (proper : List (R322ExtractionStep (2 * q))) (terminal : R322ExtractionStep (2 * q)), r322AnalyticSchedule κ = proper ++ [terminal] ∧ terminal.1 = r322WholeEndpoint q hq ∧ (∀ s ∈ proper, s.1 ≠ r322WholeEndpoint q hq) ∧ terminal.2 = r322AnalyticActiveCarrier proper ∧ r322AnalyticActiveCarrier (r322AnalyticSchedule κ) = ∅

The terminal block of every non-splitting schedule is exactly its remaining carrier, and the complete schedule removes every vertex.