Pointwise first-step factorization of the actual R-322 fibre

The endpoint-fibre sum already factors into its common signed Green skeleton and one complete primitive covariance sum for every extraction block. This file reorders those block coordinates by the paper's analytic schedule and splits both products at the head. The result is the exact pointwise head-local × outer form used before the head coordinates are integrated.

noncomputable def Anderson4D.r322ExtractionBlockPrimitiveSum {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (B : ExtractionBlockIndex κ) (x : Fin m → T4) : ℝ

The complete primitive covariance coordinate carried by one concrete extraction block.

Equations

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

noncomputable def Anderson4D.r322AnalyticHeadLocalIntegrandFactor {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin m → T4) : ℝ

The local signed factor at the analytic head: every Green-chain factor touching the head block, its endpoint difference, and the complete primitive covariance sum on that block.

Equations

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

noncomputable def Anderson4D.r322AnalyticHeadOuterIntegrandFactor {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin m → T4) : ℝ

Everything remaining outside the analytic head: the exterior Green and later-difference skeleton, followed by all later primitive block sums.

Equations

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

theorem Anderson4D.sum_endpointFiber_detJintegrand_eq_analyticHead_mul_outer (ρ : SmoothCutoff) (ε : ℝ) {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ.IsFull) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) x = r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule x * r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule x

Exact pointwise head factorization of the existing endpoint fibre.

No model integrand or output predicate occurs here: the left side is the finite sum of the project's actual detJintegrand. Both the signed skeleton and the dependent primitive block product are split at the first analytic schedule step.

The outer factor is independent of head-block coordinates

theorem Anderson4D.r322AnalyticSchedule_blocks_pairwise_disjoint {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise Disjoint (List.map Prod.snd (r322AnalyticSchedule κ))

The analytic schedule inherits pairwise disjointness from the concrete extraction-block list.

theorem Anderson4D.r322AnalyticHeadBlock_disjoint_tailBlock {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) (j : Fin tail.length) : Disjoint head.2 (tail.get j).2

In a displayed head/tail schedule, the concrete head block is disjoint from every later concrete block.

theorem Anderson4D.extractionBlockPrimitiveCovarianceFactor_eq_of_eq_on {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (B : ExtractionBlockIndex κ) (σ : ↥(primitiveFullPairings (residualBlockOrder ↑B))) (x y : Fin m → T4) (hxy : ∀ i ∈ ↑B, x i = y i) : extractionBlockPrimitiveCovarianceFactor ρ ε κ B σ x = extractionBlockPrimitiveCovarianceFactor ρ ε κ B σ y

A primitive covariance coordinate reads only ambient positions belonging to its certified extraction block.

theorem Anderson4D.r322ExtractionBlockPrimitiveSum_eq_of_eq_on {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (B : ExtractionBlockIndex κ) (x y : Fin m → T4) (hxy : ∀ i ∈ ↑B, x i = y i) : r322ExtractionBlockPrimitiveSum ρ ε κ B x = r322ExtractionBlockPrimitiveSum ρ ε κ B y

Consequently the complete primitive sum on one block depends only on that block's ambient coordinates.

theorem Anderson4D.r322AnalyticTailPrimitiveProduct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (x y : Fin m → T4) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule κ = head :: tail) (hxy : ∀ i ∉ head.2, x i = y i) : ∏ j : Fin tail.length, r322ExtractionBlockPrimitiveSum ρ ε κ (r322AnalyticTailBlockIndex κ hschedule j) x = ∏ j : Fin tail.length, r322ExtractionBlockPrimitiveSum ρ ε κ (r322AnalyticTailBlockIndex κ hschedule j) y

The product of all later primitive coordinates is unchanged when only head-block coordinates move.

theorem Anderson4D.r322AnalyticHeadOuterIntegrandFactor_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (x y : Fin m → T4) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule κ = head :: tail) (hxy : ∀ i ∉ head.2, x i = y i) : r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule x = r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule y

The complete outer pointwise factor, including every later primitive coordinate, is constant in the head-block variables.