Boundary-safe copied-cell reduction for the primitive integral

The canonical labels used in paper §5.1 live in one fundamental box. Across the cut of that box, ordinary differences of labels do not represent torus distances. This file therefore keeps the literal copied labels and records the analytic cell estimate with the corresponding periodic edge weight.

No endpoint translation is discarded: the finite decomposition and the lossless copied-label reindexing below retain an arbitrary decidable support predicate on the complete reduction tuple.

The boundary-safe edge and chain weights

noncomputable def Anderson4D.periodicCellEdgeWeight (δ : ℝ) (a b : Z4) : ℝ

The dimensionless inverse-square edge weight between two torus cell centres. It agrees with latticeEdgeWeight whenever the chosen lattice representatives do not wrap.

Equations

• Anderson4D.periodicCellEdgeWeight δ a b = δ ^ 2 / (δ ^ 2 + dist (Anderson4D.latticeTorusCenter δ a) (Anderson4D.latticeTorusCenter δ b) ^ 2)

theorem Anderson4D.periodicCellEdgeWeight_nonneg (δ : ℝ) (a b : Z4) : 0 ≤ periodicCellEdgeWeight δ a b

theorem Anderson4D.periodicCellEdgeWeight_comm (δ : ℝ) (a b : Z4) : periodicCellEdgeWeight δ a b = periodicCellEdgeWeight δ b a

def Anderson4D.periodicTerminalPathWeight (δ : ℝ) (a e : Z4) : List Z4 → ℝ

Product of periodic edge weights along a path with fixed endpoints.

Equations

• Anderson4D.periodicTerminalPathWeight δ a e [] = Anderson4D.periodicCellEdgeWeight δ a e
• Anderson4D.periodicTerminalPathWeight δ a e (b :: bs) = Anderson4D.periodicCellEdgeWeight δ a b * Anderson4D.periodicTerminalPathWeight δ b e bs

theorem Anderson4D.periodicTerminalPathWeight_nonneg (δ : ℝ) (a e : Z4) (as : List Z4) : 0 ≤ periodicTerminalPathWeight δ a e as

theorem Anderson4D.periodicCellEdgeWeight_eq_latticeEdgeWeight_of_noWrap {δ : ℝ} (hδ : 0 < δ) {a b : Z4} (hcenter : dist (latticeTorusCenter δ a) (latticeTorusCenter δ b) = δ * znorm (a - b)) : periodicCellEdgeWeight δ a b = latticeEdgeWeight a b

On a no-wrap edge, the boundary-safe weight is exactly the ordinary integer-lattice weight.

theorem Anderson4D.periodicTerminalPathWeight_eq_latticeTerminalPathWeight_of_noWrap {δ : ℝ} (hδ : 0 < δ) (a e : Z4) (as : List Z4) (hnowrap : LatticeCellPathNoWrap δ a (as ++ [e])) : periodicTerminalPathWeight δ a e as = latticeTerminalPathWeight a e as

Pathwise form of the preceding exact identity.

theorem Anderson4D.periodicTerminalPathWeight_congr_centers (δ : ℝ) {a a' e e' : Z4} {as as' : List Z4} (ha : latticeTorusCenter δ a = latticeTorusCenter δ a') (he : latticeTorusCenter δ e = latticeTorusCenter δ e') (hs : List.map (latticeTorusCenter δ) as = List.map (latticeTorusCenter δ) as') : periodicTerminalPathWeight δ a e as = periodicTerminalPathWeight δ a' e' as'

A periodic path weight only depends on the torus centres of all its labels.

theorem Anderson4D.primitiveUnwrappedTerminalWeight_eq_periodicCopied {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : latticeTerminalPathWeight (primitiveFirstCell n hn y) (primitiveUnwrappedLast ε n hn y) (primitiveUnwrappedInternal ε n hn y) = periodicTerminalPathWeight (compatibleMeshSize ε) (primitiveFirstCell n hn y) (primitiveLastCell n hn y) (primitiveInternalCellLabels n hn y)

The no-wrap weight produced internally by the analytic chain proof is literally the periodic weight of the original canonical copied labels.

The canonical periodic reduction statistic

noncomputable def Anderson4D.primitivePeriodicCopiedWeight (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : ℝ

Boundary-safe version of the pointwise statistic in (5.5), on the literal copied tuple rather than occurrence-wise path lifts.

Equations

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

noncomputable def Anderson4D.primitivePeriodicReductionWeight (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (u : Fin (2 * n - 1 + 1) → Z4) : ℝ

The same boundary-safe statistic as a function on the literal reduction carrier.

Equations

• Anderson4D.primitivePeriodicReductionWeight ε n hn u = Anderson4D.primitivePeriodicCopiedWeight ε n hn (Anderson4D.primitiveCopiedSourceTuple n hn u)

@[simp]

theorem Anderson4D.primitivePeriodicReductionWeight_reductionTuple (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitivePeriodicReductionWeight ε n hn (primitiveCopiedReductionTuple n hn y) = primitivePeriodicCopiedWeight ε n hn y

@[simp]

theorem Anderson4D.primitiveCopiedReductionTuple_ofFn (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.ofFn (primitiveCopiedReductionTuple n hn y) = List.ofFn y

theorem Anderson4D.primitiveCopiedCellDiameter_eq_reductionDiameter (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitiveTupleDiameterBracketSq ⋯ y = primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y)

The arithmetic cast from the cell tuple to the reduction tuple does not change its diameter maximum.

theorem Anderson4D.primitivePeriodicCopiedWeight_nonneg (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : 0 ≤ primitivePeriodicCopiedWeight ε n hn y

theorem Anderson4D.primitivePeriodicReductionWeight_nonneg (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (u : Fin (2 * n - 1 + 1) → Z4) : 0 ≤ primitivePeriodicReductionWeight ε n hn u

theorem Anderson4D.primitivePeriodicCopiedWeight_eq_reductionWeight_of_noWrap {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) (hnowrap : LatticeCellPathNoWrap (compatibleMeshSize ε) (primitiveFirstCell n hn y) (primitiveInternalCellLabels n hn y ++ [primitiveLastCell n hn y])) : primitivePeriodicCopiedWeight ε n hn y = reductionWeight (2 * n - 1) (primitiveCopiedReductionTuple n hn y)

In the absence of a boundary crossing, the periodic statistic is exactly the ordinary copied-label reductionWeight.

Canonical copied-cell analytic bounds

theorem Anderson4D.exists_primitiveInsertedIntegrand_copiedFiber_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ (κ : PartialPairing (Fin (2 * n))), κ.IsFull → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4) (y : Fin (2 * n) → Z4) (v : Fin (2 * n - 2) → T4), pairedCellAssignment κ (compatibleMeshSize ε) (primitiveAssemble n hn z w v) = y → primitiveCovarianceProduct ρ ε n κ (primitiveAssemble n hn z w v) ≠ 0 → have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have D := primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y); ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ≤ ENNReal.ofReal ((ε⁻¹ ^ dim * C) ^ n * ((12 + 32 * R ^ 2) * δ ^ 2 * D)) * terminalSingularProduct z w (List.ofFn v)

Pointwise majorization on an actual paired cell fiber, with the diameter of the literal copied reduction tuple and no occurrence-wise lift in the statement.

theorem Anderson4D.exists_primitiveInsertedIntegrand_copiedFiber_lintegral_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ (κ : PartialPairing (Fin (2 * n))), κ.IsFull → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4) (y : Fin (2 * n) → Z4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have D := primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y); have c := fun (i : Fin (2 * n - 2)) => latticeTorusCenter δ (y (primitiveInternalIdx n hn i)); (∫⁻ (v : Fin (2 * n - 2) → T4) in (fun (q : Fin (2 * n - 2) → T4) => pairedCellAssignment κ δ (primitiveAssemble n hn z w q)) ⁻¹' {y}, ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ENNReal.ofReal ((ε⁻¹ ^ dim * C) ^ n * ((12 + 32 * R ^ 2) * δ ^ 2 * D)) * terminalCellLIntegral (R * δ) z w (List.ofFn c)

Integrated form of the canonical copied-fiber bound. Covariance support enlarges the actual assignment fiber to the product of canonical torus cells, after which Tonelli identifies the singular chain exactly.

theorem Anderson4D.primitiveCopiedCellMaximumTerminalLIntegral_exhaustive_order : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 2 ≤ n) {ε : ℝ}, 0 < ε → ∀ (R : ℝ), 0 < R → ∀ (y : Fin (2 * n) → Z4) (z w : T4), z ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (primitiveFirstCell n ⋯ y) → w ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (primitiveLastCell n ⋯ y) → have δ := compatibleMeshSize ε; have D := primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n ⋯ y); have W := periodicTerminalPathWeight δ (primitiveFirstCell n ⋯ y) (primitiveLastCell n ⋯ y) (primitiveInternalCellLabels n ⋯ y); ENNReal.ofReal ((12 + 32 * R ^ 2) * δ ^ 2 * D) * terminalCellLIntegral (R * δ) z w (List.map (latticeTorusCenter δ) (primitiveInternalCellLabels n ⋯ y)) ≤ ENNReal.ofReal ((12 + 32 * R ^ 2) * D * (C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4) * W) + ENNReal.ofReal ((12 + 32 * R ^ 2) * D * (C * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4) * W)

The canonical diameter maximum times the true terminal-chain integral has the paper scale, with the boundary-safe periodic product of the same copied labels.

theorem Anderson4D.primitiveInsertedIntegrand_copiedFiber_exhaustive_order (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4) (y : Fin (2 * n) → Z4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have D := primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n ⋯ y); have W := periodicTerminalPathWeight δ (primitiveFirstCell n ⋯ y) (primitiveLastCell n ⋯ y) (primitiveInternalCellLabels n ⋯ y); (∫⁻ (v : Fin (2 * n - 2) → T4) in (fun (q : Fin (2 * n - 2) → T4) => pairedCellAssignment κ δ (primitiveAssemble n ⋯ z w q)) ⁻¹' {y}, ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal ((12 + 32 * R ^ 2) * D * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4) * W) + ENNReal.ofReal ((12 + 32 * R ^ 2) * D * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4) * W))

Complete continuous estimate on one actual paired canonical-cell fiber. The right-hand side contains only the literal copied labels and the periodic edge product forced by the torus geometry.

Endpoint support and lossless filtered summation

def Anderson4D.primitiveCanonicalEndpointSupported (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : T4) (y : Fin (2 * n) → Z4) : Prop

The endpoint constraint genuinely supplied by a nonzero endpoint-fixed cell fiber.

Equations

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

def Anderson4D.primitiveCopiedEndpointSupported (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : T4) (u : Fin (2 * n - 1 + 1) → Z4) : Prop

The same endpoint constraint transported to the exact reduction-tuple carrier used by sum_copiedLabels_filter_eq_boundedPairing_filter.

Equations

• Anderson4D.primitiveCopiedEndpointSupported ρ ε n hn z w u = Anderson4D.primitiveCanonicalEndpointSupported ρ ε n hn z w (Anderson4D.primitiveCopiedSourceTuple n hn u)

@[implicit_reducible]

noncomputable instance Anderson4D.primitiveCopiedEndpointSupported_decidable (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : T4) (u : Fin (2 * n - 1 + 1) → Z4) : Decidable (primitiveCopiedEndpointSupported ρ ε n hn z w u)

Equations

• Anderson4D.primitiveCopiedEndpointSupported_decidable ρ ε n hn z w u = Classical.propDecidable (Anderson4D.primitiveCopiedEndpointSupported ρ ε n hn z w u)

@[simp]

theorem Anderson4D.primitiveCopiedEndpointSupported_reductionTuple (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : T4) (y : Fin (2 * n) → Z4) : primitiveCopiedEndpointSupported ρ ε n hn z w (primitiveCopiedReductionTuple n hn y) ↔ primitiveCanonicalEndpointSupported ρ ε n hn z w y

noncomputable def Anderson4D.primitiveCopiedFiberContribution (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (z w : T4) (y : Fin (2 * n) → Z4) : ENNReal

Actual contribution of one canonical paired-assignment fiber.

Equations

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

theorem Anderson4D.primitiveCopiedFiberContribution_eq_zero_of_not_endpointSupported (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (z w : T4) (y : Fin (2 * n) → Z4) (hunsupported : ¬primitiveCanonicalEndpointSupported ρ ε n hn z w y) : primitiveCopiedFiberContribution ρ ε n hn G κ z w y = 0

Failure of the endpoint-support predicate forces the genuine canonical fiber contribution to vanish.

theorem Anderson4D.sum_copiedLabels_filter_eq_boundedPairing_filter_ennreal {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] (f : (Fin (2 * n - 1 + 1) → Z4) → ENNReal) : ∑ y ∈ primitiveCanonicalCellCarrier ε n κ with P (primitiveCopiedReductionTuple n hn y), f (primitiveCopiedReductionTuple n hn y) = ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n hn κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, f u

ENNReal companion of the real-valued lossless reindexing theorem. The proof is purely finite and retains any decidable tuple predicate.

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_eq_boundedPairing_filter (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (z w : T4) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] (hvanish : ∀ y ∈ primitiveCanonicalCellCarrier ε n κ, ¬P (primitiveCopiedReductionTuple n hn y) → primitiveCopiedFiberContribution ρ ε n hn G κ z w y = 0) : (∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n hn κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, primitiveCopiedFiberContribution ρ ε n hn G κ z w (primitiveCopiedSourceTuple n hn u)

Exact endpoint-fixed Fubini decomposition, followed by exact copied-label reindexing. The predicate is arbitrary; the only semantic premise is that fibers outside it vanish.

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_eq_endpointSupportedCells (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (z w : T4) : (∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n hn κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with (primitiveCopiedEndpointSupported ρ ε n hn z w) u, primitiveCopiedFiberContribution ρ ε n hn G κ z w (primitiveCopiedSourceTuple n hn u)

Concrete specialization retaining precisely the endpoint support forced by nonvanishing covariance.

Complete periodic copied-label cell reduction

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_periodicCopiedSum_filter (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [inst : DecidablePred P], (∀ y ∈ primitiveCanonicalCellCarrier ε n κ, ¬P (primitiveCopiedReductionTuple n ⋯ y) → primitiveCopiedFiberContribution ρ ε n ⋯ G κ z w y = 0) → have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); (∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n ⋯ κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal (farCoeff * primitivePeriodicReductionWeight ε n ⋯ u) + ENNReal.ofReal (nearCoeff * primitivePeriodicReductionWeight ε n ⋯ u))

The endpoint-fixed primitive integral is bounded by the finite, losslessly reindexed periodic copied-label statistic. P may be any decidable endpoint-support refinement; no translation enlargement is made.

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_periodicEndpointSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); (∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n ⋯ κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with (primitiveCopiedEndpointSupported ρ ε n ⋯ z w) u, ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal (farCoeff * primitivePeriodicReductionWeight ε n ⋯ u) + ENNReal.ofReal (nearCoeff * primitivePeriodicReductionWeight ε n ⋯ u))

Specialization of the preceding theorem to the exact endpoint support forced by covariance.

Exact remaining boundary interface

def Anderson4D.PeriodicCellEdgeComparison (δ C : ℝ) : Prop

The sole pointwise interface that would turn the periodic cell statistic back into the existing Euclidean copied-label statistic. It is deliberately defined, not assumed by any theorem above. A constant uniform in the mesh cannot satisfy this predicate on the canonical torus box.

Equations

• Anderson4D.PeriodicCellEdgeComparison δ C = ∀ (a b : Anderson4D.Z4), Anderson4D.periodicCellEdgeWeight δ a b ≤ C * Anderson4D.latticeEdgeWeight a b

theorem Anderson4D.periodicCellEdgeComparison_of_noWrap {δ : ℝ} (hδ : 0 < δ) {a b : Z4} (hcenter : dist (latticeTorusCenter δ a) (latticeTorusCenter δ b) = δ * znorm (a - b)) : periodicCellEdgeWeight δ a b ≤ latticeEdgeWeight a b

On a genuinely no-wrap edge the required comparison holds with constant one, in fact as an equality.

theorem Anderson4D.periodicCellEdgeWeight_translateCellIndex_eq_one {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) (k y : Z4) : periodicCellEdgeWeight δ (translateCellIndex q k y) y = 1

A whole-period translate has periodic edge weight exactly one. Its ordinary lattice weight still sees the (possibly arbitrarily large) integer translate; this is the precise cut obstruction to canonical (5.3).