Complete primitive-block factorization of an R-324 contraction

For one contraction triple, Definition 3.1 first removes primitive blocks inside each copy. The remaining doubled carrier is then partitioned by the canonical residual nested blocks. This file proves that these three block families are disjoint, cover the whole doubled carrier, and factor the full covariance product exactly.

def Anderson4D.momentLeftExtractionBlocks {m : ℕ} (κp : PartialPairing (Fin m)) : List (Finset (Fin (2 * m)))

Definition 3.1 blocks in the left copy of the doubled carrier.

Equations

• Anderson4D.momentLeftExtractionBlocks κp = List.map (fun (B : Finset (Fin m)) => Finset.image Anderson4D.leftMomentIndex B) (Anderson4D.extractionBlocks κp)

def Anderson4D.momentRightExtractionBlocks {m : ℕ} (κm : PartialPairing (Fin m)) : List (Finset (Fin (2 * m)))

Definition 3.1 blocks in the right copy of the doubled carrier.

Equations

• Anderson4D.momentRightExtractionBlocks κm = List.map (fun (B : Finset (Fin m)) => Finset.image Anderson4D.rightMomentIndex B) (Anderson4D.extractionBlocks κm)

def Anderson4D.momentLeftRemoved {m : ℕ} (κp : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Union of all within-left removed blocks.

Equations

• Anderson4D.momentLeftRemoved κp = Anderson4D.finsetUnionList (Anderson4D.momentLeftExtractionBlocks κp)

def Anderson4D.momentRightRemoved {m : ℕ} (κm : PartialPairing (Fin m)) : Finset (Fin (2 * m))

Union of all within-right removed blocks.

Equations

• Anderson4D.momentRightRemoved κm = Anderson4D.finsetUnionList (Anderson4D.momentRightExtractionBlocks κm)

theorem Anderson4D.momentLeftExtractionBlocks_pairwise_disjoint {m : ℕ} (κp : PartialPairing (Fin m)) : List.Pairwise Disjoint (momentLeftExtractionBlocks κp)

theorem Anderson4D.momentRightExtractionBlocks_pairwise_disjoint {m : ℕ} (κm : PartialPairing (Fin m)) : List.Pairwise Disjoint (momentRightExtractionBlocks κm)

theorem Anderson4D.IsRelPrimitiveOn.image_leftMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsRelPrimitiveOn κp B) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (Finset.image leftMomentIndex B)

Relative primitivity is preserved by the order-preserving embedding into the left doubled copy.

theorem Anderson4D.IsRelPrimitiveOn.image_rightMomentIndex {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {B : Finset (Fin m)} (hB : IsRelPrimitiveOn κm B) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (Finset.image rightMomentIndex B)

Relative primitivity is preserved by the order-preserving embedding into the right doubled copy.

theorem Anderson4D.momentLeftExtractionBlock_isFullyPairedOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : IsFullyPairedOn (momentCombinedPairing κp κm π) B

theorem Anderson4D.momentLeftExtractionBlock_isRelPrimitiveOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) B

theorem Anderson4D.momentRightExtractionBlock_isFullyPairedOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : IsFullyPairedOn (momentCombinedPairing κp κm π) B

theorem Anderson4D.momentRightExtractionBlock_isRelPrimitiveOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) B

theorem Anderson4D.momentLeftExtractionBlock_primitivePairing_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentLeftExtractionBlocks κp) : have hfull := ⋯; residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) B hfull ∈ primitiveFullPairings (residualBlockOrder B)

Every within-left collapse block is a genuine standard primitive pairing after increasing reindexing.

theorem Anderson4D.momentRightExtractionBlock_primitivePairing_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentRightExtractionBlocks κm) : have hfull := ⋯; residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) B hfull ∈ primitiveFullPairings (residualBlockOrder B)

Every within-right collapse block is a genuine standard primitive pairing after increasing reindexing.

theorem Anderson4D.disjoint_image_leftMomentIndex_rightMomentIndex {m : ℕ} (A B : Finset (Fin m)) : Disjoint (Finset.image leftMomentIndex A) (Finset.image rightMomentIndex B)

The two doubled halves are disjoint, even after restricting either half to arbitrary finsets.

theorem Anderson4D.image_univ_leftMomentIndex_union_rightMomentIndex (m : ℕ) : Finset.image leftMomentIndex Finset.univ ∪ Finset.image rightMomentIndex Finset.univ = Finset.univ

Every doubled index lies in exactly one of the two canonical copies.

theorem Anderson4D.momentLeftRemoved_union_final {m : ℕ} (κp : PartialPairing (Fin m)) : momentLeftRemoved κp ∪ Finset.image leftMomentIndex (finalActive κp) = Finset.image leftMomentIndex Finset.univ

theorem Anderson4D.momentRightRemoved_union_final {m : ℕ} (κm : PartialPairing (Fin m)) : momentRightRemoved κm ∪ Finset.image rightMomentIndex (finalActive κm) = Finset.image rightMomentIndex Finset.univ

theorem Anderson4D.momentLeftRemoved_disjoint_final {m : ℕ} (κp : PartialPairing (Fin m)) : Disjoint (momentLeftRemoved κp) (Finset.image leftMomentIndex (finalActive κp))

theorem Anderson4D.momentRightRemoved_disjoint_final {m : ℕ} (κm : PartialPairing (Fin m)) : Disjoint (momentRightRemoved κm) (Finset.image rightMomentIndex (finalActive κm))

theorem Anderson4D.momentLeftRemoved_disjoint_rightRemoved {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (momentLeftRemoved κp) (momentRightRemoved κm)

theorem Anderson4D.momentLeftRemoved_disjoint_residual {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (momentLeftRemoved κp) (momentResidualActive κp κm)

theorem Anderson4D.momentRightRemoved_disjoint_residual {m : ℕ} (κp κm : PartialPairing (Fin m)) : Disjoint (momentRightRemoved κm) (momentResidualActive κp κm)

theorem Anderson4D.momentRemoved_union_residual_eq_univ {m : ℕ} (κp κm : PartialPairing (Fin m)) : momentLeftRemoved κp ∪ momentRightRemoved κm ∪ momentResidualActive κp κm = Finset.univ

The left removed region, right removed region, and residual carrier partition the entire doubled carrier.

theorem Anderson4D.primitiveCovarianceProduct_momentCombinedPairing_eq_prod_all_blocks (ρ : 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) (momentLeftExtractionBlocks κp)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) (momentRightExtractionBlocks κm)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) (momentResidualCollapseBlocks κp κm π)).prod

The complete covariance product of one contraction factors into: the within-left Definition 3.1 blocks, the within-right blocks, and the canonical residual nested blocks.

theorem Anderson4D.primitiveCovarianceProduct_momentCombinedPairing_eq_prod_nonempty_blocks (ρ : 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) (momentLeftExtractionBlocks κp)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) (momentRightExtractionBlocks κm)).prod * (List.map (fun (B : Finset (Fin (2 * m))) => pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) B v) (nonemptyMomentResidualCollapseBlocks κp κm π)).prod

Analytic form of the complete factorization, with empty residual shells removed before invoking Proposition 4.1.

noncomputable def Anderson4D.momentContractionPrimitiveBlockProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (e : MomentContraction m) (v : Fin (2 * m) → T4) : ℝ

The complete product of all primitive covariance blocks belonging to one contraction entity.

Equations

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

theorem Anderson4D.primitiveCovarianceProduct_momentContraction_eq_blockProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (e : MomentContraction m) (v : Fin (2 * m) → T4) : primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v = momentContractionPrimitiveBlockProduct ρ ε m e v

theorem Anderson4D.primitiveCovarianceProduct_fullPairing_eq_blockProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }) (v : Fin (2 * m) → T4) : primitiveCovarianceProduct ρ ε m (↑κ) v = momentContractionPrimitiveBlockProduct ρ ε m ((momentContractionEquivFullPairing m).symm κ) v

Full-pairing-indexed form of the complete block factorization.

theorem Anderson4D.norm_momentSignaturePhysicalIntegrand_eq_commonSkeletons_mul_sum_blockProducts (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (x y z w : T4) (v : Fin (2 * m) → T4) : ‖momentSignaturePhysicalIntegrand ρ ε m α β s x y z w v‖ = ‖renormalizedGreenSkeleton e₀.fst (assemble x y fun (i : Fin m) => v (leftMomentIndex i))‖ * ‖renormalizedGreenSkeleton e₀.snd.fst (assemble z w fun (i : Fin m) => v (rightMomentIndex i))‖ * ∑ κ ∈ momentFullPairingFiber m s, momentContractionPrimitiveBlockProduct ρ ε m ((momentContractionEquivFullPairing m).symm κ) v

Exact block-product form of the norm of a fixed-signature physical integrand. Both Green skeletons remain outside the full-pairing sum; every summand inside is now explicitly a product of the left, right, and residual primitive blocks.