Primitive §5.1 assembly on period-compatible cells

Paper: R-51 — §5.1 (5.1)–(5.5) — reduction of Prop 4.1 to the lattice bound

This file closes the geometric part of paper §5.1 which is specific to the primitive kernel. Canonical torus cells cannot be used directly in (5.3): two neighbouring torus points may have floor labels on opposite sides of the fundamental cube. We therefore use compatibleMeshSize and unwrap the whole linear chain by period-block translations. The translations preserve the torus centres and give the exact no-wrap hypotheses consumed by terminalCellLIntegral_exhaustive_order.

The final finite reindexing from these unwrapped, endpoint-fixed paths to the bounded-box sum consumed by primitive_lattice_estimate is intentionally not asserted here. In particular, this file contains no hypothesis equivalent to Proposition 4.1 and does not declare Proposition41.

Counting the smaller endpoints exactly once

theorem Anderson4D.card_pairSupport_filter_lt_eq_pairs {ι : Type u_1} [Fintype ι] [LinearOrder ι] (κ : PartialPairing ι) : {i ∈ κ.pairSupport | i < κ i}.card = κ.pairs.card

In a finite linear order, selecting the smaller endpoint of every nontrivial two-cycle is in bijection with the unordered-pair carrier.

theorem Anderson4D.card_primitiveCovarianceRepresentatives {n : ℕ} (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : {i ∈ κ.pairSupport | i < κ i}.card = n

A full pairing of 2n positions has exactly n selected covariance factors in the smaller-endpoint convention of primitiveCovarianceProduct.

The exact covariance power ledger

theorem Anderson4D.exists_primitiveCovarianceProduct_uniform_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (κ : PartialPairing (Fin (2 * n))), κ.IsFull → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (x : Fin (2 * n) → T4), primitiveCovarianceProduct ρ ε n κ x ≤ (ε⁻¹ ^ dim * C) ^ n

The uniform pointwise covariance bound has exactly n factors for a full pairing on 2n slots.

The inserted diameter is the lattice maximum in (5.5)

theorem Anderson4D.dist_latticeTorusCenter_le {δ : ℝ} (hδ : 0 ≤ δ) (a b : Z4) : dist (latticeTorusCenter δ a) (latticeTorusCenter δ b) ≤ δ * znorm (a - b)

Periodization can only decrease the distance between Euclidean cell representatives.

theorem Anderson4D.latticeBracketSq_le_primitiveTupleDiameterBracketSq {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) (i j : Fin m) : latticeBracketSq (y i) (y j) ≤ primitiveTupleDiameterBracketSq hm y

Every pairwise lattice bracket is below the tuple maximum used by the fixed-data lattice assembly.

theorem Anderson4D.torusTupleDiameterSq_le_compatibleCellMaximum {m : ℕ} [Nonempty (Fin m)] (hm : 0 < m) {δ R : ℝ} (hδ : 0 < δ) (hR : 0 < R) (y : Fin m → Z4) (x : Fin m → T4) (hx : ∀ (i : Fin m), x i ∈ latticeCellNeighborhood δ R (y i)) : torusTupleDiameterSq x ≤ 8 * δ ^ 2 * (4 * R ^ 2 + primitiveTupleDiameterBracketSq hm y)

If every torus point lies in the radius-Rδ neighbourhood of its lattice centre, its squared tuple diameter is controlled by the genuine lattice maximum.

theorem Anderson4D.primitiveInsertedFactor_le_cellMaximum {m : ℕ} [Nonempty (Fin m)] (hm : 0 < m) {ε R : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hR : 0 < R) (y : Fin m → Z4) (x : Fin m → T4) (hx : ∀ (i : Fin m), x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (y i)) : ε ^ 2 + torusTupleDiameterSq x ≤ (12 + 32 * R ^ 2) * compatibleMeshSize ε ^ 2 * primitiveTupleDiameterBracketSq hm y

The paper insertion ε² + max |xᵢ-xⱼ|² is bounded by δ² times the same tuple maximum appearing in reductionWeight. The compatible-mesh comparison ε < 2δ supplies the otherwise missing ε² term.

Pointwise identification of the primitive integrand

noncomputable def Anderson4D.primitiveSingularChainProduct (n : ℕ) (hn : 1 ≤ n) (x : Fin (2 * n) → T4) : ℝ

The nonnegative inverse-square chain which dominates the arbitrary admissible input functions in the primitive integrand.

Equations

• Anderson4D.primitiveSingularChainProduct n hn x = ∏ j : Fin (2 * n - 1), Anderson4D.invSqKer (x (Anderson4D.primitiveEdgeLeft n hn j) - x (Anderson4D.primitiveEdgeRight n hn j))

theorem Anderson4D.primitiveSingularChainProduct_nonneg (n : ℕ) (hn : 1 ≤ n) (x : Fin (2 * n) → T4) : 0 ≤ primitiveSingularChainProduct n hn x

theorem Anderson4D.primitiveSingularChainProduct_eq_listChainProduct (n : ℕ) (hn : 1 ≤ n) (x : Fin (2 * n) → T4) : primitiveSingularChainProduct n hn x = listChainProduct (fun (a b : T4) => invSqKer (a - b)) (List.ofFn x)

The finite-index primitive chain is exactly the consecutive-edge product on the complete ordered tuple. This is the pointwise identification needed before turning the product-cell integral into terminalCellLIntegral.

theorem Anderson4D.abs_primitiveChainProduct_le_singular (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : IsAdmissiblePrimitiveInput n G) (x : Fin (2 * n) → T4) : |primitiveChainProduct n hn G x| ≤ primitiveSingularChainProduct n hn x

The chain part of every admissible primitive input is pointwise dominated by the exact nonnegative singular chain.

theorem Anderson4D.abs_primitiveIntegrand_le_singular_mul_covariance (ρ : SmoothCutoff) {ε : ℝ} (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : IsAdmissiblePrimitiveInput n G) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : |primitiveIntegrand ρ ε n hn G κ x| ≤ primitiveSingularChainProduct n hn x * primitiveCovarianceProduct ρ ε n κ x

Pointwise absolute-value reduction of the actual primitive integrand. The covariance product stays in the statement (rather than being replaced by a support predicate), and its sign is discharged from cutoff positivity.

theorem Anderson4D.exists_abs_primitiveIntegrand_uniform_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 → ∀ (x : Fin (2 * n) → T4), |primitiveIntegrand ρ ε n hn G κ x| ≤ (ε⁻¹ ^ dim * C) ^ n * primitiveSingularChainProduct n hn x

Uniform version of the preceding pointwise reduction, with the exact n-factor covariance power exposed.

The actual endpoint-fixed finite cell partition

theorem Anderson4D.FiniteMeasurableCells.lintegral_eq_sum {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) (μ : MeasureTheory.Measure X) (f : X → ENNReal) : ∫⁻ (x : X), f x ∂μ = ∑ i ∈ P.indices, ∫⁻ (x : X) in P.index ⁻¹' {i}, f x ∂μ

A finite measurable partition decomposes every nonnegative Lebesgue integral exactly, without an integrability premise.

theorem Anderson4D.measurable_primitiveAssemble (n : ℕ) (hn : 1 ≤ n) (z w : T4) : Measurable fun (v : Fin (2 * n - 2) → T4) => primitiveAssemble n hn z w v

Endpoint assembly is measurable in all internal variables.

noncomputable def Anderson4D.primitivePairedInternalCells (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (δ : ℝ) (hδ : 0 < δ) (z w : T4) : FiniteMeasurableCells (Fin (2 * n - 2) → T4) (Fin (2 * n) → Z4)

The genuine finite partition of the 2n-2 integration variables: assemble the fixed endpoints first, then floor only the chosen endpoint of each pair and copy its label to its mate.

Equations

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

theorem Anderson4D.primitive_lintegral_eq_sum_pairedInternalCells (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) {δ : ℝ} (hδ : 0 < δ) (z w : T4) (f : (Fin (2 * n - 2) → T4) → ENNReal) : (∫⁻ (v : Fin (2 * n - 2) → T4), f v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∑ y ∈ Fintype.piFinset fun (x : Fin (2 * n)) => torusGrid δ, ∫⁻ (v : Fin (2 * n - 2) → T4) in (fun (u : Fin (2 * n - 2) → T4) => pairedCellAssignment κ δ (primitiveAssemble n hn z w u)) ⁻¹' {y}, f v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

Exact finite cell decomposition of the actual endpoint-fixed primitive integration domain.

Covariance support puts every variable in its copied cell

theorem Anderson4D.primitiveCoordinates_mem_pairedCompatibleCells {m : ℕ} (ρ : SmoothCutoff) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (x : Fin m → T4) (hη : ∀ i < κ i, ρ.etaEpsT4 ε (x i - x (κ i)) ≠ 0) (i : Fin m) : x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) (1 + 4 * ρ.radius) (pairedCellAssignment κ (compatibleMeshSize ε) x i)

For a full pairing, nonvanishing of every selected covariance factor puts both members of every pair in the common compatible-mesh neighbourhood indexed by the smaller endpoint. The conclusion is stated for every slot, not merely for the selected half of the pairs.

theorem Anderson4D.primitiveCoordinates_mem_pairedCompatibleCells_of_covariance_ne_zero {n : ℕ} (ρ : SmoothCutoff) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (x : Fin (2 * n) → T4) (hcov : primitiveCovarianceProduct ρ ε n κ x ≠ 0) (i : Fin (2 * n)) : x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) (1 + 4 * ρ.radius) (pairedCellAssignment κ (compatibleMeshSize ε) x i)

Nonvanishing of the actual covariance product supplies the hypotheses of primitiveCoordinates_mem_pairedCompatibleCells.

The primitive linear cell path

def Anderson4D.primitiveInternalCellLabels (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List Z4

Cell labels of the 2n-2 integrated vertices, in paper order.

Equations

• Anderson4D.primitiveInternalCellLabels n hn y = List.ofFn fun (i : Fin (2 * n - 2)) => y (Anderson4D.primitiveInternalIdx n hn i)

@[simp]

theorem Anderson4D.primitiveInternalCellLabels_length (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : (primitiveInternalCellLabels n hn y).length = 2 * n - 2

def Anderson4D.primitiveFirstCell (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : Z4

The first cell label in the primitive chain.

Equations

• Anderson4D.primitiveFirstCell n hn y = y ⟨0, ⋯⟩

def Anderson4D.primitiveLastCell (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : Z4

The last cell label in the primitive chain.

Equations

• Anderson4D.primitiveLastCell n hn y = y (Anderson4D.primitiveLast n hn)

def Anderson4D.primitiveOriginalCellList (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List Z4

Original ordered cell-label list before period-block unwrapping.

Equations

• Anderson4D.primitiveOriginalCellList n hn y = Anderson4D.primitiveFirstCell n hn y :: (Anderson4D.primitiveInternalCellLabels n hn y ++ [Anderson4D.primitiveLastCell n hn y])

@[simp]

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

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

Centre-preserving no-wrap representatives of all internal labels.

Equations

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

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

A centre-preserving no-wrap representative of the fixed terminal label, chosen relative to the end of the already unwrapped internal path.

Equations

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

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

Complete list of centre-preserving representatives, including both fixed endpoints.

Equations

• Anderson4D.primitiveUnwrappedCellList ε n hn y = Anderson4D.primitiveFirstCell n hn y :: (Anderson4D.primitiveUnwrappedInternal ε n hn y ++ [Anderson4D.primitiveUnwrappedLast ε n hn y])

@[simp]

theorem Anderson4D.primitiveUnwrappedCellList_length (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : (primitiveUnwrappedCellList ε n hn y).length = 2 * n

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

Finite-tuple form of primitiveUnwrappedCellList, used to feed the existing reductionWeight/Hepp-tree interfaces.

Equations

• Anderson4D.primitiveUnwrappedCellTuple ε n hn y i = (Anderson4D.primitiveUnwrappedCellList ε n hn y).get (Fin.cast ⋯ i)

@[simp]

theorem Anderson4D.primitiveUnwrappedCellTuple_ofFn (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.ofFn (primitiveUnwrappedCellTuple ε n hn y) = primitiveUnwrappedCellList ε n hn y

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

Arithmetic cast of the complete unwrapped tuple to the literal Fin ((2n-1)+1) carrier expected by reductionWeight (2n-1).

Equations

• Anderson4D.primitiveUnwrappedReductionTuple ε n hn y i = Anderson4D.primitiveUnwrappedCellTuple ε n hn y (Fin.cast ⋯ i)

@[simp]

theorem Anderson4D.primitiveUnwrappedReductionTuple_ofFn (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.ofFn (primitiveUnwrappedReductionTuple ε n hn y) = primitiveUnwrappedCellList ε n hn y

@[simp]

theorem Anderson4D.primitiveUnwrappedInternal_length (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : (primitiveUnwrappedInternal ε n hn y).length = 2 * n - 2

theorem Anderson4D.primitiveUnwrappedInternal_map_centers {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.map (latticeTorusCenter (compatibleMeshSize ε)) (primitiveUnwrappedInternal ε n hn y) = List.map (latticeTorusCenter (compatibleMeshSize ε)) (primitiveInternalCellLabels n hn y)

Unwrapping does not change any internal torus centre.

theorem Anderson4D.primitiveUnwrappedLast_center {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : latticeTorusCenter (compatibleMeshSize ε) (primitiveUnwrappedLast ε n hn y) = latticeTorusCenter (compatibleMeshSize ε) (primitiveLastCell n hn y)

Unwrapping does not change the terminal torus centre.

theorem Anderson4D.primitiveUnwrappedCellList_map_centers {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.map (latticeTorusCenter (compatibleMeshSize ε)) (primitiveUnwrappedCellList ε n hn y) = List.map (latticeTorusCenter (compatibleMeshSize ε)) (primitiveOriginalCellList n hn y)

All centres of the complete unwrapped list agree, position by position, with the original canonical labels.

theorem Anderson4D.primitiveUnwrappedCellTuple_center {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) (i : Fin (2 * n)) : latticeTorusCenter (compatibleMeshSize ε) (primitiveUnwrappedCellTuple ε n hn y i) = latticeTorusCenter (compatibleMeshSize ε) (y i)

Function-indexed centre preservation, suitable for transporting a whole tuple of cell-membership hypotheses to the unwrapped realization.

theorem Anderson4D.primitiveCoordinates_mem_unwrappedCells {ε R : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) (x : Fin (2 * n) → T4) (hx : ∀ (i : Fin (2 * n)), x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (y i)) (i : Fin (2 * n)) : x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (primitiveUnwrappedCellTuple ε n hn y i)

Whole-tuple transport of compatible-cell membership to the unwrapped labels.

theorem Anderson4D.primitiveInsertedFactor_le_unwrappedCellMaximum {ε R : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hR : 0 < R) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) (x : Fin (2 * n) → T4) (hx : ∀ (i : Fin (2 * n)), x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (y i)) : ε ^ 2 + torusTupleDiameterSq x ≤ (12 + 32 * R ^ 2) * compatibleMeshSize ε ^ 2 * primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedCellTuple ε n hn y)

Inserted-factor specialization to the centre-preserving unwrapped tuple. This is the exact δ² · max⟨uᵢ-uⱼ⟩² factor which multiplies the terminal chain estimate before the covariance ledger is applied.

theorem Anderson4D.primitiveUnwrappedPath_noWrap {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : LatticeCellPathNoWrap (compatibleMeshSize ε) (primitiveFirstCell n hn y) (primitiveUnwrappedInternal ε n hn y ++ [primitiveUnwrappedLast ε n hn y])

The complete unwrapped primitive path satisfies the exact no-wrap predicate, including its final edge.

Exact identification with the existing lattice weight

theorem Anderson4D.adjacentProduct_eq_listChainProduct {α : Type u_1} {R : Type u_2} [CommMonoid R] {m : ℕ} (edge : α → α → R) (w : Fin m → α) : ∏ j : AdjacentIndex m, edge (w ↑j) (w (adjacentSucc j)) = listChainProduct edge (List.ofFn w)

Generic list form of the paper's AdjacentIndex product.

theorem Anderson4D.listChainProduct_lattice_eq_terminal (y e : Z4) (ys : List Z4) : listChainProduct latticeEdgeWeight (y :: (ys ++ [e])) = latticeTerminalPathWeight y e ys

A complete list with fixed endpoints carries exactly the terminal lattice path weight used by the exhaustive cell estimate.

theorem Anderson4D.primitiveUnwrappedReductionWeight_eq (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y) = primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedReductionTuple ε n hn y) * latticeTerminalPathWeight (primitiveFirstCell n hn y) (primitiveUnwrappedLast ε n hn y) (primitiveUnwrappedInternal ε n hn y)

Pointwise (5.5) identification.

The lattice weight produced by the actual compatible-mesh, no-wrap primitive cell path is literally reductionWeight: its adjacent product is the same latticeTerminalPathWeight that occurs in primitiveTerminalCellLIntegral_exhaustive_order, and its maximum is the existing primitiveTupleDiameterBracketSq.

The exhaustive per-cell estimate on the actual primitive path

theorem Anderson4D.mem_latticeCellNeighborhood_iff_of_center_eq {δ R : ℝ} {a b : Z4} (h : latticeTorusCenter δ a = latticeTorusCenter δ b) (x : T4) : x ∈ latticeCellNeighborhood δ R a ↔ x ∈ latticeCellNeighborhood δ R b

Membership in a lattice-cell neighbourhood depends only on its torus centre. This is the small but essential boundary-safe transport used for the last unwrapped label.

theorem Anderson4D.primitiveTerminalCellLIntegral_exhaustive_order : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 2 ≤ n) {ε : ℝ}, 0 < ε → ∀ (R : ℝ), 0 < R → ∀ (y : Fin (2 * n) → Z4) (x z : T4), x ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (primitiveFirstCell n ⋯ y) → z ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (primitiveLastCell n ⋯ y) → terminalCellLIntegral (R * compatibleMeshSize ε) x z (List.map (latticeTorusCenter (compatibleMeshSize ε)) (primitiveInternalCellLabels n ⋯ y)) ≤ ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * compatibleMeshSize ε ^ (4 * n - 6) * latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y)) + ENNReal.ofReal ((C * cellChainRadiusFactor R) ^ (2 * n - 3) * compatibleMeshSize ε ^ (4 * n - 6) * latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y))

Primitive-cell form of paper (5.3)--(5.4).

For n ≥ 2, the genuine internal primitive chain, with the two prescribed endpoints left unintegrated, is bounded on every compatible-mesh cell by the paper scale δ^(4n-6) and the linear lattice weight of centre-preserving no-wrap representatives. No integrability hypothesis and no periodic boundary assumption is present: the left side is the actual Tonelli terminalCellLIntegral, and unwrapping proves the latter internally.

theorem Anderson4D.compatibleCell_inserted_power_ledger (δ : ℝ) (n : ℕ) (hn : 2 ≤ n) : δ ^ 2 * δ ^ (4 * n - 6) = δ ^ (4 * n - 4)

Exact exponent cancellation in the inserted per-cell ledger.

theorem Anderson4D.primitiveInsertedTerminalCellLIntegral_exhaustive_order : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 2 ≤ n) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (R : ℝ), 0 < R → ∀ (y : Fin (2 * n) → Z4) (x : Fin (2 * n) → T4), (∀ (i : Fin (2 * n)), x i ∈ latticeCellNeighborhood (compatibleMeshSize ε) R (y i)) → have δ := compatibleMeshSize ε; have u := primitiveUnwrappedCellTuple ε n ⋯ y; have D := primitiveTupleDiameterBracketSq ⋯ u; have W := latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y); ENNReal.ofReal (ε ^ 2 + torusTupleDiameterSq x) * terminalCellLIntegral (R * δ) (x ⟨0, ⋯⟩) (x (primitiveLast n ⋯)) (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)

Inserted primitive-cell form of (5.2)--(5.5).

This theorem multiplies the exhaustive 2n-2-variable terminal-chain integral by the actual insertion ε² + max |xᵢ-xⱼ|². Centre preservation transports all cell memberships to the unwrapped tuple; the insertion is absorbed by its actual maximum; and the scale ledger closes to δ^(4n-4). The remaining linear product together with that maximum is identified with reductionWeight by primitiveUnwrappedReductionWeight_eq.

theorem Anderson4D.primitiveCovarianceSupportedCellChain : ∃ (C : ℝ), 0 < C ∧ ∀ (ρ : SmoothCutoff) (n : ℕ) (hn : 2 ≤ n) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ κ ∈ primitiveFullPairings n, ∀ (x : Fin (2 * n) → T4), primitiveCovarianceProduct ρ ε n κ x ≠ 0 → have δ := compatibleMeshSize ε; have R := 1 + 4 * ρ.radius; have y := pairedCellAssignment κ δ x; terminalCellLIntegral (R * δ) (x ⟨0, ⋯⟩) (x (primitiveLast n ⋯)) (List.map (latticeTorusCenter δ) (primitiveInternalCellLabels n ⋯ y)) ≤ ENNReal.ofReal ((C * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 6) * latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y)) + ENNReal.ofReal ((C * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 6) * latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y))

Covariance-supported specialization of primitiveTerminalCellLIntegral_exhaustive_order.

Here the cell tuple is not arbitrary: it is exactly pairedCellAssignment κ δ x for a primitive full pairing and an actual tuple on which the covariance product is nonzero. Thus the endpoint-cell hypotheses of the analytic estimate are discharged from ηε support.

theorem Anderson4D.primitiveCovarianceSupportedInsertedCellChain : ∃ (C : ℝ), 0 < C ∧ ∀ (ρ : SmoothCutoff) (n : ℕ) (hn : 2 ≤ n) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ κ ∈ primitiveFullPairings n, ∀ (x : Fin (2 * n) → T4), primitiveCovarianceProduct ρ ε n κ x ≠ 0 → have δ := compatibleMeshSize ε; have R := 1 + 4 * ρ.radius; have y := pairedCellAssignment κ δ x; have u := primitiveUnwrappedCellTuple ε n ⋯ y; have D := primitiveTupleDiameterBracketSq ⋯ u; have W := latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε n ⋯ y); ENNReal.ofReal (ε ^ 2 + torusTupleDiameterSq x) * terminalCellLIntegral (R * δ) (x ⟨0, ⋯⟩) (x (primitiveLast n ⋯)) (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)

Fully support-discharged inserted cell estimate. This is the final continuous statement before summing compatible cell fibers and applying the finite lattice/Hepp-tree estimate.

Exact Tonelli identification on a product cell

def Anderson4D.terminalSingularProduct (x z : T4) : List T4 → ENNReal

The ℝ≥0∞ chain density with fixed endpoints. Keeping this recursive form separate from terminalCellLIntegral makes the finite-product Tonelli identity transparent: the latter is precisely the iterated integral of this density.

Equations

• Anderson4D.terminalSingularProduct x z [] = ENNReal.ofReal (Anderson4D.invSqKer (x - z))
• Anderson4D.terminalSingularProduct x z (u :: us) = ENNReal.ofReal (Anderson4D.invSqKer (x - u)) * Anderson4D.terminalSingularProduct u z us

theorem Anderson4D.terminalSingularProduct_eq_ofReal_listChainProduct (x z : T4) (us : List T4) : terminalSingularProduct x z us = ENNReal.ofReal (listChainProduct (fun (a b : T4) => invSqKer (a - b)) (x :: (us ++ [z])))

theorem Anderson4D.measurable_terminalSingularProduct_ofFn (m : ℕ) (z : T4) : Measurable fun (p : T4 × (Fin m → T4)) => terminalSingularProduct p.1 z (List.ofFn p.2)

Joint measurability of the terminal chain density in its left endpoint and all integrated vertices.

theorem Anderson4D.terminalSingularProduct_lintegral_pi_restrict (r : ℝ) (x z : T4) (m : ℕ) (c : Fin m → T4) : (∫⁻ (v : Fin m → T4), terminalSingularProduct x z (List.ofFn v) ∂MeasureTheory.Measure.pi fun (i : Fin m) => paperMeasure.restrict (Metric.ball (c i) r)) = terminalCellLIntegral r x z (List.ofFn c)

Integrating the exact chain density against the product of the restricted cell measures is definitionally the recursive terminalCellLIntegral. This is the missing Tonelli bridge between the endpoint-fixed product-cell partition and the exhaustive cell-chain theorem.

theorem Anderson4D.terminalSingularProduct_setLIntegral_productCell (r : ℝ) (x z : T4) (m : ℕ) (c : Fin m → T4) : (∫⁻ (v : Fin m → T4) in Set.univ.pi fun (i : Fin m) => Metric.ball (c i) r, terminalSingularProduct x z (List.ofFn v) ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure) = terminalCellLIntegral r x z (List.ofFn c)

Set-integral form of terminalSingularProduct_lintegral_pi_restrict.

theorem Anderson4D.list_ofFn_eq_primitive_endpoints {α : Type u_1} (n : ℕ) (hn : 1 ≤ n) (x : Fin (2 * n) → α) : List.ofFn x = x ⟨0, ⋯⟩ :: ((List.ofFn fun (i : Fin (2 * n - 2)) => x (primitiveInternalIdx n hn i)) ++ [x (primitiveLast n hn)])

Generic finite-list decomposition into first endpoint, internal slots, and last endpoint, using the same slot maps as primitiveAssemble.

theorem Anderson4D.list_ofFn_primitiveAssemble (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) : List.ofFn (primitiveAssemble n hn z w v) = z :: (List.ofFn v ++ [w])

The complete ordered tuple assembled from fixed endpoints has exactly the paper list z, v₁, …, v_{2n-2}, w.

theorem Anderson4D.primitiveSingularChainProduct_assemble_eq_terminal (n : ℕ) (hn : 1 ≤ n) (z w : T4) (v : Fin (2 * n - 2) → T4) : ENNReal.ofReal (primitiveSingularChainProduct n hn (primitiveAssemble n hn z w v)) = terminalSingularProduct z w (List.ofFn v)

Pointwise, the actual primitive singular product after endpoint assembly is the fixed-endpoint chain density integrated by terminalCellLIntegral.

theorem Anderson4D.primitiveSingularChainProduct_setLIntegral_productCell (n : ℕ) (hn : 1 ≤ n) (r : ℝ) (z w : T4) (c : Fin (2 * n - 2) → T4) : (∫⁻ (v : Fin (2 * n - 2) → T4) in Set.univ.pi fun (i : Fin (2 * n - 2)) => Metric.ball (c i) r, ENNReal.ofReal (primitiveSingularChainProduct n hn (primitiveAssemble n hn z w v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = terminalCellLIntegral r z w (List.ofFn c)

Exact product-cell integral of the singular majorant after endpoint assembly.

theorem Anderson4D.primitiveInternal_mem_productCell_of_fiber_covariance_ne_zero (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (z w : T4) (y : Fin (2 * n) → Z4) (v : Fin (2 * n - 2) → T4) (hfiber : pairedCellAssignment κ (compatibleMeshSize ε) (primitiveAssemble n hn z w v) = y) (hcov : primitiveCovarianceProduct ρ ε n κ (primitiveAssemble n hn z w v) ≠ 0) : v ∈ Set.univ.pi fun (i : Fin (2 * n - 2)) => Metric.ball (latticeTorusCenter (compatibleMeshSize ε) (y (primitiveInternalIdx n hn i))) ((1 + 4 * ρ.radius) * compatibleMeshSize ε)

On a genuine paired-assignment fiber, nonvanishing covariance places every internal integration variable in the corresponding enlarged product cell.

theorem Anderson4D.exists_primitiveInsertedIntegrand_fiber_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 u := primitiveUnwrappedCellTuple ε n hn y; have D := primitiveTupleDiameterBracketSq ⋯ u; 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 a genuine paired cell fiber. The actual covariance product supplies support, the actual insertion is absorbed by the unwrapped lattice maximum, and the only remaining variable-dependent factor is the exact terminal singular chain density.

theorem Anderson4D.exists_primitiveInsertedIntegrand_fiber_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 u := primitiveUnwrappedCellTuple ε n hn y; have D := primitiveTupleDiameterBracketSq ⋯ u; 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 genuine fiber bound. The domain on the left is the actual fiber of pairedCellAssignment; the product cell on the right is not assumed but follows pointwise from nonvanishing of the covariance. Tonelli then turns its singular-chain integral into terminalCellLIntegral.

Closing the exact per-fiber scale ledger

theorem Anderson4D.primitiveCellMaximumTerminalLIntegral_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 u := primitiveUnwrappedCellTuple ε n ⋯ y; have D := primitiveTupleDiameterBracketSq ⋯ u; have W := latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε 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 uniform cell maximum, rather than a value of the insertion at a single tuple, multiplies the terminal-chain integral. This is the form needed after pulling the insertion outside a product-cell integral.

theorem Anderson4D.primitiveInsertedIntegrand_fiber_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 u := primitiveUnwrappedCellTuple ε n ⋯ y; have D := primitiveTupleDiameterBracketSq ⋯ u; have W := latticeTerminalPathWeight (primitiveFirstCell n ⋯ y) (primitiveUnwrappedLast ε n ⋯ y) (primitiveUnwrappedInternal ε 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 cell fiber.

This theorem starts with the real primitive inserted integrand, not a proxy. It performs the covariance-support reduction, product-cell enlargement, Tonelli identification, exhaustive chain estimate, and exact δ^(4n-4) ledger. The resulting lattice weight is then handled by finite summation and reindexing.

Exact reduction to the existing finite lattice statistic

theorem Anderson4D.primitiveTupleDiameterBracketSq_comp_equiv {m k : ℕ} (hm : 0 < m) (hk : 0 < k) (e : Fin m ≃ Fin k) (y : Fin k → Z4) : (primitiveTupleDiameterBracketSq hm fun (i : Fin m) => y (e i)) = primitiveTupleDiameterBracketSq hk y

The tuple-diameter maximum is invariant under a bijective reindexing of the finite slots.

theorem Anderson4D.primitiveUnwrappedCellDiameter_eq_reductionDiameter (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedCellTuple ε n hn y) = primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedReductionTuple ε n hn y)

The cell-tuple maximum and the arithmetic-cast reduction-tuple maximum are literally equal.

theorem Anderson4D.primitiveUnwrappedCellStatistic_eq_reductionWeight (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedCellTuple ε n hn y) * latticeTerminalPathWeight (primitiveFirstCell n hn y) (primitiveUnwrappedLast ε n hn y) (primitiveUnwrappedInternal ε n hn y) = reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)

The two lattice factors displayed by the continuous fiber estimate are exactly the pre-existing reductionWeight, with no inequality or hidden constant.

theorem Anderson4D.primitiveUnwrappedCellStatistic_scalarLedger (a b ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : a * primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedCellTuple ε n hn y) * b * latticeTerminalPathWeight (primitiveFirstCell n hn y) (primitiveUnwrappedLast ε n hn y) (primitiveUnwrappedInternal ε n hn y) = a * b * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)

Scalar ledger used to rewrite either exhaustive branch directly into the finite lattice interface.

Summing the genuine endpoint-fixed cell partition

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_unwrappedReductionSum (ρ : 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 grid := Fintype.piFinset fun (x : Fin (2 * n)) => torusGrid δ; have farCoeff := (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (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) ≤ ∑ y ∈ grid with (RespectsPairing κ) y, ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal ((12 + 32 * R ^ 2) * farCoeff * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n ⋯ y)) + ENNReal.ofReal ((12 + 32 * R ^ 2) * nearCoeff * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n ⋯ y)))

For one primitive pairing, the complete endpoint-fixed integral is bounded by a finite sum of the existing reductionWeight, evaluated at the centre-preserving unwrapped representative. The filter is the original copied-pair constraint and is proved from the actual cell assignment.

This theorem closes all continuous summation. Its right-hand side isolates the remaining finite period-lift reindexing problem.

noncomputable def Anderson4D.primitiveUnwrappedReductionCellSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : ENNReal

Purely finite statistic left after the continuous §5.1 argument: canonical copied-pair labels are sent to their centre-preserving unwrapped chain representatives before evaluating reductionWeight.

Equations

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

theorem Anderson4D.primitiveUnwrappedReductionCellSum_factor {a b q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : ∑ y ∈ Fintype.piFinset fun (x : Fin (2 * n)) => torusGrid (compatibleMeshSize ε) with (RespectsPairing κ) y, ENNReal.ofReal q * (ENNReal.ofReal (a * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)) + ENNReal.ofReal (b * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y))) = ENNReal.ofReal q * (ENNReal.ofReal a + ENNReal.ofReal b) * primitiveUnwrappedReductionCellSum ε n hn κ

Constant factors in either exhaustive branch pull cleanly out of the remaining finite unwrapped reduction sum.