Pointwise primitive-block factorization for R-322

This module separates the two ingredients of a fixed endpoint-signature integrand:

• the signed Green/difference skeleton, which is common to the whole fibre;
• the covariance pairing product, whose first complete primitive coordinate is exposed by the block-complement equivalence.

The statements are pointwise and use an arbitrary active carrier. No integration order or R-322 estimate is hidden here; those are supplied by the subsequent collapse module.

The common signed J skeleton

noncomputable def Anderson4D.renormalizedJGreenSkeleton {n : ℕ} (σ : PartialPairing (Fin n)) (x : Fin n → T4) : ℝ

The Green and extracted-difference factors of the closed J integrand, without its covariance product.

Equations

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

theorem Anderson4D.detJintegrand_eq_skeleton_mul_covariance (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (x : Fin (2 * q) → T4) : detJintegrand ρ ε q σ x = renormalizedJGreenSkeleton σ x * pairingCovarianceProductOn ρ ε σ Finset.univ x

The frozen J integrand is exactly its common signed skeleton times the ambient covariance product.

theorem Anderson4D.renormalizedJGreenSkeleton_eq_of_signature_eq {n : ℕ} (σ τ : PartialPairing (Fin n)) (hsignature : reductionEndpointSignature τ = reductionEndpointSignature σ) : renormalizedJGreenSkeleton τ = renormalizedJGreenSkeleton σ

Endpoint signatures determine the complete signed J skeleton.

theorem Anderson4D.sum_endpointFiber_detJintegrand_eq_skeleton_mul_covariance (ρ : SmoothCutoff) (ε : ℝ) {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (x : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) x = renormalizedJGreenSkeleton κ x * ∑ τ : ReductionEndpointFiberAt κ, pairingCovarianceProductOn ρ ε (↑τ) Finset.univ x

Pointwise, the complete endpoint-fibre sum has one common signed Green skeleton multiplying the exact covariance fibre sum.

The first primitive covariance coordinate on an arbitrary active set

theorem Anderson4D.extractionFiber_firstCoordinate_eq_orderedBlockPairing {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : ExtractionFiberAt κ fuel active) : ↑((extractionFiberEquivBlockComplement κ fuel active h) τ).1 = orderedClosedBlockPairing (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯) ↑(extractionFiberPrimitiveClosedOn κ fuel active h τ)

The block coordinate returned by extractionFiberEquivBlockComplement is definitionally the increasingly ordered restriction carried by extractionFiberPrimitiveClosedOn.

theorem Anderson4D.pairingCovarianceProductOn_extractionFiber_eq_firstCoordinate {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : ExtractionFiberAt κ fuel active) (x : Fin m → T4) : pairingCovarianceProductOn ρ ε (↑τ) (selectedExtractionBlock κ active h) x = primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock κ active h)) ↑((extractionFiberEquivBlockComplement κ fuel active h) τ).1 fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock κ active h))) => x ↑((residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯) i)

Arbitrary ordered-block analytic coordinate.

For every member of an extraction fibre on an arbitrary active carrier, the ambient covariance factor on its selected sparse block is exactly the standard primitive covariance factor indexed by the first coordinate of the block-complement equivalence. This is the reusable pointwise identity for both R-322 and the residual R-324 collapse.

theorem Anderson4D.extractionFiber_blockCoordinate_eq_outside {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB κB' : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) (κC : ExtractionComplementFiberAt κ fuel active h) (i : Fin m) (hi : i ∉ selectedExtractionBlock κ active h) : ↑((extractionFiberEquivBlockComplement κ fuel active h).symm (κB, κC)) i = ↑((extractionFiberEquivBlockComplement κ fuel active h).symm (κB', κC)) i

Changing only the exposed primitive block coordinate leaves the ambient pairing unchanged off that block.

theorem Anderson4D.pairingCovarianceProductOn_complement_eq_of_blockCoordinate {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB κB' : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) (κC : ExtractionComplementFiberAt κ fuel active h) (x : Fin m → T4) : pairingCovarianceProductOn ρ ε (↑((extractionFiberEquivBlockComplement κ fuel active h).symm (κB, κC))) (active \ selectedExtractionBlock κ active h) x = pairingCovarianceProductOn ρ ε (↑((extractionFiberEquivBlockComplement κ fuel active h).symm (κB', κC))) (active \ selectedExtractionBlock κ active h) x

Consequently the covariance product on the complementary active carrier is independent of the primitive block coordinate.

theorem Anderson4D.sum_extractionFiber_covariance_eq_primitive_mul_complement {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (x : Fin m → T4) : ∑ τ : ExtractionFiberAt κ fuel active, pairingCovarianceProductOn ρ ε (↑τ) active x = (∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h))), primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock κ active h)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock κ active h))) => x ↑((residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯) i)) * ∑ κC : ExtractionComplementFiberAt κ fuel active h, pairingCovarianceProductOn ρ ε (↑((extractionFiberEquivBlockComplement κ fuel active h).symm (selectedExtractionPrimitivePairing κ active h, κC))) (active \ selectedExtractionBlock κ active h) x

Exact one-step factorization of the covariance fibre sum on an arbitrary active carrier. The first factor is the complete primitive pairing sum on the selected block; the second is the remaining complementary fibre. There is no pairing-cardinality loss.

theorem Anderson4D.pairingCovarianceProductOn_endpointFiber_eq_firstCoordinate {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (τ : ReductionEndpointFiberAt κ) (x : Fin m → T4) : pairingCovarianceProductOn ρ ε (↑τ) (selectedExtractionBlock κ Finset.univ h) x = primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)) ↑((reductionEndpointFiberEquivBlockComplement κ h) τ).1 fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock κ Finset.univ h))) => x ↑((residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ Finset.univ h) ⋯) i)

Endpoint-signature specialization of the arbitrary ordered-block identity.