Recursive J kernels and Proposition 3.3

Paper: D-C2q — §3.2 (3.8)–(3.11) — the renormalization constants

This file applies the edge-replacement recursion of Proposition 3.2 to the internal J chain of paper §3.2. The final extraction of a full interval has no right chain edge; it is represented by the value 1, exactly as in the totalized closed formula detJintegrand.

noncomputable def Anderson4D.jChainEdgeWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (e : Fin (n - 1)) : ℝ

A generalized internal chain edge for a tuple of length n.

Equations

• Anderson4D.jChainEdgeWith G xt e = G e (xt ⟨↑e, ⋯⟩ - xt ⟨↑e + 1, ⋯⟩)

noncomputable def Anderson4D.diffFactorJWith {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (p : Fin n × Fin n) : ℝ

Generalized endpoint difference for the internal J chain. The last endpoint of the whole interval has no edge to its right and contributes 1.

Equations

• Anderson4D.diffFactorJWith G xt p = if h : ↑p.2 + 1 < n then G ⟨↑p.2, ⋯⟩ (xt p.2 - xt ⟨↑p.2 + 1, h⟩) - G ⟨↑p.2, ⋯⟩ (xt p.1 - xt ⟨↑p.2 + 1, h⟩) else 1

def Anderson4D.jReplacementList {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) : List (Fin n × Fin n) → List (Fin (n - 1) × ℝ)

Valid edge replacements extracted from a list of endpoint pairs.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.jReplacementList G xt [] = []

theorem Anderson4D.jReplacementList_values {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (ps : List (Fin n × Fin n)) : (List.map Prod.snd (jReplacementList G xt ps)).prod = (List.map (diffFactorJWith G xt) ps).prod

Invalid (whole-interval) endpoints contribute 1, so filtering them from the replacement recursion preserves the product of differences.

noncomputable def Anderson4D.extractedJRightEdges {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (ps : List (Fin n × Fin n)) : Finset (Fin (n - 1))

Edges replaced in the internal J chain.

Equations

• Anderson4D.extractedJRightEdges G xt ps = (List.map Prod.fst (Anderson4D.jReplacementList G xt ps)).toFinset

noncomputable def Anderson4D.detJclosedIntegrandWith (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (σ : PartialPairing (Fin n)) (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) : ℝ

Closed generalized J integrand obtained from the replacement list.

Equations

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

noncomputable def Anderson4D.detJrecursiveIntegrandWith (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (σ : PartialPairing (Fin n)) (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) : ℝ

Recursive Definition 3.1 semantics for the internal J chain.

Equations

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

theorem Anderson4D.detJrecursiveIntegrandWith_eq_prod (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (σ : PartialPairing (Fin n)) (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) : detJrecursiveIntegrandWith ρ ε n σ G xt = detJclosedIntegrandWith ρ ε n σ G xt

Proposition 3.3, generalized-input integrand form.

Green specialization and the frozen J formula

@[simp]

theorem Anderson4D.diffFactorJWith_green {n : ℕ} (xt : Fin n → T4) (p : Fin n × Fin n) : diffFactorJWith (fun (x : Fin (n - 1)) => greenFn) xt p = diffFactorJ xt p

theorem Anderson4D.mem_jReplacementList_keys_iff {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (ps : List (Fin n × Fin n)) (e : Fin (n - 1)) : e ∈ List.map Prod.fst (jReplacementList G xt ps) ↔ ↑e ∈ List.map (fun (p : Fin n × Fin n) => ↑p.2) ps

The valid replacement keys are exactly the right-endpoint values which can index an internal chain edge. A whole-interval right endpoint is automatically impossible on the left.

theorem Anderson4D.mem_extractedJRightEdges_iff {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (xt : Fin n → T4) (ps : List (Fin n × Fin n)) (e : Fin (n - 1)) : e ∈ extractedJRightEdges G xt ps ↔ ↑e ∈ List.map (fun (p : Fin n × Fin n) => ↑p.2) ps

theorem Anderson4D.detJclosedIntegrandWith_green_eq_detJintegrand (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xt : Fin (2 * q) → T4) : detJclosedIntegrandWith ρ ε (2 * q) σ (fun (x : Fin (2 * q - 1)) => greenFn) xt = detJintegrand ρ ε q σ xt

The generalized closed J integrand at the constant Green family is the frozen formula (3.12) from Kernels.lean.

noncomputable def Anderson4D.detJrecursive (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : PartialPairing (Fin (2 * q)) → T4 → T4 → ℝ

Recursive J_{2q,σ} obtained by integrating the recursive integrand.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.detJrecursive ρ lam ε 0 x_4 x✝¹ x✝ = 0

theorem Anderson4D.renormJ_eq_prod (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (z w : T4) : detJrecursive ρ lam ε q σ z w = detJ ρ lam ε q σ z w

Proposition 3.3, integrated form. The recursively renormalized J kernel equals the closed formula used by detJ.