One concrete proper-block collapse for R-322

Paper: R-322 — §4.1 (4.8) — one proper-block collapse

This file formalizes the analytic operation in paper (4.7)--(4.8). A primitive block with profile J sits between a left input Gp and the endpoint difference of a right input Gr. Integrating the two block endpoints produces a new one-variable input kernel.

The construction below is concrete: it is the nested Bochner integral from (4.8), not an output predicate. We prove

• equality with the difference form of the renormalization step;
• equality with raw insertion minus its scalar counterterm under the exact Fubini/integrability hypotheses already isolated for Proposition 3.2;
• a product-measure Fubini form;
• preservation of the hyperoctahedral class E.

The pointwise |z|⁻² estimate is a separate quantitative step: it combines Proposition 4.1 with the three regions (4.10)--(4.12).

noncomputable def Anderson4D.r322CollapseIntegrand (Gp J Gr : T4 → ℝ) (u : T4) (p : T4 × T4) : ℝ

The two-variable integrand in paper (4.8), after translating the right external endpoint to zero.

Equations

• Anderson4D.r322CollapseIntegrand Gp J Gr u p = Gp (u - p.1) * J (p.1 - p.2) * (Gr p.2 - Gr p.1)

noncomputable def Anderson4D.r322Collapse (Gp J Gr : T4 → ℝ) (u : T4) : ℝ

One concrete proper-block collapse, paper (4.8).

Equations

• Anderson4D.r322Collapse Gp J Gr u = ∫ (p : Anderson4D.T4 × Anderson4D.T4), Anderson4D.r322CollapseIntegrand Gp J Gr u p ∂Anderson4D.paperMeasure.prod Anderson4D.paperMeasure

theorem Anderson4D.r322Collapse_eq_differenceRenormalizationStep (Gp J Gr : T4 → ℝ) (u : T4) (hint : MeasureTheory.Integrable (r322CollapseIntegrand Gp J Gr u) (paperMeasure.prod paperMeasure)) : r322Collapse Gp J Gr u = differenceRenormalizationStep Gp J Gr u 0

The translated collapse is exactly the difference-renormalization step of paper (3.7), with right endpoint fixed at zero.

theorem Anderson4D.raw_sub_counterterm_eq_r322Collapse (Gp J Gr : T4 → ℝ) (u : T4) (hshift : ∀ (z : T4), ∫ (w : T4), J (z - w) ∂paperMeasure = ∫ (v : T4), J v ∂paperMeasure) (hrawInner : ∀ (z : T4), MeasureTheory.Integrable (fun (w : T4) => Gp (u - z) * J (z - w) * Gr w) paperMeasure) (hdiagInner : ∀ (z : T4), MeasureTheory.Integrable (fun (w : T4) => Gp (u - z) * J (z - w) * Gr z) paperMeasure) (hrawOuter : MeasureTheory.Integrable (fun (z : T4) => ∫ (w : T4), Gp (u - z) * J (z - w) * Gr w ∂paperMeasure) paperMeasure) (hdiagOuter : MeasureTheory.Integrable (fun (z : T4) => ∫ (w : T4), Gp (u - z) * J (z - w) * Gr z ∂paperMeasure) paperMeasure) (hjoint : MeasureTheory.Integrable (r322CollapseIntegrand Gp J Gr u) (paperMeasure.prod paperMeasure)) : rawRenormalizationStep Gp J Gr u 0 - renormalizationCounterterm Gp J Gr u 0 = r322Collapse Gp J Gr u

Concrete one-step version of (3.7)/(4.8): raw insertion minus the counterterm is the collapsed input kernel.

Product-measure Fubini form

theorem Anderson4D.r322Collapse_eq_prodIntegral (Gp J Gr : T4 → ℝ) (u : T4) : r322Collapse Gp J Gr u = ∫ (p : T4 × T4), r322CollapseIntegrand Gp J Gr u p ∂paperMeasure.prod paperMeasure

Joint integrability licenses the product-measure form of the collapse. This prevents any later use of a junk-totalized iterated integral.

Hyperoctahedral symmetry propagation

theorem Anderson4D.r322Collapse_memE {Gp J Gr : T4 → ℝ} (hGp : MemEClassT4 Gp) (hJ : MemEClassT4 J) (hGr : MemEClassT4 Gr) : MemEClassT4 (r322Collapse Gp J Gr)

A concrete proper-block collapse preserves the paper's class E.