Periodic-boundary bridge for the continuum cell decomposition

The canonical floor index of a torus point jumps at the boundary of the fundamental cube. Consequently, covariance support never implies equality of the two canonical floor indices. This file instead works with the Euclidean representative supplied by PairedCellConstraint: it floors that representative, proves that the represented torus point lies in the resulting lattice-centred neighbourhood, and proves a quantitative no-wrapping criterion for the two lattice centres.

The criterion is deliberately geometric. No singular-integral or lattice sum estimate is included in its assumptions.

Exact no-wrap criterion for one lattice edge

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

Coordinatewise half-period condition for the Euclidean displacement between two lattice representatives.

Equations

• Anderson4D.LatticeEdgeNoWrap ε y y' = ∀ (i : Fin Anderson4D.dim), |ε * ↑((y - y') i)| ≤ Real.pi

theorem Anderson4D.latticeTorusCenter_dist_eq_of_edgeNoWrap {ε : ℝ} (hε : 0 < ε) {y y' : Z4} (h : LatticeEdgeNoWrap ε y y') : dist (latticeTorusCenter ε y) (latticeTorusCenter ε y') = ε * znorm (y - y')

Under the half-period condition, quotienting the two Euclidean lattice centres does not shorten their distance.

theorem Anderson4D.latticeEdgeNoWrap_of_scale_mul_znorm_le_pi {ε : ℝ} (hε : 0 ≤ ε) {y y' : Z4} (h : ε * znorm (y - y') ≤ Real.pi) : LatticeEdgeNoWrap ε y y'

A sup-norm bound is a convenient sufficient form of the coordinatewise half-period condition.

theorem Anderson4D.latticeTorusCenter_dist_eq_of_scale_mul_znorm_le_pi {ε : ℝ} (hε : 0 < ε) {y y' : Z4} (h : ε * znorm (y - y') ≤ Real.pi) : dist (latticeTorusCenter ε y) (latticeTorusCenter ε y') = ε * znorm (y - y')

The form consumed directly by invSqKer_latticeCellEdge_le.

Recursive adapters for the existing chain interfaces

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

Every consecutive displacement in a lattice path is at most one half-period after multiplication by the mesh.

Equations

• Anderson4D.LatticeCellPathWithinHalfPeriod ε y [] = True
• Anderson4D.LatticeCellPathWithinHalfPeriod ε y (y' :: ys) = (ε * Anderson4D.znorm (y - y') ≤ Real.pi ∧ Anderson4D.LatticeCellPathWithinHalfPeriod ε y' ys)

theorem Anderson4D.LatticeCellPathWithinHalfPeriod.toNoWrap {ε : ℝ} (hε : 0 < ε) {y : Z4} {ys : List Z4} (h : LatticeCellPathWithinHalfPeriod ε y ys) : LatticeCellPathNoWrap ε y ys

The quantitative half-period predicate supplies exactly the geometric hypothesis required by integratedLatticeCellChain_le.

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

Half-period version of the far-terminal path predicate. Unlike LatticeTerminalPathFar, all geometric premises are expressed directly in the Euclidean lattice norm.

Equations

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

theorem Anderson4D.LatticeTerminalPathWithinHalfPeriod.toTerminalPathFar {ε R : ℝ} (hε : 0 < ε) {y e : Z4} {ys : List Z4} (h : LatticeTerminalPathWithinHalfPeriod ε R y e ys) : LatticeTerminalPathFar ε R y e ys

Adapter from the quantitative terminal-path condition to the existing far-terminal chain interface.

Euclidean representatives and lattice neighbourhoods

@[simp]

theorem Anderson4D.periodizeR4_sub (x x' : R4) : periodizeR4 (x - x') = periodizeR4 x - periodizeR4 x'

theorem Anderson4D.periodizeR4_torusLift (z : T4) : periodizeR4 (torusLift z) = z

theorem Anderson4D.dist_periodizeR4_le_norm_sub (x x' : R4) : dist (periodizeR4 x) (periodizeR4 x') ≤ ‖x - x'‖

The coordinatewise quotient map is distance non-increasing for the fixed sup norms.

theorem Anderson4D.PairedCellConstraint.first_mem_latticeCellNeighborhood {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : z ∈ latticeCellNeighborhood ε 1 y

The first endpoint of a paired-cell constraint lies in the radius-one lattice neighbourhood of the recorded cell.

theorem Anderson4D.PairedCellConstraint.second_mem_latticeCellNeighborhood {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : w ∈ latticeCellNeighborhood ε (1 + 2 * ρ.radius) y

The supported paired endpoint lies in the enlarged neighbourhood of the same recorded lattice cell. This is the boundary-safe substitute for the false assertion that both canonical floor indices are equal.

theorem Anderson4D.PairedCellConstraint.endpoints_mem_latticeCellNeighborhood {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : z ∈ latticeCellNeighborhood ε (1 + 2 * ρ.radius) y ∧ w ∈ latticeCellNeighborhood ε (1 + 2 * ρ.radius) y

Both paired endpoints lie in one common enlarged lattice neighbourhood.

Flooring the boundary-safe representative

theorem Anderson4D.PairedCellConstraint.exists_floored_representative {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : ∃ (y' : Z4) (wrep : R4), periodizeR4 wrep = w ∧ floorCell ε wrep = y' ∧ w ∈ latticeCellNeighborhood ε 1 y' ∧ znorm (y - y') < 2 + 2 * ρ.radius

Flooring the chosen Euclidean representative of the paired endpoint produces a genuine lattice cell containing that endpoint, and its index is within a cutoff-dependent bounded displacement of the first index.

theorem Anderson4D.PairedCellConstraint.exists_floored_representative_noWrap {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) (hscale : ε * (2 + 2 * ρ.radius) ≤ Real.pi) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : ∃ (y' : Z4), w ∈ latticeCellNeighborhood ε 1 y' ∧ znorm (y - y') < 2 + 2 * ρ.radius ∧ dist (latticeTorusCenter ε y) (latticeTorusCenter ε y') = ε * znorm (y - y')

At scales below the explicit half-period threshold, the first cell and the floored boundary-safe representative form an exact no-wrap edge. The conclusion is in the form consumed by invSqKer_latticeCellEdge_le.

Direct consumption by the singular-cell estimates

theorem Anderson4D.invSqKer_pairedFlooredCellEdge_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ρ : SmoothCutoff) (ε : ℝ), 0 < ε → ε * (2 + 2 * ρ.radius) ≤ Real.pi → ∀ (z w : T4) (y : Z4), PairedCellConstraint ρ ε z w y → ∃ (y' : Z4), w ∈ latticeCellNeighborhood ε 1 y' ∧ znorm (y - y') < 2 + 2 * ρ.radius ∧ ∫ (u : T4) in latticeCellNeighborhood ε 1 y', invSqKer (z - u) ∂paperMeasure ≤ C * (1 ^ 2 + 1 ^ 4) * ε ^ 2 * latticeEdgeWeight y y'

One covariance-supported pair, floored through its boundary-safe representative, supplies a legitimate invocation of invSqKer_latticeCellEdge_le. The theorem returns the chosen cell because the canonical floor cell of w is intentionally not used.

theorem Anderson4D.integratedLatticeCellChain_le_of_withinHalfPeriod : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y : Z4) (ys : List Z4) (x : T4), LatticeCellPathWithinHalfPeriod ε 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

integratedLatticeCellChain_le with its no-wrap premise discharged by the checkable half-period inequalities.

theorem Anderson4D.terminalLatticeCellChain_le_of_withinHalfPeriod : ∃ (C : ℝ), 0 < C ∧ ∀ (ε R : ℝ), 0 < ε → 0 < R → ∀ (y e : Z4) (ys : List Z4) (x z : T4), x ∈ latticeCellNeighborhood ε R y → z ∈ latticeCellNeighborhood ε R e → LatticeTerminalPathWithinHalfPeriod ε 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 analogue of integratedLatticeCellChain_le_of_withinHalfPeriod.

Exact index translations on a period-compatible mesh

def Anderson4D.translateCellIndex (q : ℤ) (k y : Z4) : Z4

Translating a lattice index by q cells in each chosen coordinate.

Equations

• Anderson4D.translateCellIndex q k y i = y i + q * k i

structure Anderson4D.PeriodCompatibleMesh (δ : ℝ) (q : ℤ) : Prop

Compatibility condition saying that exactly q mesh cells make one torus period. It is intended for a mesh δ = 2π/q; the covariance scale may remain an arbitrary nearby positive real.

• cellCount_pos : 0 < q
• period_eq : δ * ↑q = 2 * Real.pi

noncomputable def Anderson4D.compatibleCellCount (ε : ℝ) : ℤ

Number of cells in the compatible mesh selected at covariance scale ε.

Equations

• Anderson4D.compatibleCellCount ε = ⌈2 * Real.pi / ε⌉

noncomputable def Anderson4D.compatibleMeshSize (ε : ℝ) : ℝ

Mesh size 2π/q, where q = ⌈2π/ε⌉. Unlike using ε itself as the mesh, this makes the discrete grid exactly periodic while staying comparable to ε.

Equations

• Anderson4D.compatibleMeshSize ε = 2 * Real.pi / ↑(Anderson4D.compatibleCellCount ε)

theorem Anderson4D.compatibleCellCount_pos {ε : ℝ} (hε : 0 < ε) : 0 < compatibleCellCount ε

theorem Anderson4D.compatibleMesh_isPeriodCompatible {ε : ℝ} (hε : 0 < ε) : PeriodCompatibleMesh (compatibleMeshSize ε) (compatibleCellCount ε)

theorem Anderson4D.compatibleMeshSize_pos {ε : ℝ} (hε : 0 < ε) : 0 < compatibleMeshSize ε

theorem Anderson4D.compatibleMeshSize_le {ε : ℝ} (hε : 0 < ε) : compatibleMeshSize ε ≤ ε

The compatible mesh is no coarser than the covariance scale.

theorem Anderson4D.lt_two_mul_compatibleMeshSize {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ε < 2 * compatibleMeshSize ε

For the theorem regime ε ≤ 1, the covariance scale is less than twice the compatible mesh size. Thus changing meshes only enlarges the fixed cell-neighbourhood constant.

theorem Anderson4D.latticeTorusCenter_translateCellIndex {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (k y : Z4) : latticeTorusCenter δ (translateCellIndex q k y) = latticeTorusCenter δ y

Translating by a whole number of period-cell blocks does not change the torus centre.

noncomputable def Anderson4D.nearestPeriodTranslate (q : ℤ) (y y' : Z4) : Z4

The period-block translate of y' nearest to y, coordinatewise.

Equations

• Anderson4D.nearestPeriodTranslate q y y' = Anderson4D.translateCellIndex q (fun (i : Fin Anderson4D.dim) => round (↑((y - y') i) / ↑q)) y'

theorem Anderson4D.nearestPeriodTranslate_edgeNoWrap {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (y y' : Z4) : LatticeEdgeNoWrap δ y (nearestPeriodTranslate q y y')

A nearest period-block translate is always inside the half-period window around the reference index.

theorem Anderson4D.latticeTorusCenter_nearestPeriodTranslate {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (y y' : Z4) : latticeTorusCenter δ (nearestPeriodTranslate q y y') = latticeTorusCenter δ y'

The nearest translate represents the same torus centre as the original index.

theorem Anderson4D.exists_periodTranslate_dist_eq {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (y y' : Z4) : ∃ (y'' : Z4), latticeTorusCenter δ y'' = latticeTorusCenter δ y' ∧ dist (latticeTorusCenter δ y) (latticeTorusCenter δ y'') = δ * znorm (y - y'')

Every edge on a compatible mesh admits a centre-preserving lattice representative satisfying the exact distance identity required by the cell estimates.

Centre-preserving unwrapping of complete paths

def Anderson4D.unwrapLatticePath (q : ℤ) (y : Z4) : List Z4 → List Z4

Recursively choose, for each original path vertex, the period-block translate nearest to the previously chosen vertex.

Equations

• Anderson4D.unwrapLatticePath q y [] = []
• Anderson4D.unwrapLatticePath q y (y' :: ys) = Anderson4D.nearestPeriodTranslate q y y' :: Anderson4D.unwrapLatticePath q (Anderson4D.nearestPeriodTranslate q y y') ys

@[simp]

theorem Anderson4D.unwrapLatticePath_length (q : ℤ) (y : Z4) (ys : List Z4) : (unwrapLatticePath q y ys).length = ys.length

theorem Anderson4D.unwrapLatticePath_map_centers {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (y : Z4) (ys : List Z4) : List.map (latticeTorusCenter δ) (unwrapLatticePath q y ys) = List.map (latticeTorusCenter δ) ys

Unwrapping changes lattice labels but not the corresponding list of torus centres.

theorem Anderson4D.unwrapLatticePath_noWrap {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) (y : Z4) (ys : List Z4) : LatticeCellPathNoWrap δ y (unwrapLatticePath q y ys)

Every recursively unwrapped path satisfies the exact no-wrap predicate, with no condition on the original canonical indices.

theorem Anderson4D.integratedLatticeCellChain_le_unwrapped : ∃ (C : ℝ), 0 < C ∧ ∀ (δ R : ℝ) (q : ℤ), PeriodCompatibleMesh δ q → 0 < R → ∀ (y : Z4) (ys : List Z4), ∀ x ∈ latticeCellNeighborhood δ R y, integratedCellChain (R * δ) x (List.map (latticeTorusCenter δ) ys) ≤ (C * (R ^ 2 + R ^ 4)) ^ ys.length * δ ^ (2 * ys.length) * latticeCellPathWeight y (unwrapLatticePath q y ys)

On a period-compatible mesh, the arbitrary torus-centre path is therefore covered by integratedLatticeCellChain_le; only its lattice weight is evaluated on the centre-preserving unwrapped labels.

Covariance support on the compatible mesh

theorem Anderson4D.SmoothCutoff.exists_representative_near_meshCell_of_etaEpsT4_ne_zero (ρ : SmoothCutoff) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (z w : T4) (y : Z4) (hzcell : torusFloorCell δ z = y) (hη : ρ.etaEpsT4 ε (z - w) ≠ 0) : ∃ (wrep : R4), periodizeR4 wrep = w ∧ ‖wrep - cellRepresentative δ y‖ < δ + 2 * ρ.radius * ε

Covariance support and an independently chosen positive mesh give a boundary-safe representative of the paired endpoint. Its distance to the first mesh cell is δ + 2Rε, separating the mesh and covariance scales.

theorem Anderson4D.SmoothCutoff.etaEpsT4_pair_mem_compatibleCellNeighborhood (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z w : T4) (hη : ρ.etaEpsT4 ε (z - w) ≠ 0) : have δ := compatibleMeshSize ε; have y := torusFloorCell δ z; z ∈ latticeCellNeighborhood δ (1 + 4 * ρ.radius) y ∧ w ∈ latticeCellNeighborhood δ (1 + 4 * ρ.radius) y

At the compatible mesh δ = 2π/⌈2π/ε⌉, both endpoints of a nonzero covariance factor lie in one common cell neighbourhood with the fixed radius factor 1 + 4R. This is valid for every real 0 < ε ≤ 1; no commensurability assumption is placed on the covariance scale itself.