Covariance-product decomposition over R-324 collapse blocks

The successive primitive reductions in paper §4.2 use pairwise-disjoint closed blocks. This file provides the exact algebraic bridge between the ambient doubled covariance product and the standard, increasingly reindexed primitive covariance product on each block.

No estimate is used here: all statements are finite-product identities.

noncomputable def Anderson4D.pairingCovarianceProductOn {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (v : Fin n → T4) : ℝ

The covariance product whose lower endpoints lie in an ambient block. The strict inequality already excludes fixed points, so no separate pairSupport filter is needed.

Equations

• Anderson4D.pairingCovarianceProductOn ρ ε κ B v = ∏ i ∈ B with i < κ i, ρ.etaEpsT4 ε (v i - v (κ i))

theorem Anderson4D.pairingCovarianceProductOn_empty {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε κ ∅ v = 1

theorem Anderson4D.pairingCovarianceProductOn_union {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (A B : Finset (Fin n)) (hAB : Disjoint A B) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε κ (A ∪ B) v = pairingCovarianceProductOn ρ ε κ A v * pairingCovarianceProductOn ρ ε κ B v

A covariance product over a disjoint union is the product of the two block products.

theorem Anderson4D.disjoint_finsetUnionList_of_forall_mem {α : Type u_1} [DecidableEq α] (A : Finset α) (blocks : List (Finset α)) (hA : ∀ B ∈ blocks, Disjoint A B) : Disjoint A (finsetUnionList blocks)

A block disjoint from every member of a list is disjoint from their finite union.

theorem Anderson4D.pairingCovarianceProductOn_finsetUnionList {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (blocks : List (Finset (Fin n))) (hblocks : List.Pairwise Disjoint blocks) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε κ (finsetUnionList blocks) v = (List.map (fun (B : Finset (Fin n)) => pairingCovarianceProductOn ρ ε κ B v) blocks).prod

Exact multiplicative decomposition over a pairwise-disjoint block list.

theorem Anderson4D.pairingCovarianceProductOn_univ (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))) (v : Fin (2 * q) → T4) : pairingCovarianceProductOn ρ ε κ Finset.univ v = primitiveCovarianceProduct ρ ε q κ v

On the whole carrier, the block product is exactly the covariance product used in Proposition 4.1.

theorem Anderson4D.pairingCovarianceProductOn_eq_residualPrimitiveBlock {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε κ B v = primitiveCovarianceProduct ρ ε (residualBlockOrder B) (residualPrimitiveBlockPairing κ B hB) fun (i : Fin (2 * residualBlockOrder B)) => v ↑((residualPrimitiveBlockOrderIso κ B hB) i)

Restricting a covariance product to a certified closed block and increasingly reindexing that block gives the standard primitive covariance product at the exact half-cardinality order.

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

The residual doubled covariance product is exactly the product of its canonical R-324 residual block factors. Each factor is identified with a standard primitive covariance product by pairingCovarianceProductOn_eq_residualPrimitiveBlock.

Removing analytically vacuous empty residual blocks

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

Empty shells contribute the multiplicative identity and must not be sent to Proposition 4.1, whose primitive order starts at one.

Equations

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

@[simp]

theorem Anderson4D.mem_nonemptyMomentResidualCollapseBlocks {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin (2 * m))} : B ∈ nonemptyMomentResidualCollapseBlocks κp κm π ↔ B ∈ momentResidualCollapseBlocks κp κm π ∧ B.Nonempty

theorem Anderson4D.finsetUnionList_filter_nonempty {α : Type u_1} [DecidableEq α] (blocks : List (Finset α)) : finsetUnionList (List.filter (fun (B : Finset α) => decide B.Nonempty) blocks) = finsetUnionList blocks

Filtering empty blocks does not change their union.

theorem Anderson4D.prod_pairingCovarianceProductOn_filter_nonempty {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin n)) (blocks : List (Finset (Fin n))) (v : Fin n → T4) : (List.map (fun (B : Finset (Fin n)) => pairingCovarianceProductOn ρ ε κ B v) (List.filter (fun (B : Finset (Fin n)) => decide B.Nonempty) blocks)).prod = (List.map (fun (B : Finset (Fin n)) => pairingCovarianceProductOn ρ ε κ B v) blocks).prod

Filtering empty blocks does not change their covariance-product factorization.

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

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

theorem Anderson4D.one_le_residualBlockOrder_of_nonempty {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hne : B.Nonempty) : 1 ≤ residualBlockOrder B

Every nonempty fully-paired block has positive half-cardinality order, as required by Proposition 4.1.

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