Complete primitive closed partitions

The block collapses in paper Sections 4.1--4.2 use the same finite combinatorial object: a list of nonempty, pairwise-disjoint, closed primitive blocks which covers the ambient carrier. This file packages exactly those properties, independently of any particular R-322 or R-324 construction.

The package is the input to the multiplicity-free product reindexing of a fixed pairing fibre. Its elementary consequences below make the two bookkeeping points explicit: the ambient pairing is full, and the sum of the half-cardinalities of the blocks is exactly half the ambient cardinality.

structure Anderson4D.PrimitiveBlockPartition {n : ℕ} (κ : PartialPairing (Fin n)) : Type

A complete primitive closed block partition for one ambient pairing.

• blocks : List (Finset (Fin n))
• pairwise_disjoint : List.Pairwise Disjoint self.blocks
• cover : finsetUnionList self.blocks = Finset.univ
• nonempty : List.Forall Finset.Nonempty self.blocks
• fullyPaired : List.Forall (IsFullyPairedOn κ) self.blocks
• primitive : List.Forall (IsRelPrimitiveOn κ) self.blocks

theorem Anderson4D.PrimitiveBlockPartition.block_nonempty {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {B : Finset (Fin n)} (hB : B ∈ P.blocks) : B.Nonempty

theorem Anderson4D.PrimitiveBlockPartition.block_fullyPaired {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {B : Finset (Fin n)} (hB : B ∈ P.blocks) : IsFullyPairedOn κ B

theorem Anderson4D.PrimitiveBlockPartition.block_primitive {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {B : Finset (Fin n)} (hB : B ∈ P.blocks) : IsRelPrimitiveOn κ B

theorem Anderson4D.PrimitiveBlockPartition.exists_block_mem {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (i : Fin n) : ∃ B ∈ P.blocks, i ∈ B

Every ambient index belongs to at least one scheduled block.

theorem Anderson4D.PrimitiveBlockPartition.block_eq_of_mem {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {B C : Finset (Fin n)} (hB : B ∈ P.blocks) (hC : C ∈ P.blocks) {i : Fin n} (hiB : i ∈ B) (hiC : i ∈ C) : B = C

Pairwise disjointness makes the scheduled block containing an index unique.

theorem Anderson4D.PrimitiveBlockPartition.isFull {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : κ.IsFull

A complete partition by fully paired blocks contains no fixed point.

theorem Anderson4D.PrimitiveBlockPartition.one_le_blockOrder {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {B : Finset (Fin n)} (hB : B ∈ P.blocks) : 1 ≤ residualBlockOrder B

Every scheduled block has positive primitive order.

theorem Anderson4D.PrimitiveBlockPartition.sum_blockCards {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : (List.map Finset.card P.blocks).sum = n

The block cardinalities add to the complete ambient cardinality.

theorem Anderson4D.PrimitiveBlockPartition.two_mul_sum_blockOrders {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : 2 * (List.map residualBlockOrder P.blocks).sum = n

Exact global order ledger. This is the generic no-hidden-power form used by both R-322 and R-324.