Recursive deterministic renormalization and the closed formula

Paper: D-RI — Def 3.1 / Prop 3.2 — deterministic renormalization, closed formula (3.6)

The definitions in Kernels.lean use the closed formula (3.6), as required by DESIGN §5.7bis. This file supplies the converse obligation: after the one-step identity (3.7), every application of paper Definition 3.1 replaces one chain edge by its endpoint difference. We implement those replacements recursively in extraction order and prove that their result is exactly the closed product. Unlike a definitional alias, the recursive side carries a shrinking active-edge set.

All definitions accept a family [G₀, …, Gₘ]; specializing every entry to greenFn recovers detIntegrand.

The one-step analytic identity

noncomputable def Anderson4D.rawRenormalizationStep (Gp J Gr : T4 → ℝ) (x y : T4) : ℝ

The unrenormalized two-kernel insertion in the first line of paper (3.5), with J between the two boundary kernels.

Equations

• Anderson4D.rawRenormalizationStep Gp J Gr x y = ∫ (z : Anderson4D.T4), ∫ (w : Anderson4D.T4), Gp (x - z) * J (z - w) * Gr (w - y) ∂Anderson4D.paperMeasure ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.renormalizationCounterterm (Gp J Gr : T4 → ℝ) (x y : T4) : ℝ

The scalar counterterm in paper (3.5), with the formal delta already evaluated.

Equations

• Anderson4D.renormalizationCounterterm Gp J Gr x y = (∫ (u : Anderson4D.T4), J u ∂Anderson4D.paperMeasure) * ∫ (z : Anderson4D.T4), Gp (x - z) * Gr (z - y) ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.differenceRenormalizationStep (Gp J Gr : T4 → ℝ) (x y : T4) : ℝ

The difference-integrand form in the second line of paper (3.7).

Equations

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

theorem Anderson4D.raw_sub_counterterm_eq_difference (Gp J Gr : T4 → ℝ) (x y : T4) (hshift : ∀ (z : T4), ∫ (w : T4), J (z - w) ∂paperMeasure = ∫ (u : T4), J u ∂paperMeasure) (hrawInner : ∀ (z : T4), MeasureTheory.Integrable (fun (w : T4) => Gp (x - z) * J (z - w) * Gr (w - y)) paperMeasure) (hdiagInner : ∀ (z : T4), MeasureTheory.Integrable (fun (w : T4) => Gp (x - z) * J (z - w) * Gr (z - y)) paperMeasure) (hrawOuter : MeasureTheory.Integrable (fun (z : T4) => ∫ (w : T4), Gp (x - z) * J (z - w) * Gr (w - y) ∂paperMeasure) paperMeasure) (hdiagOuter : MeasureTheory.Integrable (fun (z : T4) => ∫ (w : T4), Gp (x - z) * J (z - w) * Gr (z - y) ∂paperMeasure) paperMeasure) : rawRenormalizationStep Gp J Gr x y - renormalizationCounterterm Gp J Gr x y = differenceRenormalizationStep Gp J Gr x y

Paper (3.7). Subtracting the scalar counterterm is equivalent to replacing the right boundary kernel by its endpoint difference.

The hypotheses expose exactly the two uses of Bochner-integral linearity and translation invariance needed by the paper's formal calculation; later analytic estimates discharge them for the concrete kernels.

A generic replacement-product recursion

def Anderson4D.replacementProduct {ι : Type u_1} [DecidableEq ι] (base : ι → ℝ) : List (ι × ℝ) → Finset ι → ℝ

Starting with the product of base over active, recursively remove the key of each replacement and multiply by its new value. This is the scalar semantics of successive edge replacements, without division and hence with no junk case when an old edge factor vanishes.

Equations

• Anderson4D.replacementProduct base [] x✝ = ∏ i ∈ x✝, base i
• Anderson4D.replacementProduct base (u :: us) x✝ = u.2 * Anderson4D.replacementProduct base us (x✝.erase u.1)

theorem Anderson4D.replacementProduct_eq_prod {ι : Type u_1} [DecidableEq ι] (base : ι → ℝ) (us : List (ι × ℝ)) (active : Finset ι) : replacementProduct base us active = (List.map Prod.snd us).prod * ∏ i ∈ active \ (List.map Prod.fst us).toFinset, base i

A recursive sequence of replacements is the product of all replacement values times the product of untouched base entries. Repeated keys are allowed: they are removed once but every explicitly requested replacement value is retained.

Generalized chain inputs

def Anderson4D.extractedRightEdge {m : ℕ} (p : Fin m × Fin m) : Fin (m + 1)

The chain edge immediately to the right of an extracted interval p = (l,r). Paper indices are one-based, so a zero-based right endpoint r replaces edge r+1 among the m+1 chain edges.

Equations

• Anderson4D.extractedRightEdge p = ⟨↑p.2 + 1, ⋯⟩

@[simp]

theorem Anderson4D.extractedRightEdge_val {m : ℕ} (p : Fin m × Fin m) : ↑(extractedRightEdge p) = ↑p.2 + 1

noncomputable def Anderson4D.chainEdgeWith {m : ℕ} (G : Fin (m + 1) → T4 → ℝ) (xt : Fin (m + 2) → T4) (e : Fin (m + 1)) : ℝ

Unrenormalized value of chain edge e for generalized input kernels G₀,…,Gₘ.

Equations

• Anderson4D.chainEdgeWith G xt e = G e (xt e.castSucc - xt e.succ)

noncomputable def Anderson4D.diffFactorWith {m : ℕ} (G : Fin (m + 1) → T4 → ℝ) (xt : Fin (m + 2) → T4) (p : Fin m × Fin m) : ℝ

The difference which replaces the edge to the right of an extracted interval, with the correct member of the generalized kernel family.

Equations

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

def Anderson4D.extractedRightEdges {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin (m + 1))

The finite set of chain edges replaced by the extraction procedure.

Equations

• Anderson4D.extractedRightEdges κ = (List.map Anderson4D.extractedRightEdge (Anderson4D.extract κ)).toFinset

noncomputable def Anderson4D.detIntegrandWith (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (G : Fin (m + 1) → T4 → ℝ) (xt : Fin (m + 2) → T4) : ℝ

The generalized closed integrand (paper (3.6)) before the global coupling factor and integration.

Equations

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

noncomputable def Anderson4D.detRIkernelWith (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (G : Fin (m + 1) → T4 → ℝ) (xt : Fin (m + 2) → T4) : ℝ

Recursive deterministic renormalization kernel (paper Def. 3.1 after the one-step identity (3.7)). Each smallest-leftmost interval returned by extract κ removes its right chain edge and inserts the corresponding difference. The covariance factors do not change during this operation.

Equations

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

noncomputable def Anderson4D.detRIkernel (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : ℝ

Specialization of the recursive kernel to the Green chain used in the paper.

Equations

• Anderson4D.detRIkernel ρ ε m κ xt = Anderson4D.detRIkernelWith ρ ε m κ (fun (x : Fin (m + 1)) => Anderson4D.greenFn) xt

theorem Anderson4D.prod_if_mem_eq_prod_sdiff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → ℝ) : (∏ i : ι, if i ∈ s then 1 else f i) = ∏ i ∈ Finset.univ \ s, f i

A product which replaces all entries in s by one is the product of the base function over the complement of s.

theorem Anderson4D.prod_if_not_extractedRightEdges {m : ℕ} (κ : PartialPairing (Fin m)) (f : Fin (m + 1) → ℝ) : (∏ e : Fin (m + 1), if e ∈ extractedRightEdges κ then 1 else f e) = ∏ e ∈ Finset.univ \ extractedRightEdges κ, f e

The untouched-edge product written with an if is exactly the product over the complement of the replaced edge set.

theorem Anderson4D.detRIkernelWith_eq_prod (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (G : Fin (m + 1) → T4 → ℝ) (xt : Fin (m + 2) → T4) : detRIkernelWith ρ ε m κ G xt = detIntegrandWith ρ ε m κ G xt

Proposition 3.2, generalized-input integrand form. The recursive edge-removal semantics of Definition 3.1 equals the closed formula (3.6). The proof is a genuine induction over the extracted endpoint list through replacementProduct_eq_prod.

theorem Anderson4D.detRIkernel_eq_prod (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detRIkernel ρ ε m κ xt = detIntegrandWith ρ ε m κ (fun (x : Fin (m + 1)) => greenFn) xt

Green-kernel specialization of Proposition 3.2.

theorem Anderson4D.detIntegrandWith_green_eq_detIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detIntegrandWith ρ ε m κ (fun (x : Fin (m + 1)) => greenFn) xt = detIntegrand ρ ε m κ xt

The generalized closed formula specializes definitionally (up to the equivalent Fin/value membership representation of replaced edges) to the original frozen detIntegrand.

theorem Anderson4D.detRIkernel_eq_detIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detRIkernel ρ ε m κ xt = detIntegrand ρ ε m κ xt

Direct Green-kernel form of Proposition 3.2.

Integrated recursive kernels

noncomputable def Anderson4D.detRIrecursiveFull (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) : ℝ

The fully integrated kernel built from the recursive edge-replacement semantics.

Equations

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

noncomputable def Anderson4D.detRIrecursiveProfile (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) (z : Fin m → T4) : ℝ

The profile version of detRIrecursiveFull, integrating only paired variables and keeping the single variables free.

Equations

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

theorem Anderson4D.detRIrecursiveFull_eq_detRIfull (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) : detRIrecursiveFull ρ lam ε m κ x y = detRIfull ρ lam ε m κ x y

Integrated form of Proposition 3.2.

theorem Anderson4D.detRIrecursiveProfile_eq_detRIprofile (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) (z : Fin m → T4) : detRIrecursiveProfile ρ lam ε m κ x y z = detRIprofile ρ lam ε m κ x y z

Profile-integrated form of Proposition 3.2.