The exact selected-block kernel update for R-322

After the signed Fubini reindex, the selected primitive pairing coordinate is summed and integrated before any absolute value is taken. This file identifies that complete kernel with primitiveKernelDiff and records the result as an update of one named slot in a heterogeneous edge family.

All complementary coordinates, remaining finite sums, and remaining integrals can be carried by an arbitrary outer parameter type.

The complete signed primitive coordinate

noncomputable def Anderson4D.r322SelectedPrimitiveKernelSum (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z : T4) : ℝ

The complete generalized J kernel carried by one selected primitive block, with the right endpoint translated to zero.

Equations

• Anderson4D.r322SelectedPrimitiveKernelSum ρ lam ε n hn G z = ∑ σ ∈ Anderson4D.primitiveFullPairings n, Anderson4D.detJWith ρ lam ε n hn G σ z 0

theorem Anderson4D.r322SelectedPrimitiveKernelSum_eq_primitiveKernelDiff (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) : r322SelectedPrimitiveKernelSum ρ lam ε n hn G = primitiveKernelDiff ρ lam ε n hn G

Summing the selected primitive pairing coordinate and all of its internal variables gives exactly the signed kernel used by the collapse.

Updating exactly one heterogeneous edge

noncomputable def Anderson4D.r322ReplaceEdge {ι : Type u_1} [DecidableEq ι] (edges : ι → T4 → ℝ) (slot : ι) (Gp J Gr : T4 → ℝ) : ι → T4 → ℝ

Replace one named heterogeneous edge by the concrete proper-block collapse. Every other edge is retained definitionally.

Equations

• Anderson4D.r322ReplaceEdge edges slot Gp J Gr = Function.update edges slot (Anderson4D.r322Collapse Gp J Gr)

@[simp]

theorem Anderson4D.r322ReplaceEdge_apply_same {ι : Type u_1} [DecidableEq ι] (edges : ι → T4 → ℝ) (slot : ι) (Gp J Gr : T4 → ℝ) (u : T4) : r322ReplaceEdge edges slot Gp J Gr slot u = r322Collapse Gp J Gr u

theorem Anderson4D.r322ReplaceEdge_apply_ne {ι : Type u_1} [DecidableEq ι] (edges : ι → T4 → ℝ) (slot other : ι) (hother : other ≠ slot) (Gp J Gr : T4 → ℝ) (u : T4) : r322ReplaceEdge edges slot Gp J Gr other u = edges other u

theorem Anderson4D.selectedPrimitiveInnerIntegral_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), r322CollapseIntegrand Gp (r322SelectedPrimitiveKernelSum ρ lam ε n hn G) Gr u p ∂paperMeasure.prod paperMeasure = r322ReplaceEdge edges slot Gp (primitiveKernelDiff ρ lam ε n hn G) Gr slot u

Exact one-selected-block kernel identity.

The inner product integral containing the complete primitive pairing sum is literally the value of the updated heterogeneous edge at slot. This is a signed equality: neither the primitive sum nor the Green difference is put under an absolute value.

Complement coordinates and remaining sums stay outside

theorem Anderson4D.integral_outer_selectedPrimitiveInner_eq_updatedEdge {ι : Type u_1} {Ω : Type u_2} [DecidableEq ι] [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (outer : Ω → ℝ) (edges : Ω → ι → T4 → ℝ) (slot : ι) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Ω → Fin (2 * n - 1) → T4 → ℝ) (Gp Gr : Ω → T4 → ℝ) (u : Ω → T4) : ∫ (ω : Ω), outer ω * ∫ (p : T4 × T4), r322CollapseIntegrand (Gp ω) (r322SelectedPrimitiveKernelSum ρ lam ε n hn (G ω)) (Gr ω) (u ω) p ∂paperMeasure.prod paperMeasure ∂ν = ∫ (ω : Ω), outer ω * r322ReplaceEdge (edges ω) slot (Gp ω) (primitiveKernelDiff ρ lam ε n hn (G ω)) (Gr ω) slot (u ω) ∂ν

Parameterized outer form of the exact update.

ω may contain all complementary spatial coordinates, the complementary pairing fibre, and any remaining dependent finite-sum coordinates. Hence this equality can be inserted beneath the next outer sum or product measure without changing their order.