Proper selected-block replacement in signed R-324 phase A

This module records the analytic end of a genuine proper selected-block update. The complete primitive pairing coordinate is evaluated at its two actual endpoints, translated to the difference kernel used by r322CollapseIntegrand, and then replaced by the named updated edge.

The subsequent R-324 theorem applies this identity only after identifying the corresponding factors of the original reconstructed deterministic integrand.

The complete primitive coordinate at two actual endpoints

theorem Anderson4D.sum_detJWith_eq_r322SelectedPrimitiveKernelSum_sub (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ∑ κB : ↥(primitiveFullPairings n), detJWith ρ lam ε n hn G (↑κB) z w = r322SelectedPrimitiveKernelSum ρ lam ε n hn G (z - w)

Translation invariance identifies the complete primitive coordinate at (z,w) with the selected difference kernel at z-w.

Exact signed proper-edge update

theorem Anderson4D.integral_completePrimitiveAtEndpoints_eq_selectedPrimitiveInner (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Gp Gr : T4 → ℝ) (u : T4) : ∫ (p : T4 × T4), (Gp (u - p.1) * ∑ κB : ↥(primitiveFullPairings n), detJWith ρ lam ε n hn G (↑κB) p.1 p.2) * (Gr p.2 - Gr p.1) ∂paperMeasure.prod paperMeasure = ∫ (p : T4 × T4), r322CollapseIntegrand Gp (r322SelectedPrimitiveKernelSum ρ lam ε n hn G) Gr u p ∂paperMeasure.prod paperMeasure

The endpoint integral containing the complete primitive coordinate at its actual endpoints is exactly the existing selected-kernel collapse.

theorem Anderson4D.integral_completePrimitiveAtEndpoints_eq_replacementEdge {ι : Type u_1} [DecidableEq ι] (edges : ι → T4 → ℝ) (slot : ι) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Gp Gr : T4 → ℝ) (u : T4) : ∫ (p : T4 × T4), (Gp (u - p.1) * ∑ κB : ↥(primitiveFullPairings n), detJWith ρ lam ε n hn G (↑κB) p.1 p.2) * (Gr p.2 - Gr p.1) ∂paperMeasure.prod paperMeasure = r322ReplaceEdge edges slot Gp (primitiveKernelDiff ρ lam ε n hn G) Gr slot u

Exact generalized proper-block replacement.

The selected pairing sum and both endpoint integrations remain signed. The conclusion is the value of the named updated edge, so the result can be substituted into the actual R-324 outer coordinate without changing any other edge.