All-order integrability of the R-322 J kernels

The pointwise reduction output used in (3.22) carries an integrability field. This file discharges that field at every positive order.

Each valid replacement in the closed J chain removes the edge immediately to the right of an extracted interval and inserts a difference. Expanding the differences chooses either the original edge or a shortcut from an earlier vertex. Every branch is therefore an increasing Green tree, so the joint tree-integrability theorem applies. The covariance product is measurable and bounded at a fixed positive scale.

Joint integrability is finally transported to the fixed terminal endpoint w = 0. Fubini first supplies one integrable terminal section; simultaneous translation of every spatial variable identifies that section with the zero section. Thus no unjustified pointwise Fubini claim is used.

Valid extracted right edges of the internal J chain

def Anderson4D.jExtractedRightEdges {n : ℕ} (σ : PartialPairing (Fin n.succ)) : Finset (Fin n)

The valid extracted right edges of a J chain. An extracted interval ending at the last vertex has no edge to its right and is intentionally absent.

Equations

• Anderson4D.jExtractedRightEdges σ = {e : Fin n | ↑e ∈ List.map (fun (p : Fin n.succ × Fin n.succ) => ↑p.2) (Anderson4D.extract σ)}

@[simp]

theorem Anderson4D.mem_jExtractedRightEdges {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) : e ∈ jExtractedRightEdges σ ↔ ↑e ∈ List.map (fun (p : Fin n.succ × Fin n.succ) => ↑p.2) (extract σ)

noncomputable def Anderson4D.diffFactorJSuccWith {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) (p : Fin n.succ × Fin n.succ) : ℝ

Positive-length specialization of the generalized J difference.

Equations

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

@[simp]

theorem Anderson4D.diffFactorJSuccWith_green {n : ℕ} (x : Fin n.succ → T4) (p : Fin n.succ × Fin n.succ) : diffFactorJSuccWith (fun (x : Fin n) => greenFn) x p = diffFactorJ x p

def Anderson4D.jSuccReplacementList {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) : List (Fin n.succ × Fin n.succ) → List (Fin n × ℝ)

Positive-length specialization of jReplacementList, with its edge carrier written definitionally as Fin n rather than Fin (n.succ - 1). This avoids dependent casts in the tree expansion.

Equations

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

theorem Anderson4D.jSuccReplacementList_values {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) (ps : List (Fin n.succ × Fin n.succ)) : (List.map Prod.snd (jSuccReplacementList G x ps)).prod = (List.map (diffFactorJSuccWith G x) ps).prod

The specialized list retains exactly the product of all closed-form difference factors; an invalid terminal extraction contributes 1.

theorem Anderson4D.mem_jSuccReplacementList_keys_iff {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) (ps : List (Fin n.succ × Fin n.succ)) (e : Fin n) : e ∈ List.map Prod.fst (jSuccReplacementList G x ps) ↔ ↑e ∈ List.map (fun (p : Fin n.succ × Fin n.succ) => ↑p.2) ps

Membership of specialized replacement keys is exactly membership of the extracted right-endpoint value list.

theorem Anderson4D.exists_jExtractedPairOfRightEdge {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) (he : e ∈ jExtractedRightEdges σ) : ∃ p ∈ extract σ, ↑p.2 = ↑e

Membership in the valid edge set is witnessed by an actual extracted interval with that right endpoint.

noncomputable def Anderson4D.jExtractedPairOfRightEdge {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) (he : e ∈ jExtractedRightEdges σ) : Fin n.succ × Fin n.succ

The unique extracted interval represented by a valid right edge.

Equations

• Anderson4D.jExtractedPairOfRightEdge σ e he = Classical.choose ⋯

theorem Anderson4D.jExtractedPairOfRightEdge_mem {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) (he : e ∈ jExtractedRightEdges σ) : jExtractedPairOfRightEdge σ e he ∈ extract σ

theorem Anderson4D.jExtractedPairOfRightEdge_right {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) (he : e ∈ jExtractedRightEdges σ) : ↑(jExtractedPairOfRightEdge σ e he).2 = ↑e

theorem Anderson4D.jExtractedPairOfRightEdge_eq {n : ℕ} (σ : PartialPairing (Fin n.succ)) (p : Fin n.succ × Fin n.succ) (hp : p ∈ extract σ) (hvalid : ↑p.2 + 1 < n.succ) : jExtractedPairOfRightEdge σ ⟨↑p.2, ⋯⟩ ⋯ = p

The chosen inverse of a valid extracted right edge returns its original extracted interval.

noncomputable def Anderson4D.jExtractedShortcutParent {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) (he : e ∈ jExtractedRightEdges σ) : Fin (↑e + 1)

The shortcut parent is the left endpoint of the extracted interval.

Equations

• Anderson4D.jExtractedShortcutParent σ e he = ⟨↑(Anderson4D.jExtractedPairOfRightEdge σ e he).1, ⋯⟩

Increasing-tree expansion of the signed Green skeleton

noncomputable def Anderson4D.jOriginalGreenEdge {n : ℕ} (x : Fin n.succ → T4) (e : Fin n) : ℂ

Original internal chain edge with right vertex e+1.

Equations

• Anderson4D.jOriginalGreenEdge x e = ↑(Anderson4D.greenFn (x e.castSucc - x e.succ))

def Anderson4D.jOrdinaryEdgeParent {n : ℕ} (e : Fin n) : Fin (↑e + 1)

The predecessor of an ordinary internal J edge.

Equations

• Anderson4D.jOrdinaryEdgeParent e = ⟨↑e, ⋯⟩

noncomputable def Anderson4D.jExtractedShortcutGreenEdge {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) (e : Fin n) : ℂ

Shortcut edge at a valid extracted right endpoint, and zero at every unextracted endpoint.

Equations

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

noncomputable def Anderson4D.expandedJGreenTreeParent {n : ℕ} (σ : PartialPairing (Fin n.succ)) (original : Finset (Fin n)) : IncreasingTreeParent n

Parent map of one branch in the powerset expansion.

Equations

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

noncomputable def Anderson4D.expandedJGreenBranch {n : ℕ} (σ : PartialPairing (Fin n.succ)) (original : Finset (Fin n)) (x : Fin n.succ → T4) : ℂ

One powerset branch of the internal J Green product.

Equations

• Anderson4D.expandedJGreenBranch σ original x = (∏ e ∈ original, Anderson4D.jOriginalGreenEdge x e) * ∏ e ∈ originalᶜ, Anderson4D.jExtractedShortcutGreenEdge σ x e

theorem Anderson4D.expandedJGreenBranch_eq_tree {n : ℕ} (σ : PartialPairing (Fin n.succ)) (original : Finset (Fin n)) (hshortcut : ∀ e ∉ original, e ∈ jExtractedRightEdges σ) : expandedJGreenBranch σ original = increasingTreeGreenProduct (expandedJGreenTreeParent σ original)

A branch that only chooses existing shortcuts is exactly an increasing Green tree.

theorem Anderson4D.integrable_expandedJGreenBranch {n : ℕ} (σ : PartialPairing (Fin n.succ)) (original : Finset (Fin n)) : MeasureTheory.Integrable (expandedJGreenBranch σ original) (MeasureTheory.Measure.pi fun (x : Fin n.succ) => paperMeasure)

Every expansion branch is jointly integrable. A branch asking for a nonexistent shortcut is identically zero.

noncomputable def Anderson4D.expandedJGreenMajorant {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) : ℂ

Product of edgewise sums dominating the signed expansion.

Equations

• Anderson4D.expandedJGreenMajorant σ x = ∏ e : Fin n, (Anderson4D.jOriginalGreenEdge x e + Anderson4D.jExtractedShortcutGreenEdge σ x e)

theorem Anderson4D.expandedJGreenMajorant_eq_sum_branches {n : ℕ} (σ : PartialPairing (Fin n.succ)) : expandedJGreenMajorant σ = fun (x : Fin n.succ → T4) => ∑ original : Finset (Fin n), expandedJGreenBranch σ original x

theorem Anderson4D.integrable_expandedJGreenMajorant {n : ℕ} (σ : PartialPairing (Fin n.succ)) : MeasureTheory.Integrable (expandedJGreenMajorant σ) (MeasureTheory.Measure.pi fun (x : Fin n.succ) => paperMeasure)

Identification with the frozen signed skeleton

theorem Anderson4D.jReplacementList_keys_nodup_of_right_nodup {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) (ps : List (Fin n.succ × Fin n.succ)) (hps : (List.map Prod.snd ps).Nodup) : (List.map Prod.fst (jSuccReplacementList G x ps)).Nodup

Filtering invalid whole-interval replacements preserves distinctness of right-edge keys.

theorem Anderson4D.prod_jExtractedRightEdges_eq_jReplacementList {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) {M : Type u_1} [CommMonoid M] (f : Fin n → M) : ∏ e ∈ jExtractedRightEdges σ, f e = (List.map (fun (u : Fin n × ℝ) => f u.1) (jSuccReplacementList (fun (x : Fin n) => greenFn) x (extract σ))).prod

Products over the valid edge finset can be reindexed by the exact replacement list.

theorem Anderson4D.mem_jReplacementList_exists_source {n : ℕ} (G : Fin n → T4 → ℝ) (x : Fin n.succ → T4) (ps : List (Fin n.succ × Fin n.succ)) (u : Fin n × ℝ) (hu : u ∈ jSuccReplacementList G x ps) : ∃ p ∈ ps, ↑p.2 + 1 < n.succ ∧ ↑u.1 = ↑p.2 ∧ u.2 = diffFactorJSuccWith G x p

Every entry of a replacement list comes from a valid source interval.

theorem Anderson4D.jExtractedShortcutGreenEdge_at_pair {n : ℕ} (σ : PartialPairing (Fin n.succ)) (p : Fin n.succ × Fin n.succ) (hp : p ∈ extract σ) (hvalid : ↑p.2 + 1 < n.succ) (x : Fin n.succ → T4) : jExtractedShortcutGreenEdge σ x ⟨↑p.2, ⋯⟩ = ↑(greenFn (x p.1 - x ⟨↑p.2 + 1, hvalid⟩))

At a valid extracted interval, the chosen shortcut is the Green edge from its left endpoint to the vertex immediately after its right endpoint.

theorem Anderson4D.jReplacementList_green_entry_eq_difference {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) (u : Fin n × ℝ) (hu : u ∈ jSuccReplacementList (fun (x : Fin n) => greenFn) x (extract σ)) : ↑u.2 = jOriginalGreenEdge x u.1 - jExtractedShortcutGreenEdge σ x u.1

Each concrete replacement-list value is its original edge minus its chosen shortcut.

theorem Anderson4D.prod_jGreenDifference_eq_extract_diffFactorJ {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) : ∏ e ∈ jExtractedRightEdges σ, (jOriginalGreenEdge x e - jExtractedShortcutGreenEdge σ x e) = (List.map (fun (p : Fin n.succ × Fin n.succ) => ↑(diffFactorJ x p)) (extract σ)).prod

The product of signed edge differences is exactly the replacement-list value product, including the convention that a whole-interval extraction contributes 1.

noncomputable def Anderson4D.expandedJGreenDifferenceProduct {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) : ℂ

Uniform signed edge-difference product.

Equations

• Anderson4D.expandedJGreenDifferenceProduct σ x = ∏ e : Fin n, (Anderson4D.jOriginalGreenEdge x e - Anderson4D.jExtractedShortcutGreenEdge σ x e)

theorem Anderson4D.renormalizedJGreenSkeleton_eq_differenceProduct {n : ℕ} (σ : PartialPairing (Fin n.succ)) : (fun (x : Fin n.succ → T4) => ↑(renormalizedJGreenSkeleton σ x)) = expandedJGreenDifferenceProduct σ

The frozen J Green skeleton is exactly the uniform edge-difference product.

Joint integrability of the signed skeleton

theorem Anderson4D.measurable_jOriginalGreenEdge {n : ℕ} (e : Fin n) : Measurable fun (x : Fin n.succ → T4) => jOriginalGreenEdge x e

theorem Anderson4D.measurable_jExtractedShortcutGreenEdge {n : ℕ} (σ : PartialPairing (Fin n.succ)) (e : Fin n) : Measurable fun (x : Fin n.succ → T4) => jExtractedShortcutGreenEdge σ x e

theorem Anderson4D.measurable_expandedJGreenDifferenceProduct {n : ℕ} (σ : PartialPairing (Fin n.succ)) : Measurable (expandedJGreenDifferenceProduct σ)

theorem Anderson4D.norm_expandedJGreenDifferenceProduct_le {n : ℕ} (σ : PartialPairing (Fin n.succ)) (x : Fin n.succ → T4) : ‖expandedJGreenDifferenceProduct σ x‖ ≤ ‖expandedJGreenMajorant σ x‖

Edgewise triangle inequality between the signed expansion and the nonnegative product-of-sums majorant.

theorem Anderson4D.integrable_renormalizedJGreenSkeleton {n : ℕ} (σ : PartialPairing (Fin n.succ)) : MeasureTheory.Integrable (fun (x : Fin n.succ → T4) => ↑(renormalizedJGreenSkeleton σ x)) (MeasureTheory.Measure.pi fun (x : Fin n.succ) => paperMeasure)

Joint integrability of the signed Green skeleton of every positive- length J tuple.

theorem Anderson4D.integrable_renormalizedJGreenSkeleton_of_pos {n : ℕ} (hn : 0 < n) (σ : PartialPairing (Fin n)) : MeasureTheory.Integrable (fun (x : Fin n → T4) => ↑(renormalizedJGreenSkeleton σ x)) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)

Cardinality-generic positive-length form of integrable_renormalizedJGreenSkeleton.

Bounded covariance factor and the complete J integrand

noncomputable def Anderson4D.detJCovarianceFactor (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (σ : PartialPairing (Fin n)) (x : Fin n → T4) : ℂ

Covariance product of the internal J tuple, in the complex scalar field used for joint integrability.

Equations

• Anderson4D.detJCovarianceFactor ρ ε σ x = ↑(Anderson4D.pairingCovarianceProductOn ρ ε σ Finset.univ x)

theorem Anderson4D.measurable_detJCovarianceFactor (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {n : ℕ} (σ : PartialPairing (Fin n)) : Measurable (detJCovarianceFactor ρ ε σ)

theorem Anderson4D.exists_norm_detJCovarianceFactor_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {n : ℕ} (σ : PartialPairing (Fin n)) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : Fin n → T4), ‖detJCovarianceFactor ρ ε σ x‖ ≤ B

At a fixed positive small scale the complete covariance product is uniformly bounded on the compact tuple space.

theorem Anderson4D.detJintegrand_eq_renormalizedJGreenSkeleton_mul_covariance (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (x : Fin (2 * q) → T4) : ↑(detJintegrand ρ ε q σ x) = ↑(renormalizedJGreenSkeleton σ x) * detJCovarianceFactor ρ ε σ x

Exact complex factorization of the frozen J integrand.

theorem Anderson4D.integrable_detJintegrand_joint (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) : MeasureTheory.Integrable (fun (x : Fin (2 * (q + 1)) → T4) => ↑(detJintegrand ρ ε (q + 1) σ x)) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1))) => paperMeasure)

Joint integrability of every positive-order frozen J integrand in all of its spatial vertices.

def Anderson4D.r322DetJTupleSucc (q : ℕ) (z w : T4) (u : Fin (2 * q) → T4) : Fin (2 * (q + 1)) → T4

The tuple (z,u,w) used by a positive-order J kernel.

Equations

• Anderson4D.r322DetJTupleSucc q z w u j = Anderson4D.assemble z w u (Fin.cast ⋯ j)

@[simp]

theorem Anderson4D.r322DetJTupleSucc_zero (q : ℕ) (z w : T4) (u : Fin (2 * q) → T4) : r322DetJTupleSucc q z w u 0 = z

Fubini coordinates for the two endpoints

noncomputable def Anderson4D.r322FlatAssembleMeasurableEquiv (m : ℕ) : (Fin (m + 2) → T4) ≃ᵐ T4 × T4 × (Fin m → T4)

Split the first and last vertices from a tuple of canonical length m+2. The inverse is assemble.

Equations

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

@[simp]

theorem Anderson4D.r322FlatAssembleMeasurableEquiv_symm_apply (m : ℕ) (x y : T4) (v : Fin m → T4) : (r322FlatAssembleMeasurableEquiv m).symm (x, y, v) = assemble x y v

theorem Anderson4D.measurePreserving_r322FlatAssembleMeasurableEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r322FlatAssembleMeasurableEquiv m)) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))

noncomputable def Anderson4D.r322DetJFlatMeasurableEquiv (q : ℕ) : (Fin (2 * (q + 1)) → T4) ≃ᵐ T4 × T4 × (Fin (2 * q) → T4)

Cast the algebraic cardinality 2(q+1) to the canonical endpoint presentation 2q+2, then split the two endpoints.

Equations

• Anderson4D.r322DetJFlatMeasurableEquiv q = (MeasurableEquiv.piCongrLeft (fun (x : Fin (2 * q + 2)) => Anderson4D.T4) (finCongr ⋯)).trans (Anderson4D.r322FlatAssembleMeasurableEquiv (2 * q))

@[simp]

theorem Anderson4D.r322DetJFlatMeasurableEquiv_symm_apply (q : ℕ) (x y : T4) (v : Fin (2 * q) → T4) : (r322DetJFlatMeasurableEquiv q).symm (x, y, v) = fun (j : Fin (2 * (q + 1))) => assemble x y v (Fin.cast ⋯ j)

theorem Anderson4D.measurePreserving_r322DetJFlatMeasurableEquiv (q : ℕ) : MeasureTheory.MeasurePreserving (⇑(r322DetJFlatMeasurableEquiv q)) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1))) => paperMeasure) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure)))

def Anderson4D.r322MoveMiddleMeasurableEquiv (A : Type u_1) (B : Type u_2) (C : Type u_3) [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] : A × B × C ≃ᵐ B × A × C

Move the terminal endpoint to the front of the flat coordinate triple.

Equations

• Anderson4D.r322MoveMiddleMeasurableEquiv A B C = MeasurableEquiv.prodAssoc.symm.trans ((MeasurableEquiv.prodComm.prodCongr (MeasurableEquiv.refl C)).trans MeasurableEquiv.prodAssoc)

theorem Anderson4D.measurePreserving_r322MoveMiddleMeasurableEquiv {A : Type u_1} {B : Type u_2} {C : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] (μ : MeasureTheory.Measure A) (ν : MeasureTheory.Measure B) (τ : MeasureTheory.Measure C) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite τ] : MeasureTheory.MeasurePreserving (⇑(r322MoveMiddleMeasurableEquiv A B C)) (μ.prod (ν.prod τ)) (ν.prod (μ.prod τ))

@[simp]

theorem Anderson4D.r322MoveMiddleMeasurableEquiv_symm_apply (A : Type u_1) (B : Type u_2) (C : Type u_3) [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] (b : B) (a : A) (c : C) : (r322MoveMiddleMeasurableEquiv A B C).symm (b, a, c) = (a, b, c)

theorem Anderson4D.integrable_detJintegrand_flat_r322 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin (2 * q) → T4)) => detJintegrand ρ ε (q + 1) σ (r322DetJTupleSucc q p.1 p.2.1 p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure)))

Joint integrability in the flat (z,w,v) coordinates used by detJ.

theorem Anderson4D.integrable_detJintegrand_terminalFirst_r322 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin (2 * q) → T4)) => detJintegrand ρ ε (q + 1) σ (r322DetJTupleSucc q p.2.1 p.1 p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure)))

The same joint integrability with the terminal endpoint first.

theorem Anderson4D.exists_integrable_detJintegrand_endpoint_section (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) : ∃ (w : T4), MeasureTheory.Integrable (fun (p : T4 × (Fin (2 * q) → T4)) => detJintegrand ρ ε (q + 1) σ (r322DetJTupleSucc q p.1 w p.2)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure))

Fubini supplies at least one terminal endpoint whose remaining (z,v) section is integrable.

theorem Anderson4D.integrable_detJ_of_endpoint_section (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (w : T4) (hsection : MeasureTheory.Integrable (fun (p : T4 × (Fin (2 * q) → T4)) => detJintegrand ρ ε (q + 1) σ (r322DetJTupleSucc q p.1 w p.2)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure))) : MeasureTheory.Integrable (fun (z : T4) => detJ ρ lam ε (q + 1) σ z w) paperMeasure

Integrability of one raw endpoint section descends through the internal Bochner integral defining detJ.

Translation invariance of the complete J kernel

theorem Anderson4D.assemble_add_const_r322 {n : ℕ} (x y a : T4) (v : Fin n → T4) (j : Fin (n + 2)) : assemble (x + a) (y + a) (fun (i : Fin n) => v i + a) j = assemble x y v j + a

theorem Anderson4D.detJintegrand_add_const_r322 (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (x : Fin (2 * q) → T4) (a : T4) : (detJintegrand ρ ε q σ fun (i : Fin (2 * q)) => x i + a) = detJintegrand ρ ε q σ x

The frozen J integrand contains only differences, so a simultaneous translation of all vertices cancels pointwise.

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

Simultaneously translating both endpoints leaves a J kernel unchanged. The internal variables are reindexed by Haar translation.

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

Difference form of translation invariance.

theorem Anderson4D.integrable_detJ_zero (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q : ℕ) (hq : 1 ≤ q) (σ : PartialPairing (Fin (2 * q))) : MeasureTheory.Integrable (fun (z : T4) => detJ ρ lam ε q σ z 0) paperMeasure

Every positive-order frozen J kernel is genuinely integrable at the fixed endpoint w=0. The exceptional endpoint supplied by Fubini is moved to zero by simultaneous Haar translation.