Complete cell-chain dichotomy for paper §5.1

This file closes the analytic gap between the one-sided estimates in CellSingular.lean and the per-cell chain estimate used in (5.3)--(5.4). The integration order is centred at a selected pivot:

• in the far branch, all variables are integrated from the two endpoints towards a pointwise far edge;
• in the all-near branch, all outer variables are integrated towards the three-edge local convolution proved in LocalTripleScale.lean.

The elementary lattice predicate latticePathAllNear is proved to be complementary to latticePathHasFarEdge; the case split is therefore not an analytic hypothesis in disguise.

The exhaustive lattice case split

def Anderson4D.latticePathAllNear (R : ℝ) (y e : Z4) : List Z4 → Prop

Every edge of the lattice path y :: internal ++ [e] has length at most 4R.

Equations

• Anderson4D.latticePathAllNear R y e [] = (Anderson4D.znorm (y - e) ≤ 4 * R)
• Anderson4D.latticePathAllNear R y e (y' :: ys) = (Anderson4D.znorm (y - y') ≤ 4 * R ∧ Anderson4D.latticePathAllNear R y' e ys)

def Anderson4D.latticePathHasFarEdge (R : ℝ) (y e : Z4) : List Z4 → Prop

At least one edge of the lattice path y :: internal ++ [e] has length at least 4R.

Equations

• Anderson4D.latticePathHasFarEdge R y e [] = (4 * R ≤ Anderson4D.znorm (y - e))
• Anderson4D.latticePathHasFarEdge R y e (y' :: ys) = (4 * R ≤ Anderson4D.znorm (y - y') ∨ Anderson4D.latticePathHasFarEdge R y' e ys)

theorem Anderson4D.latticePath_allNear_or_hasFarEdge (R : ℝ) (y e : Z4) (ys : List Z4) : latticePathAllNear R y e ys ∨ latticePathHasFarEdge R y e ys

The near and far alternatives in the proof of (5.3) cover every lattice path. No geometric alternative is left as an assumption.

def Anderson4D.walkEnd {α : Type u_1} (a : α) : List α → α

Last vertex reached by following a finite path from a starting vertex. This recursive form is convenient when stripping path edges.

Equations

• Anderson4D.walkEnd a [] = a
• Anderson4D.walkEnd a (b :: bs) = Anderson4D.walkEnd b bs

@[simp]

theorem Anderson4D.walkEnd_nil {α : Type u_1} (a : α) : walkEnd a [] = a

@[simp]

theorem Anderson4D.walkEnd_cons {α : Type u_1} (a b : α) (bs : List α) : walkEnd a (b :: bs) = walkEnd b bs

theorem Anderson4D.walkEnd_append {α : Type u_1} (a : α) (xs ys : List α) : walkEnd a (xs ++ ys) = walkEnd (walkEnd a xs) ys

@[simp]

theorem Anderson4D.walkEnd_reverse_cons {α : Type u_1} (a b : α) (bs : List α) : walkEnd a (b :: bs).reverse = b

A pivot-ordered full chain

@[irreducible]

def Anderson4D.twoSidedCellChain (r : ℝ) (x z : T4) : List T4 → List T4 → ℝ

The full chain integral, ordered from both fixed endpoints towards one pivot edge. The path represented by (left,right) is x -- left -- pivot -- reverse right -- z.

This is an honest iterated integral of the chain product, not a numerical majorant.

Equations

• Anderson4D.twoSidedCellChain r x z [] [] = Anderson4D.invSqKer (x - z)
• Anderson4D.twoSidedCellChain r x z (c :: cs) x✝ = ∫ (u : Anderson4D.T4) in Metric.ball c r, Anderson4D.invSqKer (x - u) * Anderson4D.twoSidedCellChain r u z cs x✝ ∂Anderson4D.paperMeasure
• Anderson4D.twoSidedCellChain r x z [] (c :: cs) = ∫ (u : Anderson4D.T4) in Metric.ball c r, Anderson4D.invSqKer (z - u) * Anderson4D.twoSidedCellChain r x u [] cs ∂Anderson4D.paperMeasure

theorem Anderson4D.twoSidedCellChain_nonneg (r : ℝ) (x z : T4) (left right : List T4) : 0 ≤ twoSidedCellChain r x z left right

theorem Anderson4D.twoSidedCellChain_right_nil (r : ℝ) (x z : T4) (left : List T4) : twoSidedCellChain r x z left [] = terminalCellChain r x z left

With no vertices assigned to the right side, the pivot ordering is definitionally the original fixed-terminal chain from CellSingular.lean.

Tonelli-safe chain representation

def Anderson4D.terminalCellLIntegral (r : ℝ) (x z : T4) : List T4 → ENNReal

Nonnegative Lebesgue-integral version of the fixed-terminal chain. Unlike the Bochner integral, it has no junk value when integrability has not yet been established.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.terminalCellLIntegral r x z [] = ENNReal.ofReal (Anderson4D.invSqKer (x - z))

@[irreducible]

def Anderson4D.twoSidedCellLIntegral (r : ℝ) (x z : T4) : List T4 → List T4 → ENNReal

Tonelli-safe version of the two-sided pivot ordering.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.twoSidedCellLIntegral r x z [] [] = ENNReal.ofReal (Anderson4D.invSqKer (x - z))

theorem Anderson4D.measurable_terminalCellLIntegral (r : ℝ) (cs : List T4) : Measurable fun (p : T4 × T4) => terminalCellLIntegral r p.1 p.2 cs

theorem Anderson4D.terminalCellLIntegral_append_singleton (r : ℝ) (x z c : T4) (cs : List T4) : terminalCellLIntegral r x z (cs ++ [c]) = ∫⁻ (u : T4) in Metric.ball c r, ENNReal.ofReal (invSqKer (z - u)) * terminalCellLIntegral r x u cs ∂paperMeasure

Tonelli moves a final integrated vertex to the outside of the fixed-terminal chain. No integrability premise is needed because this is an equality of nonnegative Lebesgue integrals.

theorem Anderson4D.twoSidedCellLIntegral_eq_terminal (r : ℝ) (x z : T4) (left right : List T4) : twoSidedCellLIntegral r x z left right = terminalCellLIntegral r x z (left ++ right.reverse)

Tonelli reordering for the selected pivot. The two-sided integration order is exactly the original fixed-terminal chain on left ++ reverse right. This is unconditional: all swaps took place in ℝ≥0∞ above, before any finiteness or Bochner-integrability claim.

theorem Anderson4D.lintegral_ofReal_mul_le_of_le_const {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {g : α → ENNReal} {K B : ℝ} (hf : MeasureTheory.Integrable f μ) (hfnn : ∀ᵐ (a : α) ∂μ, 0 ≤ f a) (hK : 0 ≤ K) (hB : ∫ (a : α), f a ∂μ ≤ B) (hg : ∀ᵐ (a : α) ∂μ, g a ≤ ENNReal.ofReal K) : ∫⁻ (a : α), ENNReal.ofReal (f a) * g a ∂μ ≤ ENNReal.ofReal (K * B)

A reusable nonnegative one-step estimate. It converts an ordinary integrable kernel bound and a uniform bound on the remaining ℝ≥0∞-chain into a bound for the next Lebesgue integral.

@[irreducible]

def Anderson4D.latticeTwoSidedPathWeight (y e : Z4) : List Z4 → List Z4 → ℝ

Lattice product along the same pivot-ordered path, including the pivot edge.

Equations

• Anderson4D.latticeTwoSidedPathWeight y e [] [] = Anderson4D.latticeEdgeWeight y e
• Anderson4D.latticeTwoSidedPathWeight y e (y' :: ys) x✝ = Anderson4D.latticeEdgeWeight y y' * Anderson4D.latticeTwoSidedPathWeight y' e ys x✝
• Anderson4D.latticeTwoSidedPathWeight y e [] (e' :: es) = Anderson4D.latticeEdgeWeight e e' * Anderson4D.latticeTwoSidedPathWeight y e' [] es

theorem Anderson4D.latticeEdgeWeight_nonneg_complete (y e : Z4) : 0 ≤ latticeEdgeWeight y e

theorem Anderson4D.latticeTwoSidedPathWeight_nonneg (y e : Z4) (left right : List Z4) : 0 ≤ latticeTwoSidedPathWeight y e left right

def Anderson4D.LatticeTwoSidedNoWrap (ε : ℝ) (y e : Z4) (left right : List Z4) : Prop

Exact no-wrapping data for all integrated outer edges and for the remaining pivot edge.

Equations

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

def Anderson4D.LatticeTwoSidedPivotFar (R : ℝ) (y e : Z4) (left right : List Z4) : Prop

The selected pivot is a far edge.

Equations

• Anderson4D.LatticeTwoSidedPivotFar R y e left right = (4 * R ≤ Anderson4D.znorm (Anderson4D.walkEnd y left - Anderson4D.walkEnd e right))

theorem Anderson4D.latticePathHasFarEdge_exists_twoSidedPivot {R : ℝ} {y e : Z4} {ys : List Z4} (h : latticePathHasFarEdge R y e ys) : ∃ (left : List Z4) (right : List Z4), ys = left ++ right.reverse ∧ LatticeTwoSidedPivotFar R y e left right

A far edge in a linearly ordered path can be selected as the central edge of a two-sided pivot ordering. Together with latticePath_allNear_or_hasFarEdge, this removes the last possible "assume a suitable pivot exists" shortcut from the (5.3) reduction.

theorem Anderson4D.latticePath_allNear_or_exists_twoSidedPivot (R : ℝ) (y e : Z4) (ys : List Z4) : latticePathAllNear R y e ys ∨ ∃ (left : List Z4) (right : List Z4), ys = left ++ right.reverse ∧ LatticeTwoSidedPivotFar R y e left right

Final exhaustive form used by the analytic assembly: either every edge is near, or the same internal path has a concrete two-sided decomposition with a far central pivot.

Extracting the all-near three-edge core

theorem Anderson4D.exists_eq_append_pair_of_two_le_length {α : Type u_1} {xs : List α} (h : 2 ≤ xs.length) : ∃ (pre : List α) (a : α) (b : α), xs = pre ++ [a, b]

A path with at least two internal vertices has a unique-enough decomposition into an outer prefix and its final two vertices.

theorem Anderson4D.latticeCellPathNoWrap_append_iff (ε : ℝ) (y : Z4) (xs zs : List Z4) : LatticeCellPathNoWrap ε y (xs ++ zs) ↔ LatticeCellPathNoWrap ε y xs ∧ LatticeCellPathNoWrap ε (walkEnd y xs) zs

Splitting a no-wrap path at a list append.

theorem Anderson4D.latticeCellPathNoWrap_reverse_endpoint (ε : ℝ) (p e : Z4) (right : List Z4) (hnowrap : LatticeCellPathNoWrap ε p (right.reverse ++ [e])) : LatticeCellPathNoWrap ε e right ∧ dist (latticeTorusCenter ε p) (latticeTorusCenter ε (walkEnd e right)) = ε * znorm (p - walkEnd e right)

Reverse a no-wrap segment whose final endpoint is exposed. Besides the reversed outer path, the conclusion records the final (pivot) edge with exactly the orientation used by LatticeTwoSidedNoWrap.

theorem Anderson4D.latticePathHasFarEdge_exists_twoSidedGeometry {ε R : ℝ} {y e : Z4} {ys : List Z4} (hfar : latticePathHasFarEdge R y e ys) (hnowrap : LatticeCellPathNoWrap ε y (ys ++ [e])) : ∃ (left : List Z4) (right : List Z4), ys = left ++ right.reverse ∧ LatticeTwoSidedNoWrap ε y e left right ∧ LatticeTwoSidedPivotFar R y e left right

A far edge selected from an actual no-wrap full path carries all the geometry needed by the two-sided analytic estimate.

theorem Anderson4D.latticePath_allNear_or_exists_twoSidedGeometry (ε R : ℝ) (y e : Z4) (ys : List Z4) (hnowrap : LatticeCellPathNoWrap ε y (ys ++ [e])) : latticePathAllNear R y e ys ∨ ∃ (left : List Z4) (right : List Z4), ys = left ++ right.reverse ∧ LatticeTwoSidedNoWrap ε y e left right ∧ LatticeTwoSidedPivotFar R y e left right

Exhaustive geometric split for one actual no-wrap lattice path. The near branch is the original latticePathAllNear predicate; the far branch contains a concrete decomposition and no extra geometric assumptions.

theorem Anderson4D.latticePathAllNear_append_pair {R : ℝ} {y e a b : Z4} {pre : List Z4} (h : latticePathAllNear R y e (pre ++ [a, b])) : znorm (walkEnd y pre - a) ≤ 4 * R ∧ znorm (a - b) ≤ 4 * R ∧ znorm (b - e) ≤ 4 * R

If an all-near path is written with its final two internal vertices exposed, its last three edges are 4R-near.

The far-pivot estimate

theorem Anderson4D.twoSidedLatticeCellChain_le_of_far : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (left right : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedNoWrap ε y e left right → LatticeTwoSidedPivotFar R y e left right → twoSidedCellChain (R * ε) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ (C * (R ^ 2 + R ^ 4)) ^ (left.length + right.length) * ε ^ (2 * (left.length + right.length)) * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTwoSidedPathWeight y e left right

A far pivot with k integrated vertices gives k ordinary ε²⟨Δy⟩⁻² factors and one pointwise ε⁻²⟨Δy⟩⁻² factor. This is the general (pivot-at-an-arbitrary-edge) form of the far branch in (5.3).

Tonelli-safe far estimate

@[irreducible]

def Anderson4D.latticeFarChainMajorant (C ε R : ℝ) (y e : Z4) : List Z4 → List Z4 → ℝ

Recursive real majorant for the far-pivot chain. Its recursive shape matches the two-sided Lebesgue integral exactly.

Equations

• Anderson4D.latticeFarChainMajorant C ε R y e [] [] = Anderson4D.terminalRadiusFactor R * (ε ^ 2)⁻¹ * Anderson4D.latticeEdgeWeight y e
• Anderson4D.latticeFarChainMajorant C ε R y e (y' :: ys) x✝ = C * (R ^ 2 + R ^ 4) * ε ^ 2 * Anderson4D.latticeEdgeWeight y y' * Anderson4D.latticeFarChainMajorant C ε R y' e ys x✝
• Anderson4D.latticeFarChainMajorant C ε R y e [] (e' :: es) = C * (R ^ 2 + R ^ 4) * ε ^ 2 * Anderson4D.latticeEdgeWeight e e' * Anderson4D.latticeFarChainMajorant C ε R y e' [] es

theorem Anderson4D.latticeFarChainMajorant_nonneg {C R : ℝ} (hC : 0 ≤ C) (hR : 0 < R) (ε : ℝ) (y e : Z4) (left right : List Z4) : 0 ≤ latticeFarChainMajorant C ε R y e left right

theorem Anderson4D.latticeFarChainMajorant_eq_closed (C ε R : ℝ) (y e : Z4) (left right : List Z4) : latticeFarChainMajorant C ε R y e left right = (C * (R ^ 2 + R ^ 4)) ^ (left.length + right.length) * ε ^ (2 * (left.length + right.length)) * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTwoSidedPathWeight y e left right

theorem Anderson4D.twoSidedCellLIntegral_le_of_far : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (left right : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedNoWrap ε y e left right → LatticeTwoSidedPivotFar R y e left right → twoSidedCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ ENNReal.ofReal (latticeFarChainMajorant C ε R y e left right)

Far-pivot bound for the Tonelli-safe integral. Consequently the selected pivot order is finite, and twoSidedCellLIntegral_eq_terminal transports the same bound to the original chain order.

theorem Anderson4D.twoSidedCellLIntegral_le_of_far_closed : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (left right : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedNoWrap ε y e left right → LatticeTwoSidedPivotFar R y e left right → twoSidedCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ (left.length + right.length) * ε ^ (2 * (left.length + right.length)) * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTwoSidedPathWeight y e left right)

Closed-form version of the Tonelli-safe far estimate. This is the same recursive estimate as twoSidedCellLIntegral_le_of_far, with every ordinary cell edge expanded and the powers collected.

theorem Anderson4D.terminalCellLIntegral_le_of_far_decomposition : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (ys left right : List Z4) (x z : T4), ys = left ++ right.reverse → x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedNoWrap ε y e left right → LatticeTwoSidedPivotFar R y e left right → terminalCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) ys) ≤ ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ (left.length + right.length) * ε ^ (2 * (left.length + right.length)) * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTwoSidedPathWeight y e left right)

The far-pivot estimate in the original fixed-terminal order. The only reordering step is the unconditional Tonelli identity twoSidedCellLIntegral_eq_terminal; no Bochner-integrability premise is silently introduced.

theorem Anderson4D.twoSidedLatticeCellChain_order_le_of_far : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 2 ≤ n → ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (left right : List Z4) (x z : T4), left.length + right.length = 2 * n - 2 → x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedNoWrap ε y e left right → LatticeTwoSidedPivotFar R y e left right → twoSidedCellChain (R * ε) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ (C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * ε ^ (4 * n - 6) * latticeTwoSidedPathWeight y e left right

Paper-order form of the far-pivot estimate. For the 2n-2 integrated vertices in (5.3), the exposed scale is exactly ε^(4n-6).

The all-near local-triple branch

noncomputable def Anderson4D.localTripleCellLIntegral (r : ℝ) (c₁ c₂ x y : T4) : ENNReal

Nonnegative Lebesgue-integral version of the local three-edge core. This is the object to which Tonelli/Fubini is applied; in particular it does not inherit the junk value of a non-integrable Bochner integral.

Equations

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

theorem Anderson4D.integrable_localTripleProduct (x y : T4) : MeasureTheory.Integrable (Anderson4D.localTripleProduct✝ x y) (paperMeasure.prod paperMeasure)

The local triple product is genuinely integrable on the product torus. The proof uses the public 3/2-power AM--GM majorant, so the subsequent identification of Bochner and Lebesgue integrals is not a junk-value inference.

theorem Anderson4D.localTripleCellLIntegral_eq_ofReal (r : ℝ) (c₁ c₂ x y : T4) : localTripleCellLIntegral r c₁ c₂ x y = ENNReal.ofReal (localTripleCellIntegral r c₁ c₂ x y)

The Tonelli-safe local core is the ofReal of the paper's ordinary iterated integral. Product integrability is proved above before either application of Fubini.

theorem Anderson4D.localTripleCellLIntegral_le_scale : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (c₀ c₁ c₂ c₃ x y : T4), x ∈ Metric.ball c₀ r → y ∈ Metric.ball c₃ r → dist c₀ c₁ ≤ 4 * r → dist c₁ c₂ ≤ 4 * r → dist c₂ c₃ ≤ 4 * r → localTripleCellLIntegral r c₁ c₂ x y ≤ ENNReal.ofReal (C * r ^ 2)

Scale estimate for the Tonelli-safe local core.

theorem Anderson4D.terminalCellLIntegral_pair_eq_localTriple (r : ℝ) (c₁ c₂ x y : T4) : terminalCellLIntegral r x y [c₁, c₂] = localTripleCellLIntegral r c₁ c₂ x y

The two-vertex terminal chain is exactly the Tonelli-safe local three-edge core.

Lattice geometry for the all-near core

@[irreducible]

def Anderson4D.latticeTwoSidedTripleWeight (y a b e : Z4) : List Z4 → List Z4 → ℝ

Lattice product of all edges in a chain with a three-edge central core.

Equations

• Anderson4D.latticeTwoSidedTripleWeight y a b e [] [] = Anderson4D.latticeEdgeWeight y a * Anderson4D.latticeEdgeWeight a b * Anderson4D.latticeEdgeWeight b e
• Anderson4D.latticeTwoSidedTripleWeight y a b e (y' :: ys) x✝ = Anderson4D.latticeEdgeWeight y y' * Anderson4D.latticeTwoSidedTripleWeight y' a b e ys x✝
• Anderson4D.latticeTwoSidedTripleWeight y a b e [] (e' :: es) = Anderson4D.latticeEdgeWeight e e' * Anderson4D.latticeTwoSidedTripleWeight y a b e' [] es

theorem Anderson4D.latticeTwoSidedTripleWeight_nonneg (y a b e : Z4) (left right : List Z4) : 0 ≤ latticeTwoSidedTripleWeight y a b e left right

def Anderson4D.LatticeNearEdge (ε R : ℝ) (y y' : Z4) : Prop

One no-wrapping, 4R-near lattice edge.

Equations

• Anderson4D.LatticeNearEdge ε R y y' = (dist (Anderson4D.latticeTorusCenter ε y) (Anderson4D.latticeTorusCenter ε y') = ε * Anderson4D.znorm (y - y') ∧ Anderson4D.znorm (y - y') ≤ 4 * R)

def Anderson4D.LatticeTripleNear (ε R : ℝ) (y a b e : Z4) : Prop

Exact geometric data for an all-near central triple after the outer edges have been stripped.

Equations

• Anderson4D.LatticeTripleNear ε R y a b e = (Anderson4D.LatticeNearEdge ε R y a ∧ Anderson4D.LatticeNearEdge ε R a b ∧ Anderson4D.LatticeNearEdge ε R b e)

def Anderson4D.LatticeTwoSidedTripleGeometry (ε R : ℝ) (y a b e : Z4) (left right : List Z4) : Prop

No-wrapping data on the outer paths and near data on the central triple.

Equations

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

theorem Anderson4D.latticePathAllNear_exists_tripleGeometry {ε R : ℝ} {y e : Z4} {ys : List Z4} (hlen : 2 ≤ ys.length) (hnear : latticePathAllNear R y e ys) (hnowrap : LatticeCellPathNoWrap ε y (ys ++ [e])) : ∃ (pre : List Z4) (a : Z4) (b : Z4), ys = pre ++ [a, b] ∧ LatticeTwoSidedTripleGeometry ε R y a b e pre []

All-near core extraction. For at least two internal vertices, the actual latticePathAllNear predicate and the actual no-wrap path produce the exact (prefix,a,b) geometry consumed by the local-triple estimate.

def Anderson4D.cellChainRadiusFactor (R : ℝ) : ℝ

Radius factor which absorbs both an ordinary integrated edge and the three near central lattice denominators.

Equations

• Anderson4D.cellChainRadiusFactor R = R ^ 2 + R ^ 4 + R ^ 2 * (1 + (4 * R) ^ 2) ^ 3 + 1

theorem Anderson4D.cellChainRadiusFactor_pos (R : ℝ) : 0 < cellChainRadiusFactor R

def Anderson4D.latticeNearChainMajorant (C ε R : ℝ) (y a b e : Z4) : List Z4 → ℝ

Recursive majorant for a one-sided all-near chain. Its base is the three-edge local core and every recursive layer is one ordinary cell edge.

Equations

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

theorem Anderson4D.latticeNearChainMajorant_nonneg {C : ℝ} (hC : 0 ≤ C) (ε R : ℝ) (y a b e : Z4) (left : List Z4) : 0 ≤ latticeNearChainMajorant C ε R y a b e left

theorem Anderson4D.latticeNearChainMajorant_eq_closed (C ε R : ℝ) (y a b e : Z4) (left : List Z4) : latticeNearChainMajorant C ε R y a b e left = (C * cellChainRadiusFactor R) ^ (left.length + 1) * ε ^ (2 * left.length + 2) * latticeTwoSidedTripleWeight y a b e left []

theorem Anderson4D.latticeEdgeWeight_comm (y e : Z4) : latticeEdgeWeight y e = latticeEdgeWeight e y

theorem Anderson4D.latticeTerminalPathWeight_append_singleton (y e c : Z4) (ys : List Z4) : latticeTerminalPathWeight y e (ys ++ [c]) = latticeTerminalPathWeight y c ys * latticeEdgeWeight c e

theorem Anderson4D.latticeTwoSidedPathWeight_eq_terminal (y e : Z4) (left right : List Z4) : latticeTwoSidedPathWeight y e left right = latticeTerminalPathWeight y e (left ++ right.reverse)

The pivot-ordered lattice product is the product along the original linear path.

theorem Anderson4D.latticeTwoSidedTripleWeight_eq_terminal (y a b e : Z4) (left : List Z4) : latticeTwoSidedTripleWeight y a b e left [] = latticeTerminalPathWeight y e (left ++ [a, b])

The three-edge-core lattice product is likewise the product along the original one-sided path.

theorem Anderson4D.terminalCellLIntegral_le_of_nearCore : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y a b e : Z4) (left : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedTripleGeometry ε R y a b e left [] → terminalCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) (left ++ [a, b])) ≤ ENNReal.ofReal (latticeNearChainMajorant C ε R y a b e left)

Tonelli-safe all-near estimate in the original terminal-chain order. The actual triple geometry, including the no-wrap prefix, is consumed recursively.

theorem Anderson4D.terminalCellLIntegral_le_of_nearCore_closed : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y a b e : Z4) (left : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedTripleGeometry ε R y a b e left [] → terminalCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) (left ++ [a, b])) ≤ ENNReal.ofReal ((C * cellChainRadiusFactor R) ^ (left.length + 1) * ε ^ (2 * left.length + 2) * latticeTwoSidedTripleWeight y a b e left [])

Closed paper-style form of the Tonelli-safe all-near estimate.

noncomputable def Anderson4D.exhaustiveCellChainMajorant (C ε R : ℝ) (k : ℕ) (weight : ℝ) : ENNReal

A single per-cell majorant containing both exhaustive alternatives. The first summand is the far-pivot estimate and the second is the all-near local-triple estimate. For paths of length at least two both summands have the paper scale ε^(2k-2) after cancellation in the first summand.

Equations

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

theorem Anderson4D.terminalCellLIntegral_exhaustive_perCell : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (ys : List Z4) (x z : T4), 2 ≤ ys.length → x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeCellPathNoWrap ε y (ys ++ [e]) → terminalCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) ys) ≤ exhaustiveCellChainMajorant C ε R ys.length (latticeTerminalPathWeight y e ys)

Exhaustive Tonelli-safe per-cell chain estimate.

For one actual no-wrap cell path with at least two integrated vertices, this theorem itself performs the all-near/has-far-edge split. The near branch extracts the concrete (pre,a,b) core from latticePathAllNear; the far branch extracts a two-sided pivot together with its no-wrap geometry. Both branches bound the same original terminalCellLIntegral and the same original linear lattice weight.

theorem Anderson4D.exhaustiveCellChainMajorant_eq_paperScale {ε : ℝ} (hε : ε ≠ 0) (C R weight : ℝ) (k : ℕ) (hk : 1 ≤ k) : exhaustiveCellChainMajorant C ε R k weight = ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ k * terminalRadiusFactor R * ε ^ (2 * k - 2) * weight) + ENNReal.ofReal ((C * cellChainRadiusFactor R) ^ (k - 1) * ε ^ (2 * k - 2) * weight)

Cancellation of the terminal ε⁻² factor in the exhaustive majorant.

theorem Anderson4D.terminalCellLIntegral_exhaustive_order : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 2 ≤ n → ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (ys : List Z4) (x z : T4), ys.length = 2 * n - 2 → x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeCellPathNoWrap ε y (ys ++ [e]) → terminalCellLIntegral (R * ε) x z (List.map (latticeTorusCenter ε) ys) ≤ ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * ε ^ (4 * n - 6) * latticeTerminalPathWeight y e ys) + ENNReal.ofReal ((C * cellChainRadiusFactor R) ^ (2 * n - 3) * ε ^ (4 * n - 6) * latticeTerminalPathWeight y e ys)

Paper-order specialization of the exhaustive per-cell estimate. For 2n-2 integrated vertices, both exhaustive summands expose exactly ε^(4n-6).

@[irreducible]

def Anderson4D.twoSidedTripleCellChain (r : ℝ) (a b x z : T4) : List T4 → List T4 → ℝ

Chain obtained after selecting the two central integrated vertices a,b; all other integrated vertices are ordered outwards towards the two fixed endpoints.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.twoSidedTripleCellChain r a b x z [] [] = Anderson4D.localTripleCellIntegral r a b x z

theorem Anderson4D.twoSidedTripleCellChain_nonneg (r : ℝ) (a b x z : T4) (left right : List T4) : 0 ≤ twoSidedTripleCellChain r a b x z left right

theorem Anderson4D.twoSidedTripleCellChain_right_nil (r : ℝ) (a b x z : T4) (left : List T4) : twoSidedTripleCellChain r a b x z left [] = terminalCellChain r x z (left ++ [a, b])

In the one-sided orientation the local-triple construction is exactly the ordinary terminal chain with the two central vertices appended.

theorem Anderson4D.twoSidedTripleLatticeCellChain_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y a b e : Z4) (left right : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedTripleGeometry ε R y a b e left right → twoSidedTripleCellChain (R * ε) (latticeTorusCenter ε a) (latticeTorusCenter ε b) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ (C * cellChainRadiusFactor R) ^ (left.length + right.length + 1) * ε ^ (2 * (left.length + right.length) + 2) * latticeTwoSidedTripleWeight y a b e left right

Complete all-near branch of (5.4), with the local triple theorem consumed at the base and every outer cell integrated explicitly.

theorem Anderson4D.twoSidedTripleLatticeCellChain_order_le : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 2 ≤ n → ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y a b e : Z4) (left right : List Z4) (x z : T4), left.length + right.length + 2 = 2 * n - 2 → x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTwoSidedTripleGeometry ε R y a b e left right → twoSidedTripleCellChain (R * ε) (latticeTorusCenter ε a) (latticeTorusCenter ε b) x z (List.map (latticeTorusCenter ε) left) (List.map (latticeTorusCenter ε) right) ≤ (C * cellChainRadiusFactor R) ^ (2 * n - 3) * ε ^ (4 * n - 6) * latticeTwoSidedTripleWeight y a b e left right

Paper-order form of the all-near branch. The two central variables and all outer variables total 2n-2, hence the local-triple scale and the outer ε² factors again give exactly ε^(4n-6).