The R-324 schedule as a complete primitive partition

This file is the thin interface between the concrete left/right/residual schedule of paper Section 4.2 and the generic multiplicity-free block-product engine. All five hypotheses of that engine are discharged by the concrete R-324 ledger.

def Anderson4D.momentPrimitiveBlockPartition {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : PrimitiveBlockPartition (momentCombinedPairing κp κm π)

The complete R-324 primitive schedule, packaged for generic exact block-coordinate reindexing.

Equations

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

@[simp]

theorem Anderson4D.momentPrimitiveBlockPartition_blocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (momentPrimitiveBlockPartition κp κm π).blocks = momentNonemptyPrimitiveBlocks κp κm π

theorem Anderson4D.momentPrimitiveBlockPartition_sum_orders {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (List.map residualBlockOrder (momentPrimitiveBlockPartition κp κm π).blocks).sum = m

The generic order ledger specializes to the exact perturbative order m, rather than merely an upper bound.

theorem Anderson4D.momentPrimitiveBlockPartition_order_le_truncOrder {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) {B : Finset (Fin (2 * m))} (hB : B ∈ (momentPrimitiveBlockPartition κp κm π).blocks) (ε : ℝ) (hm : m ≤ truncOrder ε) : residualBlockOrder B ≤ truncOrder ε

Every block in the packaged R-324 partition is licensed at the global truncation order.