Sum-level periodic reduction for the primitive copied cells

The boundary-safe cell estimate produces primitivePeriodicReductionWeight, not the ordinary Euclidean reductionWeight. A pointwise comparison of their edge factors with a mesh-independent constant is false across the fundamental-domain cut.

This file records the strongest comparison available from the existing period-lift machinery without such a false hypothesis:

• arbitrary endpoint filters are retained through the lossless copied-label reindexing;
• the periodic chain is identified with the centre-preserving unwrapped Euclidean chain;
• the copied diameter is bounded in the genuine finite canonical box;
• the resulting unwrapped sum enters the already proved primitive-across lattice machine, with every finite-box and winding loss displayed.

Thus no boundary loss is hidden in a pointwise PeriodicCellEdgeComparison. The displayed mesh-dependent factors show that this fallback does not provide the uniform sum-level estimate required by Proposition 4.1.

Diameter and exact unwrapped-chain ledgers

theorem Anderson4D.one_le_primitiveTupleDiameterBracketSq {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) : 1 ≤ primitiveTupleDiameterBracketSq hm y

Every nonempty lattice tuple has diameter bracket at least one.

theorem Anderson4D.primitiveTupleDiameterBracketSq_le_windingBoxBase {m M : ℕ} (hm : 0 < m) {y : Fin m → Z4} (hy : y ∈ rdec_boundedTuples M m) : primitiveTupleDiameterBracketSq hm y ≤ windingBoxBase M

The diameter bracket of a tuple in [-M,M]⁴ is bounded by the same finite-box base used by the winding-sector module.

theorem Anderson4D.primitivePeriodicCopiedWeight_mul_unwrappedDiameter {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitivePeriodicCopiedWeight ε n hn y * primitiveTupleDiameterBracketSq ⋯ (primitiveUnwrappedReductionTuple ε n hn y) = primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y) * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)

Exact division-free relation between the periodic copied statistic and the ordinary reduction statistic of its centre-preserving unwrapped path. Only the tuple diameter changes.

theorem Anderson4D.primitivePeriodicCopiedWeight_le_diameter_mul_unwrapped {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitivePeriodicCopiedWeight ε n hn y ≤ primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y) * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)

Pointwise comparison to the unwrapped ordinary statistic with only the literal copied diameter as loss. This is valid across the torus cut.

theorem Anderson4D.primitivePeriodicCopiedWeight_le_boxBase_mul_unwrapped {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : primitivePeriodicCopiedWeight ε n hn y ≤ windingBoxBase (primitiveCopiedBoxRadius ε) * reductionWeight (2 * n - 1) (primitiveUnwrappedReductionTuple ε n hn y)

Canonical-box specialization of the preceding comparison.

Arbitrarily filtered copied-label sums

noncomputable def Anderson4D.primitivePeriodicReductionFilteredRealSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ℝ

Real periodic reduction sum on the exact bounded copied-label carrier, with an arbitrary endpoint/support predicate retained.

Equations

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

noncomputable def Anderson4D.primitivePeriodicReductionFilteredSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ENNReal

Extended-real version consumed directly by the cell-integral layer.

Equations

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

theorem Anderson4D.primitivePeriodicReductionFilteredSum_eq_ofReal (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredSum ε n hn κ P = ENNReal.ofReal (primitivePeriodicReductionFilteredRealSum ε n hn κ P)

theorem Anderson4D.primitivePeriodicReductionFilteredRealSum_eq_copied {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredRealSum ε n hn κ P = ∑ y ∈ primitiveCanonicalCellCarrier ε n κ with P (primitiveCopiedReductionTuple n hn y), primitivePeriodicCopiedWeight ε n hn y

Exact lossless reindexing back to canonical copied labels, retaining the support predicate.

theorem Anderson4D.primitivePeriodicReductionFilteredRealSum_le_unwrapped {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredRealSum ε n hn κ P ≤ windingBoxBase (primitiveCopiedBoxRadius ε) * primitiveUnwrappedReductionCellRealSum ε n hn κ

Sum-level periodic-to-unwrapped comparison. It is valid for every endpoint filter, and the filter is discarded only after nonnegativity has been used.

theorem Anderson4D.primitivePeriodicReductionFilteredSum_le_unwrapped {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredSum ε n hn κ P ≤ ENNReal.ofReal (windingBoxBase (primitiveCopiedBoxRadius ε) * primitiveUnwrappedReductionCellRealSum ε n hn κ)

ENNReal form of the filtered periodic-to-unwrapped bridge.

Entry into the existing primitive-across machine

theorem Anderson4D.exists_primitivePeriodicReductionFilteredRealSum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ∃ (M : ℕ), primitivePeriodicReductionFilteredRealSum ε n hn κ P ≤ windingBoxBase (primitiveCopiedBoxRadius ε) * ↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxAmplification M (2 * n - 1) * primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

Complete unconditional fallback into the existing reductionWeight machine for a primitive full pairing. Every loss is explicit; in particular no mesh-uniform edge comparison is used.

theorem Anderson4D.primitivePeriodicReductionFilteredSum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ∃ (M : ℕ), primitivePeriodicReductionFilteredSum ε n hn κ P ≤ ENNReal.ofReal (windingBoxBase (primitiveCopiedBoxRadius ε) * ↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxBase M ^ (2 * n) * primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)))

Membership-specialized ENNReal endpoint for the actual primitive pairing carrier used by §5.1.

Scalar extraction for the cell-integral consumer

theorem Anderson4D.primitivePeriodicReductionFilteredSum_factor {a b q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n hn κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, ENNReal.ofReal q * (ENNReal.ofReal (a * primitivePeriodicReductionWeight ε n hn u) + ENNReal.ofReal (b * primitivePeriodicReductionWeight ε n hn u)) = ENNReal.ofReal q * (ENNReal.ofReal a + ENNReal.ofReal b) * primitivePeriodicReductionFilteredSum ε n hn κ P

The two exhaustive-order coefficients and the covariance factor pull out of an arbitrarily filtered periodic sum exactly.