Singular-chain bounds on individual cells

This file supplies the analytic interface between the torus singular kernel and the lattice cells of paper §5.1. The main ingredients are:

• a translation-uniform O(r²) bound for one inverse-square kernel on a torus ball;
• the corresponding bound on a lattice-cell neighbourhood;
• a far-cell pointwise estimate, with the scale and centre separation kept explicit.

These are genuine consequences of setIntegral_invSqKer_ball_le and the cell geometry. In particular, none of the statements below assumes the desired (5.3) cell integral as a hypothesis.

Translated ball estimates

noncomputable def Anderson4D.invSqKerBallIntegral (x : T4) (r : ℝ) : ℝ

The inverse-square kernel integrated on a metric ball centred at its singularity.

Equations

• Anderson4D.invSqKerBallIntegral x r = ∫ (z : Anderson4D.T4) in Metric.ball x r, Anderson4D.invSqKer (x - z) ∂Anderson4D.paperMeasure

theorem Anderson4D.measurableSet_torusDistSq_sub_le (x : T4) (r : ℝ) : MeasurableSet {z : T4 | torusDistSq (x - z) ≤ r ^ 2}

theorem Anderson4D.setIntegral_invSqKer_sub_torusDistSq_le (x : T4) (r : ℝ) : ∫ (z : T4) in {z : T4 | torusDistSq (x - z) ≤ r ^ 2}, invSqKer (x - z) ∂paperMeasure = ∫ (z : T4) in {z : T4 | torusDistSq z ≤ r ^ 2}, invSqKer z ∂paperMeasure

Translation of the centred torusDistSq ball does not change the inverse-square integral.

theorem Anderson4D.invSqKerBallIntegral_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4) (r : ℝ), 0 < r → invSqKerBallIntegral x r ≤ C * r ^ 2

Uniform local mass. A translated metric ball of radius r carries at most C r² inverse-square mass. The factor 4 converting the product sup norm to torusDistSq is absorbed into the named constant.

theorem Anderson4D.paperMeasure_singleton (x : T4) : paperMeasure {x} = 0

theorem Anderson4D.paperMeasure_ball_toReal_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4) (r : ℝ), 0 < r → (paperMeasure (Metric.ball x r)).toReal ≤ C * r ^ 4

Metric balls on the paper torus have the expected four-dimensional volume growth. This is derived from the inverse-square ball estimate: away from the null centre, 1 ≤ 4r² |x-z|⁻² on B(x,r).

A scale-sensitive one-edge estimate

theorem Anderson4D.invSqKer_le_inv_sq_norm_cell (w : T4) : invSqKer w ≤ (‖w‖ ^ 2)⁻¹

Public norm comparison for the model inverse-square kernel.

theorem Anderson4D.invSqKer_sub_le_of_mem_balls_of_far {c d x z : T4} {r : ℝ} (hr : 0 < r) (hx : x ∈ Metric.ball c r) (hz : z ∈ Metric.ball d r) (hfar : 4 * r ≤ dist c d) : invSqKer (x - z) ≤ 4 * (dist c d ^ 2)⁻¹

If two radius-r cells have centres at distance at least 4r, the kernel between any two points in the cells is controlled by the inverse square centre distance.

noncomputable def Anderson4D.metricCellEdgeWeight (r : ℝ) (c d : T4) : ℝ

The scale-sensitive edge weight generated by integrating one inverse-square factor over a radius-r cell.

Equations

• Anderson4D.metricCellEdgeWeight r c d = r ^ 4 / (r ^ 2 + dist c d ^ 2)

theorem Anderson4D.metricCellEdgeWeight_nonneg (r : ℝ) (c d : T4) : 0 ≤ metricCellEdgeWeight r c d

theorem Anderson4D.invSqKer_cellEdge_le : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (c d x : T4), x ∈ Metric.ball c r → ∫ (z : T4) in Metric.ball d r, invSqKer (x - z) ∂paperMeasure ≤ C * metricCellEdgeWeight r c d

One-cell edge bound. Uniformly for x ∈ B(c,r),

∫_{B(d,r)} |x-z|⁻² dz ≲ r⁴ / (r² + dist(c,d)²).

This combines the local O(r²) singular mass with the far-cell pointwise bound and four-dimensional cell volume.

Non-cyclic chains with every target cell integrated

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

A left-to-right chain in which every vertex listed in centres is integrated over its radius-r cell. The empty chain has value 1.

Equations

• Anderson4D.integratedCellChain r x [] = 1
• Anderson4D.integratedCellChain r x (d :: ds) = ∫ (z : Anderson4D.T4) in Metric.ball d r, Anderson4D.invSqKer (x - z) * Anderson4D.integratedCellChain r z ds ∂Anderson4D.paperMeasure

def Anderson4D.metricCellPathWeight (r : ℝ) (c : T4) : List T4 → ℝ

Product of the scale-sensitive edge weights along the same path of cell centres.

Equations

• Anderson4D.metricCellPathWeight r c [] = 1
• Anderson4D.metricCellPathWeight r c (d :: ds) = Anderson4D.metricCellEdgeWeight r c d * Anderson4D.metricCellPathWeight r d ds

theorem Anderson4D.metricCellPathWeight_nonneg (r : ℝ) (c : T4) (centres : List T4) : 0 ≤ metricCellPathWeight r c centres

theorem Anderson4D.integratedCellChain_nonneg (r : ℝ) (x : T4) (centres : List T4) : 0 ≤ integratedCellChain r x centres

theorem Anderson4D.integratedCellChain_le : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (c x : T4) (centres : List T4), x ∈ Metric.ball c r → integratedCellChain r x centres ≤ C ^ centres.length * metricCellPathWeight r c centres

Iterated non-cyclic cell collapse. Each integrated vertex costs one factor C · r⁴/(r²+d²). This is the exact induction used on either side of a pivot edge in the large-separation branch of paper (5.3).

A fixed terminal vertex and a far pivot edge

def Anderson4D.terminalCellChain (r : ℝ) (x y : T4) : List T4 → ℝ

A non-cyclic chain whose final vertex y is fixed rather than integrated.

Equations

• Anderson4D.terminalCellChain r x y [] = Anderson4D.invSqKer (x - y)
• Anderson4D.terminalCellChain r x y (d :: ds) = ∫ (z : Anderson4D.T4) in Metric.ball d r, Anderson4D.invSqKer (x - z) * Anderson4D.terminalCellChain r z y ds ∂Anderson4D.paperMeasure

def Anderson4D.TerminalEdgeFar (r : ℝ) (c e : T4) : List T4 → Prop

The final edge of the path is separated by at least 4r.

Equations

• Anderson4D.TerminalEdgeFar r c e [] = (4 * r ≤ dist c e)
• Anderson4D.TerminalEdgeFar r c e (d :: ds) = Anderson4D.TerminalEdgeFar r d e ds

def Anderson4D.metricTerminalPathWeight (r : ℝ) (c e : T4) : List T4 → ℝ

Product of integrated edge weights, followed by the pointwise inverse-square weight of the fixed terminal edge.

Equations

• Anderson4D.metricTerminalPathWeight r c e [] = 4 * (dist c e ^ 2)⁻¹
• Anderson4D.metricTerminalPathWeight r c e (d :: ds) = Anderson4D.metricCellEdgeWeight r c d * Anderson4D.metricTerminalPathWeight r d e ds

theorem Anderson4D.metricTerminalPathWeight_nonneg (r : ℝ) (c e : T4) (centres : List T4) : 0 ≤ metricTerminalPathWeight r c e centres

theorem Anderson4D.terminalCellChain_nonneg (r : ℝ) (x y : T4) (centres : List T4) : 0 ≤ terminalCellChain r x y centres

theorem Anderson4D.terminalCellChain_le_of_far : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (c e x y : T4) (centres : List T4), x ∈ Metric.ball c r → y ∈ Metric.ball e r → TerminalEdgeFar r c e centres → terminalCellChain r x y centres ≤ C ^ centres.length * metricTerminalPathWeight r c e centres

Far-pivot chain bound. If the last edge of a non-cyclic cell path is 4r-separated, all preceding vertices can be integrated successively. For k integrated vertices this has scale r^(2k) · d_pivot⁻².

The isolated all-near scaling lemma

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

The three-edge, two-variable cell integral left after stripping all outer edges in the all-near branch of (5.4).

Equations

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

def Anderson4D.LocalTripleCellScaleBound : Prop

Exact remaining scale-covariant analytic input for the all-near case. Unlike a hypothesis restating (5.3), this is only the three-edge local convolution isolated by the proved path-collapse lemmas above. The global unscaled analogue is triple_conv_invSqKer_le; closing this predicate requires a torus-to-Euclidean dilation/periodization lemma.

Equations

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

Lattice-centred cell neighbourhoods

noncomputable def Anderson4D.latticeTorusCenter (ε : ℝ) (y : Z4) : T4

The torus point represented by the Euclidean lattice centre εy.

Equations

• Anderson4D.latticeTorusCenter ε y = Anderson4D.periodizeR4 (Anderson4D.cellRepresentative ε y)

def Anderson4D.latticeCellNeighborhood (ε R : ℝ) (y : Z4) : Set T4

An Rε-neighbourhood of the lattice centre. The paper uses a fixed absolute R; keeping it explicit records the cutoff-support dependence.

Equations

• Anderson4D.latticeCellNeighborhood ε R y = Metric.ball (Anderson4D.latticeTorusCenter ε y) (R * ε)

theorem Anderson4D.measurableSet_latticeCellNeighborhood (ε R : ℝ) (y : Z4) : MeasurableSet (latticeCellNeighborhood ε R y)

theorem Anderson4D.invSqKer_integral_latticeCellNeighborhood_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y : Z4), ∀ x ∈ latticeCellNeighborhood ε R y, ∫ (z : T4) in latticeCellNeighborhood ε R y, invSqKer (x - z) ∂paperMeasure ≤ C * R ^ 2 * ε ^ 2

theorem Anderson4D.metricCellEdgeWeight_lattice_le {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) (y y' : Z4) (hcenter : dist (latticeTorusCenter ε y) (latticeTorusCenter ε y') = ε * znorm (y - y')) : metricCellEdgeWeight (R * ε) (latticeTorusCenter ε y) (latticeTorusCenter ε y') ≤ (R ^ 2 + R ^ 4) * ε ^ 2 * latticeEdgeWeight y y'

On a pair of cells whose chosen Euclidean representatives do not wrap around the torus, the metric cell weight is bounded by the exact lattice edge weight from (5.3). The explicit equality hypothesis is precisely the periodic-boundary interface; no analytic estimate is hidden in it.

theorem Anderson4D.invSqKer_latticeCellEdge_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y y' : Z4) (x : T4), dist (latticeTorusCenter ε y) (latticeTorusCenter ε y') = ε * znorm (y - y') → x ∈ latticeCellNeighborhood ε R y → ∫ (z : T4) in latticeCellNeighborhood ε R y', invSqKer (x - z) ∂paperMeasure ≤ C * (R ^ 2 + R ^ 4) * ε ^ 2 * latticeEdgeWeight y y'

Lattice specialization of invSqKer_cellEdge_le. It proves the single-step factor ε²⟨y-y'⟩⁻² used when integrating a non-pivot edge in paper (5.3), with the support-radius dependence explicit.

Lattice paths and the explicit ε ledger

def Anderson4D.latticeCellPathWeight (y : Z4) : List Z4 → ℝ

Product of the paper's lattice edge weights along a finite path.

Equations

• Anderson4D.latticeCellPathWeight y [] = 1
• Anderson4D.latticeCellPathWeight y (y' :: ys) = Anderson4D.latticeEdgeWeight y y' * Anderson4D.latticeCellPathWeight y' ys

theorem Anderson4D.latticeCellPathWeight_nonneg (y : Z4) (ys : List Z4) : 0 ≤ latticeCellPathWeight y ys

def Anderson4D.LatticeCellPathNoWrap (ε : ℝ) (y : Z4) : List Z4 → Prop

No periodic wrapping along a path of chosen Euclidean cell representatives. This is the sole geometric interface needed to identify torus centre distance with ε · znorm; it is not an analytic bound.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.LatticeCellPathNoWrap ε y [] = True

theorem Anderson4D.metricCellPathWeight_lattice_le {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) (y : Z4) (ys : List Z4) (hnowrap : LatticeCellPathNoWrap ε y ys) : metricCellPathWeight (R * ε) (latticeTorusCenter ε y) (List.map (latticeTorusCenter ε) ys) ≤ ((R ^ 2 + R ^ 4) * ε ^ 2) ^ ys.length * latticeCellPathWeight y ys

theorem Anderson4D.integratedLatticeCellChain_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y : Z4) (ys : List Z4) (x : T4), LatticeCellPathNoWrap ε y ys → x ∈ latticeCellNeighborhood ε R y → integratedCellChain (R * ε) x (List.map (latticeTorusCenter ε) ys) ≤ (C * (R ^ 2 + R ^ 4)) ^ ys.length * ε ^ (2 * ys.length) * latticeCellPathWeight y ys

Explicit non-cyclic ε scaling. Integrating k consecutive vertices over their Rε cells gives

(C(R²+R⁴))ᵏ ε^(2k) ∏⟨Δy⟩⁻².

For the 2n-2 internal vertices of (5.3), this supplies the complete ε^(4n-4) ledger away from the single pivot edge. A far pivot contributes the remaining ε⁻²; the all-near pivot is exactly the local triple- convolution branch of (5.4).

Fixed terminal lattice path: the ε^(4n-6) branch of (5.3)

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

Lattice product including the fixed terminal edge.

Equations

• Anderson4D.latticeTerminalPathWeight y e [] = Anderson4D.latticeEdgeWeight y e
• Anderson4D.latticeTerminalPathWeight y e (y' :: ys) = Anderson4D.latticeEdgeWeight y y' * Anderson4D.latticeTerminalPathWeight y' e ys

theorem Anderson4D.latticeTerminalPathWeight_nonneg (y e : Z4) (ys : List Z4) : 0 ≤ latticeTerminalPathWeight y e ys

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

Along every integrated edge the chosen representatives do not wrap; the final edge additionally has lattice separation at least 4R.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.LatticeTerminalPathFar ε R y e [] = (dist (Anderson4D.latticeTorusCenter ε y) (Anderson4D.latticeTorusCenter ε e) = ε * Anderson4D.znorm (y - e) ∧ 4 * R ≤ Anderson4D.znorm (y - e))

theorem Anderson4D.LatticeTerminalPathFar.terminalEdgeFar {ε R : ℝ} (hε : 0 < ε) {y e : Z4} {ys : List Z4} (h : LatticeTerminalPathFar ε R y e ys) : TerminalEdgeFar (R * ε) (latticeTorusCenter ε y) (latticeTorusCenter ε e) (List.map (latticeTorusCenter ε) ys)

noncomputable def Anderson4D.terminalRadiusFactor (R : ℝ) : ℝ

Radius-dependent harmless constant for the terminal far edge.

Equations

• Anderson4D.terminalRadiusFactor R = 4 * (1 + ((4 * R) ^ 2)⁻¹)

theorem Anderson4D.terminalRadiusFactor_pos {R : ℝ} (hR : 0 < R) : 0 < terminalRadiusFactor R

theorem Anderson4D.metricTerminalEdgeWeight_lattice_le {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) (y e : Z4) (hcenter : dist (latticeTorusCenter ε y) (latticeTorusCenter ε e) = ε * znorm (y - e)) (hfar : 4 * R ≤ znorm (y - e)) : 4 * (dist (latticeTorusCenter ε y) (latticeTorusCenter ε e) ^ 2)⁻¹ ≤ terminalRadiusFactor R * (ε ^ 2)⁻¹ * latticeEdgeWeight y e

The pointwise far terminal edge contributes exactly one ε⁻² lattice edge weight.

theorem Anderson4D.metricTerminalPathWeight_lattice_le {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) (y e : Z4) (ys : List Z4) (hpath : LatticeTerminalPathFar ε R y e ys) : metricTerminalPathWeight (R * ε) (latticeTorusCenter ε y) (latticeTorusCenter ε e) (List.map (latticeTorusCenter ε) ys) ≤ ((R ^ 2 + R ^ 4) * ε ^ 2) ^ ys.length * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTerminalPathWeight y e ys

Metric-to-lattice comparison for the entire far-terminal path.

theorem Anderson4D.terminalLatticeCellChain_le_of_far : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (ys : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTerminalPathFar ε R y e ys → terminalCellChain (R * ε) x z (List.map (latticeTorusCenter ε) ys) ≤ (C * (R ^ 2 + R ^ 4)) ^ ys.length * ε ^ (2 * ys.length) * (terminalRadiusFactor R * (ε ^ 2)⁻¹) * latticeTerminalPathWeight y e ys

Far-terminal lattice chain with all powers exposed.

theorem Anderson4D.pow_two_mul_mul_inv_sq {ε : ℝ} (hε : ε ≠ 0) (k : ℕ) (hk : 1 ≤ k) : ε ^ (2 * k) * (ε ^ 2)⁻¹ = ε ^ (2 * k - 2)

theorem Anderson4D.terminalLatticeCellChain_order_le_of_far : ∃ (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 → LatticeTerminalPathFar ε R y e ys → terminalCellChain (R * ε) x z (List.map (latticeTorusCenter ε) ys) ≤ (C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * ε ^ (4 * n - 6) * latticeTerminalPathWeight y e ys

Paper-order specialization of the far-terminal branch. With exactly 2n-2 internal vertices, the scale in the previous theorem simplifies to the advertised ε^(4n-6) in (5.3).