Exact order ledger for the R-322 analytic schedule

Sorting the extraction trace by paper order changes neither its block orders nor their sum. This module records that equality, its length consequence, and the proper-prefix/terminal form used by the all-order collapse.

theorem Anderson4D.sum_r322AnalyticSchedule_blockOrders_of_full {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) : (List.map (fun (s : R322ExtractionStep (2 * q)) => residualBlockOrder s.2) (r322AnalyticSchedule κ)).sum = q

The perturbative orders in the paper-sorted analytic schedule add exactly to the ambient order.

theorem Anderson4D.r322AnalyticSchedule_blockOrder_pos {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (s : R322ExtractionStep (2 * q)) (hs : s ∈ r322AnalyticSchedule κ) : 0 < residualBlockOrder s.2

Every scheduled block has positive perturbative order.

theorem Anderson4D.length_r322AnalyticSchedule_le_of_full {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) : (r322AnalyticSchedule κ).length ≤ q

Hence a full analytic schedule has at most one step per unit of ambient perturbative order.

theorem Anderson4D.sum_r322AnalyticSchedule_proper_add_terminal {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hκfull : κ.IsFull) (proper : List (R322ExtractionStep (2 * q))) (terminal : R322ExtractionStep (2 * q)) (hschedule : r322AnalyticSchedule κ = proper ++ [terminal]) : (List.map (fun (s : R322ExtractionStep (2 * q)) => residualBlockOrder s.2) proper).sum + residualBlockOrder terminal.2 = q

In the paper's proper-prefix/terminal decomposition, the proper orders plus the terminal order still add exactly to q.