Coordinate form of the R-322 endpoint-fibre integrand

The exact endpoint-fibre product equivalence is now combined with the covariance factorization over concrete extraction blocks. The result is a literal product of complete primitive pairing sums, while the signed Green/difference skeleton remains common to the whole endpoint fibre.

List products versus dependent block products

theorem Anderson4D.List.nodup_of_pairwise_disjoint_of_forall_nonempty {α : Type u_1} [DecidableEq α] (blocks : List (Finset α)) (hpairwise : List.Pairwise Disjoint blocks) (hnonempty : List.Forall Finset.Nonempty blocks) : blocks.Nodup

theorem Anderson4D.list_map_prod_eq_fintype_prod_subtype {α : Type u_1} {M : Type u_2} [DecidableEq α] [CommMonoid M] (blocks : List α) (hnodup : blocks.Nodup) (f : α → M) : (List.map f blocks).prod = ∏ a : { a : α // a ∈ blocks }, f ↑a

theorem Anderson4D.extractionBlocks_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (extractionBlocks κ).Nodup

One arbitrary concrete block coordinate

noncomputable def Anderson4D.extractionBlockPrimitiveCovarianceFactor {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (B : ExtractionBlockIndex κ) (σ : ↥(primitiveFullPairings (residualBlockOrder ↑B))) (x : Fin m → T4) : ℝ

Primitive covariance factor carried by one standard block coordinate.

Equations

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

theorem Anderson4D.pairingCovarianceProductOn_endpointFiber_eq_blockCoordinate {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) (B : ExtractionBlockIndex κ) (x : Fin m → T4) : pairingCovarianceProductOn ρ ε (↑τ) (↑B) x = extractionBlockPrimitiveCovarianceFactor ρ ε κ B (endpointFiberPrimitiveCoordinate κ τ B) x

On every concrete extraction block, the ambient covariance factor is exactly the standard primitive factor selected by the corresponding product coordinate.

Complete covariance product and fibre sum

theorem Anderson4D.primitiveCovarianceProduct_endpointFiber_eq_prod_coordinates (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (τ : ReductionEndpointFiberAt κ) (x : Fin (2 * q) → T4) : primitiveCovarianceProduct ρ ε q (↑τ) x = ∏ B : ExtractionBlockIndex κ, extractionBlockPrimitiveCovarianceFactor ρ ε κ B (endpointFiberPrimitiveCoordinate κ τ B) x

The full covariance product of one endpoint-fibre member is the product of its independent primitive block-coordinate factors.

theorem Anderson4D.sum_endpointFiber_primitiveCovarianceProduct_eq_prod_primitiveSums (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (x : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, primitiveCovarianceProduct ρ ε q (↑τ) x = ∏ B : ExtractionBlockIndex κ, ∑ σ : ↥(primitiveFullPairings (residualBlockOrder ↑B)), extractionBlockPrimitiveCovarianceFactor ρ ε κ B σ x

Summing the complete endpoint fibre separates exactly into the product of the complete primitive pairing sums on its blocks.

theorem Anderson4D.sum_endpointFiber_detJintegrand_eq_skeleton_mul_prod_primitiveSums (ρ : SmoothCutoff) (ε : ℝ) {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (x : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) x = renormalizedJGreenSkeleton κ x * ∏ B : ExtractionBlockIndex κ, ∑ σ : ↥(primitiveFullPairings (residualBlockOrder ↑B)), extractionBlockPrimitiveCovarianceFactor ρ ε κ B σ x

Pointwise endpoint-fibre integrand factorization: the common signed Green skeleton multiplies the exact product of primitive covariance sums.