Winding-sector normalization for the primitive reduction

An unwrapped compatible-mesh path remembers occurrence-wise period lifts. Paired occurrences are therefore congruent modulo the period count, but need not be literally equal. Here we normalize each pair to its canonical anchor occurrence. This produces a tuple consumed by the existing AcrossPairing layer.

The normalization does not preserve the lattice weight. We record an explicit finite-box amplification, then sum the genuine canonical cell carrier into a finite enlargement of primitiveAcrossLatticeSum in which all (rather than only primitive) across pairings are retained. No certificate or assumed estimate is used.

Literal pairing normalization

def Anderson4D.normalizePairingTuple {m : ℕ} (κ : PartialPairing (Fin m)) (u : Fin m → Z4) : Fin m → Z4

Replace both occurrences of every pair by the label at their common canonical anchor.

Equations

• Anderson4D.normalizePairingTuple κ u i = u (Anderson4D.pairingAnchor κ i)

theorem Anderson4D.normalizePairingTuple_respectsPairing {m : ℕ} (κ : PartialPairing (Fin m)) (u : Fin m → Z4) : RespectsPairing κ (normalizePairingTuple κ u)

theorem Anderson4D.normalizePairingTuple_isPeriodLift {m : ℕ} {q : ℤ} {κ : PartialPairing (Fin m)} {u : Fin m → Z4} (hu : RespectsPairingModuloPeriod q κ u) : IsPeriodLift q (normalizePairingTuple κ u) u

theorem Anderson4D.normalizePairingTuple_mem_bounded {m M : ℕ} {κ : PartialPairing (Fin m)} {u : Fin m → Z4} (hu : u ∈ rdec_boundedTuples M m) : normalizePairingTuple κ u ∈ rdec_boundedTuples M m

Explicit finite-box weight amplification

def Anderson4D.windingBoxBase (M : ℕ) : ℝ

A common upper bound for every Japanese bracket squared between two points of [-M,M]⁴. The deliberately coarse 2^(M+1) form reuses the project's decomposition bound and makes the loss manifestly exponential.

Equations

• Anderson4D.windingBoxBase M = 1 + (2 ^ (M + 1)) ^ 2

theorem Anderson4D.windingBoxBase_pos (M : ℕ) : 0 < windingBoxBase M

theorem Anderson4D.latticeBracketSq_le_windingBoxBase {M : ℕ} {x y : Z4} (hx : ∀ (i : Fin dim), |x i| ≤ ↑M) (hy : ∀ (i : Fin dim), |y i| ≤ ↑M) : latticeBracketSq x y ≤ windingBoxBase M

theorem Anderson4D.one_le_latticeBracketSq (x y : Z4) : 1 ≤ latticeBracketSq x y

theorem Anderson4D.latticeEdgeWeight_le_one (x y : Z4) : latticeEdgeWeight x y ≤ 1

theorem Anderson4D.windingBoxBase_inv_le_latticeEdgeWeight {M : ℕ} {x y : Z4} (hx : ∀ (i : Fin dim), |x i| ≤ ↑M) (hy : ∀ (i : Fin dim), |y i| ≤ ↑M) : (windingBoxBase M)⁻¹ ≤ latticeEdgeWeight x y

noncomputable def Anderson4D.windingBoxEdgeFloor (M q : ℕ) : ℝ

Lower bound for the full adjacent-edge product in a box.

Equations

• Anderson4D.windingBoxEdgeFloor M q = ∏ _j : Anderson4D.AdjacentIndex (q + 1), (Anderson4D.windingBoxBase M)⁻¹

theorem Anderson4D.windingBoxEdgeFloor_pos (M q : ℕ) : 0 < windingBoxEdgeFloor M q

theorem Anderson4D.windingBoxEdgeFloor_eq_pow (M q : ℕ) : windingBoxEdgeFloor M q = (windingBoxBase M)⁻¹ ^ q

noncomputable def Anderson4D.windingBoxAmplification (M q : ℕ) : ℝ

Explicit loss for replacing an arbitrary bounded tuple by a bounded literally paired tuple.

Equations

• Anderson4D.windingBoxAmplification M q = Anderson4D.windingBoxBase M / Anderson4D.windingBoxEdgeFloor M q

theorem Anderson4D.windingBoxAmplification_nonneg (M q : ℕ) : 0 ≤ windingBoxAmplification M q

theorem Anderson4D.windingBoxAmplification_eq_pow (M q : ℕ) : windingBoxAmplification M q = windingBoxBase M ^ (q + 1)

theorem Anderson4D.reductionWeight_le_windingBoxBase {M q : ℕ} {y : Fin (q + 1) → Z4} (hy : y ∈ rdec_boundedTuples M (q + 1)) : reductionWeight q y ≤ windingBoxBase M

theorem Anderson4D.windingBoxEdgeFloor_le_reductionWeight {M q : ℕ} {y : Fin (q + 1) → Z4} (hy : y ∈ rdec_boundedTuples M (q + 1)) : windingBoxEdgeFloor M q ≤ reductionWeight q y

theorem Anderson4D.reductionWeight_le_windingBoxAmplification_mul {M q : ℕ} {u v : Fin (q + 1) → Z4} (hu : u ∈ rdec_boundedTuples M (q + 1)) (hv : v ∈ rdec_boundedTuples M (q + 1)) : reductionWeight q u ≤ windingBoxAmplification M q * reductionWeight q v

Any two tuples in the same finite box have comparable reduction weights with the explicit exponential loss above.

Reduction-index transport and the enlarged across sum

def Anderson4D.primitiveReductionIndexEquiv (n : ℕ) (hn : 1 ≤ n) : Fin (2 * n) ≃ Fin (2 * n - 1 + 1)

Arithmetic equivalence between the cell tuple and the literal carrier of reductionWeight (2n-1).

Equations

• Anderson4D.primitiveReductionIndexEquiv n hn = finCongr ⋯

theorem Anderson4D.primitiveReductionIndexEquiv_le_iff (n : ℕ) (hn : 1 ≤ n) (i j : Fin (2 * n)) : (primitiveReductionIndexEquiv n hn) i ≤ (primitiveReductionIndexEquiv n hn) j ↔ i ≤ j

theorem Anderson4D.primitiveReductionIndexEquiv_symm_le_iff (n : ℕ) (hn : 1 ≤ n) (i j : Fin (2 * n - 1 + 1)) : (primitiveReductionIndexEquiv n hn).symm i ≤ (primitiveReductionIndexEquiv n hn).symm j ↔ i ≤ j

def Anderson4D.primitiveReductionPairing (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : PartialPairing (Fin (2 * n - 1 + 1))

Transport a paper pairing to the literal reduction-weight carrier.

Equations

• Anderson4D.primitiveReductionPairing n hn κ = (Anderson4D.PartialPairing.congr (Anderson4D.primitiveReductionIndexEquiv n hn)) κ

theorem Anderson4D.primitiveReductionPairing_isFull {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} (hκ : κ.IsFull) : (primitiveReductionPairing n hn κ).IsFull

theorem Anderson4D.primitiveReductionPairing_isPrimitive {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} (hκ : IsPrimitive κ) : IsPrimitive (primitiveReductionPairing n hn κ)

theorem Anderson4D.primitiveReductionTupleOfCellTuple_mem_bounded {n M : ℕ} {hn : 1 ≤ n} {u : Fin (2 * n) → Z4} (hu : u ∈ rdec_boundedTuples M (2 * n)) : primitiveReductionTupleOfCellTuple n hn u ∈ rdec_boundedTuples M (2 * n - 1 + 1)

noncomputable def Anderson4D.allAcrossLatticeSum (M q : ℕ) (A : Finset (Fin (q + 1))) : ℝ

The finite enlargement of primitiveAcrossLatticeSum obtained by retaining every across pairing, including the nonprimitive ones.

Equations

• Anderson4D.allAcrossLatticeSum M q A = ∑ κ : Anderson4D.AcrossPairing A, Anderson4D.latticeChainSum M (q + 1) (Anderson4D.pairedReductionStatistic q A κ)

theorem Anderson4D.allAcrossLatticeSum_nonneg (M q : ℕ) (A : Finset (Fin (q + 1))) : 0 ≤ allAcrossLatticeSum M q A

noncomputable def Anderson4D.nonprimitiveAcrossLatticeSum (M q : ℕ) (A : Finset (Fin (q + 1))) : ℝ

The exact nonprimitive remainder introduced by the enlarged carrier.

Equations

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

theorem Anderson4D.nonprimitiveAcrossLatticeSum_nonneg (M q : ℕ) (A : Finset (Fin (q + 1))) : 0 ≤ nonprimitiveAcrossLatticeSum M q A

theorem Anderson4D.allAcrossLatticeSum_eq_primitive_add_nonprimitive (M q : ℕ) (A : Finset (Fin (q + 1))) : allAcrossLatticeSum M q A = primitiveAcrossLatticeSum M q A + nonprimitiveAcrossLatticeSum M q A

Exact ledger for the finite enlargement: no other terms are hidden.

Genuine winding-sector sum assembly

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

Real-valued version of the finite unwrapped cell sum.

Equations

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

theorem Anderson4D.primitiveUnwrappedReductionCellSum_eq_ofReal_realSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveUnwrappedReductionCellSum ε n hn κ = ENNReal.ofReal (primitiveUnwrappedReductionCellRealSum ε n hn κ)

theorem Anderson4D.primitivePeriodLiftFiberMultiplicity_le_carrier (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (u : Fin (2 * n) → Z4) : primitivePeriodLiftFiberMultiplicity ε n hn κ u ≤ (primitiveCanonicalCellCarrier ε n κ).card

Every actual period-lift fiber is bounded by the canonical copied-cell carrier cardinality.

theorem Anderson4D.card_primitivePeriodLiftImage_le_carrier (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : (primitivePeriodLiftImage ε n hn κ).card ≤ (primitiveCanonicalCellCarrier ε n κ).card

The number of winding sectors is bounded by the same genuine finite carrier.

theorem Anderson4D.normalized_reductionWeight_le_allAcrossLatticeSum {n M : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) {u : Fin (2 * n - 1 + 1) → Z4} (hu : u ∈ rdec_boundedTuples M (2 * n - 1 + 1)) : reductionWeight (2 * n - 1) (normalizePairingTuple (primitiveReductionPairing n hn κ) u) ≤ allAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

Every normalized tuple contributes to the enlarged across sum associated with the canonical lower half of the transported pairing.

theorem Anderson4D.normalized_reductionWeight_le_primitiveAcrossLatticeSum {n M : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) {u : Fin (2 * n - 1 + 1) → Z4} (hu : u ∈ rdec_boundedTuples M (2 * n - 1 + 1)) : reductionWeight (2 * n - 1) (normalizePairingTuple (primitiveReductionPairing n hn κ) u) ≤ primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

Primitive version of the preceding pointwise assembly. Transport along the arithmetic index equivalence preserves primitivity, so the canonical across pairing is an actual member of the existing primitive carrier.

theorem Anderson4D.exists_primitiveUnwrappedReductionCellRealSum_le_allAcross (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : ∃ (M : ℕ), primitiveUnwrappedReductionCellRealSum ε n hn κ ≤ ↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxAmplification M (2 * n - 1) * allAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

Winding-sector bridge.

For a genuine full pairing, the complete unwrapped cell sum is bounded by an explicitly finite carrier cardinality, the explicit exponential box amplification, and the existing across lattice machine enlarged only by its displayed nonprimitive remainder.

theorem Anderson4D.primitiveUnwrappedReductionCellSum_le_ofReal_allAcross (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : ∃ (M : ℕ), primitiveUnwrappedReductionCellSum ε n hn κ ≤ ENNReal.ofReal (↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxAmplification M (2 * n - 1) * allAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)))

theorem Anderson4D.primitiveUnwrappedReductionCellSum_le_primitive_add_remainder (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : ∃ (M : ℕ), primitiveUnwrappedReductionCellSum ε n hn κ ≤ ENNReal.ofReal (↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxBase M ^ (2 * n) * (primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)) + nonprimitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))))

Fully expanded endpoint of the winding-sector reduction. The amplification is the displayed power base^(2n), and the enlarged across carrier is split exactly into the existing primitive sum plus its explicit nonprimitive remainder.

theorem Anderson4D.primitiveUnwrappedReductionCellSum_le_primitive_add_remainder_of_mem (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) : ∃ (M : ℕ), primitiveUnwrappedReductionCellSum ε n hn κ ≤ ENNReal.ofReal (↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxBase M ^ (2 * n) * (primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)) + nonprimitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))))

theorem Anderson4D.exists_primitiveUnwrappedReductionCellRealSum_le_primitiveAcross (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : ∃ (M : ℕ), primitiveUnwrappedReductionCellRealSum ε n hn κ ≤ ↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxAmplification M (2 * n - 1) * primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

Real-valued winding-sector bridge directly into the existing primitive across sum.

theorem Anderson4D.primitiveUnwrappedReductionCellSum_le_primitiveAcross (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) : ∃ (M : ℕ), primitiveUnwrappedReductionCellSum ε n hn κ ≤ ENNReal.ofReal (↑(primitiveCanonicalCellCarrier ε n κ).card * windingBoxBase M ^ (2 * n) * primitiveAcrossLatticeSum M (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)))

Final direct ENNReal bridge for every member of primitiveFullPairings: the unwrapped R-51 sum is controlled by the existing primitive across lattice sum, with every loss explicit.