The complete primitive-block ledger for R-324

For one doubled contraction, paper Section 4.2 successively removes three families of primitive blocks: the Definition 3.1 blocks in the left copy, the corresponding blocks in the right copy, and the nested residual blocks which cross the central cut. This file packages the three families into a single nonempty block list and proves the exact perturbative-order ledger.

The resulting list is the finite analytic schedule for the constructive R-324 collapse. Its block orders sum to exactly m; in particular no pairing-count or unused coupling power is hidden in the schedule.

def Anderson4D.momentAllPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List (Finset (Fin (2 * m)))

All three canonical primitive-block families, before deleting analytically vacuous empty residual shells.

Equations

• Anderson4D.momentAllPrimitiveBlocks κp κm π = Anderson4D.momentLeftExtractionBlocks κp ++ Anderson4D.momentRightExtractionBlocks κm ++ Anderson4D.momentResidualCollapseBlocks κp κm π

def Anderson4D.momentNonemptyPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List (Finset (Fin (2 * m)))

The actual R-324 analytic schedule. Proposition 4.1 starts at order one, so empty residual shells are removed.

Equations

• Anderson4D.momentNonemptyPrimitiveBlocks κp κm π = List.filter (fun (B : Finset (Fin (2 * m))) => decide B.Nonempty) (Anderson4D.momentAllPrimitiveBlocks κp κm π)

@[simp]

theorem Anderson4D.mem_momentAllPrimitiveBlocks {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin (2 * m))} : B ∈ momentAllPrimitiveBlocks κp κm π ↔ B ∈ momentLeftExtractionBlocks κp ∨ B ∈ momentRightExtractionBlocks κm ∨ B ∈ momentResidualCollapseBlocks κp κm π

@[simp]

theorem Anderson4D.mem_momentNonemptyPrimitiveBlocks {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin (2 * m))} : B ∈ momentNonemptyPrimitiveBlocks κp κm π ↔ (B ∈ momentLeftExtractionBlocks κp ∨ B ∈ momentRightExtractionBlocks κm ∨ B ∈ momentResidualCollapseBlocks κp κm π) ∧ B.Nonempty

theorem Anderson4D.momentLeftExtractionBlock_subset_removed {m : ℕ} {κp : PartialPairing (Fin m)} {B : Finset (Fin (2 * m))} (hB : B ∈ momentLeftExtractionBlocks κp) : B ⊆ momentLeftRemoved κp

A left extraction block lies in the complete left removed region.

theorem Anderson4D.momentRightExtractionBlock_subset_removed {m : ℕ} {κm : PartialPairing (Fin m)} {B : Finset (Fin (2 * m))} (hB : B ∈ momentRightExtractionBlocks κm) : B ⊆ momentRightRemoved κm

A right extraction block lies in the complete right removed region.

theorem Anderson4D.momentResidualCollapseBlock_subset_active {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin (2 * m))} (hB : B ∈ momentResidualCollapseBlocks κp κm π) : B ⊆ momentResidualActive κp κm

A residual collapse block lies in the terminal doubled carrier.

theorem Anderson4D.momentAllPrimitiveBlocks_pairwise_disjoint {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise Disjoint (momentAllPrimitiveBlocks κp κm π)

The three canonical block families are mutually disjoint as well as internally pairwise disjoint.

theorem Anderson4D.momentNonemptyPrimitiveBlocks_pairwise_disjoint {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise Disjoint (momentNonemptyPrimitiveBlocks κp κm π)

theorem Anderson4D.finsetUnionList_append {α : Type u_1} [DecidableEq α] (left right : List (Finset α)) : finsetUnionList (left ++ right) = finsetUnionList left ∪ finsetUnionList right

finsetUnionList sends concatenation to finite-set union.

theorem Anderson4D.finsetUnionList_momentNonemptyPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : finsetUnionList (momentNonemptyPrimitiveBlocks κp κm π) = Finset.univ

The nonempty analytic schedule covers the entire doubled carrier.

theorem Anderson4D.momentAllPrimitiveBlocks_forall_isFullyPairedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsFullyPairedOn (momentCombinedPairing κp κm π)) (momentAllPrimitiveBlocks κp κm π)

Every block in the complete list is closed and fully paired under the doubled contraction pairing.

theorem Anderson4D.momentAllPrimitiveBlocks_forall_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsRelPrimitiveOn (momentCombinedPairing κp κm π)) (momentAllPrimitiveBlocks κp κm π)

Every block in the complete list is relatively primitive on its sparse ordered carrier.

theorem Anderson4D.momentNonemptyPrimitiveBlocks_forall_isFullyPairedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsFullyPairedOn (momentCombinedPairing κp κm π)) (momentNonemptyPrimitiveBlocks κp κm π)

theorem Anderson4D.momentNonemptyPrimitiveBlocks_forall_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsRelPrimitiveOn (momentCombinedPairing κp κm π)) (momentNonemptyPrimitiveBlocks κp κm π)

theorem Anderson4D.momentNonemptyPrimitiveBlocks_forall_nonempty {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall Finset.Nonempty (momentNonemptyPrimitiveBlocks κp κm π)

theorem Anderson4D.one_le_residualBlockOrder_of_mem_momentNonemptyPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentNonemptyPrimitiveBlocks κp κm π) : 1 ≤ residualBlockOrder B

Every analytic block has positive primitive order.

theorem Anderson4D.sum_residualBlockOrder_filter_nonempty {n : ℕ} (blocks : List (Finset (Fin n))) : (List.map residualBlockOrder (List.filter (fun (B : Finset (Fin n)) => decide B.Nonempty) blocks)).sum = (List.map residualBlockOrder blocks).sum

Removing empty blocks does not change the sum of half-cardinality orders.

theorem Anderson4D.sum_card_momentAllPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (List.map Finset.card (momentAllPrimitiveBlocks κp κm π)).sum = 2 * m

The three block families account for every one of the 2m covariance variables.

theorem Anderson4D.two_mul_sum_momentAllPrimitiveBlockOrders {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : 2 * (List.map residualBlockOrder (momentAllPrimitiveBlocks κp κm π)).sum = 2 * m

Exact coupling-power ledger for all blocks before removing empty shells.

theorem Anderson4D.two_mul_sum_momentNonemptyPrimitiveBlockOrders {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : 2 * (List.map residualBlockOrder (momentNonemptyPrimitiveBlocks κp κm π)).sum = 2 * m

Exact coupling-power ledger for the actual nonempty analytic schedule.

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

The half-cardinality orders themselves sum to the perturbative order m.

theorem Anderson4D.residualBlockOrder_le_of_mem_momentNonemptyPrimitiveBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentNonemptyPrimitiveBlocks κp κm π) : residualBlockOrder B ≤ m

Each block order is bounded by the total perturbative order.

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

Consequently a global truncation assumption licenses Proposition 4.1 on every block in the concrete R-324 schedule.

theorem Anderson4D.primitiveCovarianceProduct_momentCombinedPairing_eq_prod_primitiveBlocks (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : primitiveCovarianceProduct ρ ε m (momentCombinedPairing κp κm π) v = (List.map (fun (B : Finset (Fin (2 * m))) => pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) (momentNonemptyPrimitiveBlocks κp κm π)).prod

The complete covariance product is the product over the unified nonempty primitive schedule.