Copied paired labels in the bounded lattice box

This file implements the finite reindexing used literally in paper §5.1: choose the label at one endpoint of each covariance pair, copy it to the other endpoint, and retain the resulting tuple in one bounded box. No occurrence-wise path unwrapping is used.

The main conclusions have no fiber-cardinality or winding amplification: the copied-label carrier embeds injectively into the bounded tuple carrier used by the lattice estimate, and its full primitive-pairing sum is bounded by the existing all-cuts primitive across-pairing sum.

The paper's finite box

noncomputable def Anderson4D.primitiveCopiedBoxRadius (ε : ℝ) : ℕ

Natural half-width of the canonical copied-label box.

Equations

• Anderson4D.primitiveCopiedBoxRadius ε = (Anderson4D.torusGridRadius (Anderson4D.compatibleMeshSize ε)).natAbs

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

theorem Anderson4D.primitiveCopiedBoxRadius_cast {ε : ℝ} (hε : 0 < ε) : ↑(primitiveCopiedBoxRadius ε) = torusGridRadius (compatibleMeshSize ε)

theorem Anderson4D.mem_torusGrid_compatible_abs_le {ε : ℝ} (hε : 0 < ε) {y : Z4} (hy : y ∈ torusGrid (compatibleMeshSize ε)) (i : Fin dim) : |y i| ≤ ↑(primitiveCopiedBoxRadius ε)

Every label in the canonical torus grid lies in the single natural integer box consumed by rdec_boundedTuples.

theorem Anderson4D.primitiveCanonicalCellCarrier_mem_bounded {ε : ℝ} (hε : 0 < ε) {n : ℕ} {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : y ∈ rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n)

Tuple form of the preceding bounded-box inclusion.

Choose once, copy to the paired occurrence

theorem Anderson4D.pairingAnchor_mem_pairingLowerHalf {m : ℕ} {κ : PartialPairing (Fin m)} (hfull : κ.IsFull) (i : Fin m) : pairingAnchor κ i ∈ pairingLowerHalf κ

theorem Anderson4D.pairingAnchor_eq_self_of_mem_pairingLowerHalf {m : ℕ} {κ : PartialPairing (Fin m)} {i : Fin m} (hi : i ∈ pairingLowerHalf κ) : pairingAnchor κ i = i

theorem Anderson4D.card_pairingLowerHalf_eq {n : ℕ} (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (pairingLowerHalf κ).card = n

A full pairing on 2n positions has exactly n independently chosen labels; the other n labels are literal copies.

def Anderson4D.copiedPairingLabels {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(pairingLowerHalf κ) → Z4) : Fin m → Z4

Extend labels chosen only at the smaller endpoint of each pair by copying the chosen value to its mate.

Equations

• Anderson4D.copiedPairingLabels κ hfull a i = a ⟨Anderson4D.pairingAnchor κ i, ⋯⟩

theorem Anderson4D.copiedPairingLabels_respectsPairing {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(pairingLowerHalf κ) → Z4) : RespectsPairing κ (copiedPairingLabels κ hfull a)

def Anderson4D.restrictToPairingLowerHalf {m : ℕ} (κ : PartialPairing (Fin m)) (y : { y : Fin m → Z4 // RespectsPairing κ y }) : ↥(pairingLowerHalf κ) → Z4

Restriction to the canonical smaller endpoint of each pair.

Equations

• Anderson4D.restrictToPairingLowerHalf κ y i = ↑y ↑i

def Anderson4D.copiedPairingLabelsEquiv {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : (↥(pairingLowerHalf κ) → Z4) ≃ { y : Fin m → Z4 // RespectsPairing κ y }

Literal formulation of the paper's copied-label sentence: for a full pairing, choosing one label per lower endpoint is equivalent to a full tuple satisfying y_{κ(i)} = y_i.

Equations

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

Lossless arithmetic reindexing

@[reducible, inline]

abbrev Anderson4D.primitiveCopiedReductionTuple (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : Fin (2 * n - 1 + 1) → Z4

The copied tuple, cast to the arithmetically equal carrier on which reductionWeight (2n-1) is defined.

Equations

• Anderson4D.primitiveCopiedReductionTuple n hn y = Anderson4D.primitiveReductionTupleOfCellTuple n hn y

theorem Anderson4D.primitiveCopiedReductionTuple_injective (n : ℕ) (hn : 1 ≤ n) : Function.Injective (primitiveCopiedReductionTuple n hn)

def Anderson4D.primitiveCopiedSourceTuple (n : ℕ) (hn : 1 ≤ n) (u : Fin (2 * n - 1 + 1) → Z4) : Fin (2 * n) → Z4

Inverse arithmetic cast, from the reduction carrier back to the paper's Fin (2n) labels.

Equations

• Anderson4D.primitiveCopiedSourceTuple n hn u i = u ((Anderson4D.primitiveReductionIndexEquiv n hn) i)

@[simp]

theorem Anderson4D.primitiveCopiedSourceTuple_reductionTuple (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : primitiveCopiedSourceTuple n hn (primitiveCopiedReductionTuple n hn y) = y

@[simp]

theorem Anderson4D.primitiveCopiedReductionTuple_sourceTuple (n : ℕ) (hn : 1 ≤ n) (u : Fin (2 * n - 1 + 1) → Z4) : primitiveCopiedReductionTuple n hn (primitiveCopiedSourceTuple n hn u) = u

noncomputable def Anderson4D.primitiveCopiedReductionCarrier (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : Finset (Fin (2 * n - 1 + 1) → Z4)

Image of the copied-label carrier on the literal reduction carrier.

Equations

• Anderson4D.primitiveCopiedReductionCarrier ε n hn κ = Finset.image (Anderson4D.primitiveCopiedReductionTuple n hn) (Anderson4D.primitiveCanonicalCellCarrier ε n κ)

@[simp]

theorem Anderson4D.mem_primitiveCopiedReductionCarrier {ε : ℝ} {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} {u : Fin (2 * n - 1 + 1) → Z4} : u ∈ primitiveCopiedReductionCarrier ε n hn κ ↔ ∃ y ∈ primitiveCanonicalCellCarrier ε n κ, primitiveCopiedReductionTuple n hn y = u

theorem Anderson4D.primitiveCopiedReductionTuple_respectsPairing {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : RespectsPairing κ y) : RespectsPairing (primitiveReductionPairing n hn κ) (primitiveCopiedReductionTuple n hn y)

Reindexing preserves the copied-pair equalities literally.

theorem Anderson4D.primitiveCopiedReductionCarrier_respectsPairing {ε : ℝ} {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} {u : Fin (2 * n - 1 + 1) → Z4} (hu : u ∈ primitiveCopiedReductionCarrier ε n hn κ) : RespectsPairing (primitiveReductionPairing n hn κ) u

theorem Anderson4D.primitiveCopiedReductionCarrier_subset_bounded {ε : ℝ} (hε : 0 < ε) {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} : primitiveCopiedReductionCarrier ε n hn κ ⊆ rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)

The copied carrier enters the bounded lattice box injectively, with no winding-sector multiplicity.

theorem Anderson4D.primitiveCopiedReductionCarrier_eq_filter_bounded {ε : ℝ} (hε : 0 < ε) {n : ℕ} {hn : 1 ≤ n} (κ : PartialPairing (Fin (2 * n))) : primitiveCopiedReductionCarrier ε n hn κ = Finset.filter (RespectsPairing (primitiveReductionPairing n hn κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1))

Exact carrier identity: after the arithmetic cast, the paper's copied grid is precisely the bounded box filtered by the transported pairing constraint.

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

Exact fiber multiplicity of the copied-label arithmetic reindexing.

Equations

• Anderson4D.primitiveCopiedReductionFiberMultiplicity ε n hn κ u = {y ∈ Anderson4D.primitiveCanonicalCellCarrier ε n κ | Anderson4D.primitiveCopiedReductionTuple n hn y = u}.card

theorem Anderson4D.primitiveCopiedReductionFiberMultiplicity_eq_ite (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (u : Fin (2 * n - 1 + 1) → Z4) : primitiveCopiedReductionFiberMultiplicity ε n hn κ u = if u ∈ primitiveCopiedReductionCarrier ε n hn κ then 1 else 0

theorem Anderson4D.primitiveCopiedReductionFiberMultiplicity_le_one (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (u : Fin (2 * n - 1 + 1) → Z4) : primitiveCopiedReductionFiberMultiplicity ε n hn κ u ≤ 1

theorem Anderson4D.sum_copiedLabels_filter_eq_boundedPairing_filter {ε : ℝ} (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) → ℝ) : ∑ 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

Lossless reindexing remains exact after imposing any decidable support predicate on the reduction tuple. In particular, the continuous layer may retain its fixed-endpoint (or bounded endpoint-neighbourhood) constraint instead of enlarging to all translations in the box.

Finite sums without amplification

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

The exact real-valued copied-label sum for one pairing.

Equations

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

theorem Anderson4D.primitiveCopiedReductionCellRealSum_eq_carrier (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveCopiedReductionCellRealSum ε n hn κ = ∑ u ∈ primitiveCopiedReductionCarrier ε n hn κ, reductionWeight (2 * n - 1) u

theorem Anderson4D.primitiveCopiedReductionCellRealSum_eq_latticeChainSum {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveCopiedReductionCellRealSum ε n hn κ = latticeChainSum (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1) fun (u : Fin (2 * n - 1 + 1) → Fin 4 → ℤ) => if RespectsPairing (primitiveReductionPairing n hn κ) u then reductionWeight (2 * n - 1) u else 0

Exact fixed-pairing reindexing into the bounded lattice sum.

theorem Anderson4D.primitiveCopiedReductionCellRealSum_le_latticeChainSum {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveCopiedReductionCellRealSum ε n hn κ ≤ latticeChainSum (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1) fun (u : Fin (2 * n - 1 + 1) → Fin 4 → ℤ) => if RespectsPairing (primitiveReductionPairing n hn κ) u then reductionWeight (2 * n - 1) u else 0

For a fixed paper pairing, the copied-label sum is a literal subsum of the bounded lattice sum for the transported pairing. There is no fiber-cardinality multiplier and no comparison of unrelated weights.

theorem Anderson4D.primitiveCopiedReductionCellRealSum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : primitiveCopiedReductionCellRealSum ε n hn κ ≤ primitiveAcrossLatticeSum (primitiveCopiedBoxRadius ε) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

The fixed-pairing copied sum enters its canonical primitive across carrier without any M- or ε-dependent prefactor.

The full primitive-pairing carrier

noncomputable def Anderson4D.primitiveCopiedPrimitiveRealSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) : ℝ

Paper (5.5), before fixing the lower-endpoint set A: sum the copied bounded-box statistic over every primitive full pairing.

Equations

• Anderson4D.primitiveCopiedPrimitiveRealSum ε n hn = ∑ κ ∈ Anderson4D.primitiveFullPairings n, Anderson4D.primitiveCopiedReductionCellRealSum ε n hn κ

theorem Anderson4D.primitiveCopiedPrimitiveRealSum_le_partialLatticeSum {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) : primitiveCopiedPrimitiveRealSum ε n hn ≤ primitivePartialLatticeSum (primitiveCopiedBoxRadius ε) (2 * n - 1)

Lossless passage from all source pairings to the literal PartialPairing bounded-lattice carrier. The outer transport is injective, so this step introduces no pairing-count factor either.

theorem Anderson4D.primitiveCopiedPrimitiveRealSum_le_sum_primitiveAcross {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) : primitiveCopiedPrimitiveRealSum ε n hn ≤ ∑ A : Finset (Fin (2 * n - 1 + 1)), primitiveAcrossLatticeSum (primitiveCopiedBoxRadius ε) (2 * n - 1) A

Final copied-label finite reindexing: the full primitive sum is bounded by the existing all-cuts across-pairing machine with coefficient exactly one. The only overcount is the paper's harmless choice of A; no factor depends on the box radius or on ε.

ENNReal form consumed by the cell-integral layer

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

Nonnegative extended-real form of one copied-pairing sum.

Equations

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

theorem Anderson4D.primitiveCopiedReductionCellSum_eq_ofReal (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveCopiedReductionCellSum ε n hn κ = ENNReal.ofReal (primitiveCopiedReductionCellRealSum ε n hn κ)

theorem Anderson4D.primitiveCopiedReductionCellSum_factor {a b q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : ∑ y ∈ primitiveCanonicalCellCarrier ε n κ, ENNReal.ofReal q * (ENNReal.ofReal (a * reductionWeight (2 * n - 1) (primitiveCopiedReductionTuple n hn y)) + ENNReal.ofReal (b * reductionWeight (2 * n - 1) (primitiveCopiedReductionTuple n hn y))) = ENNReal.ofReal q * (ENNReal.ofReal a + ENNReal.ofReal b) * primitiveCopiedReductionCellSum ε n hn κ

Drop-in scalar ledger for a direct copied-cell proof of paper (5.3).

theorem Anderson4D.primitiveCopiedReductionCellSum_le_ofReal_primitiveAcross {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : primitiveCopiedReductionCellSum ε n hn κ ≤ ENNReal.ofReal (primitiveAcrossLatticeSum (primitiveCopiedBoxRadius ε) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)))

noncomputable def Anderson4D.primitiveCopiedPrimitiveSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) : ENNReal

Extended-real sum over all primitive pairings.

Equations

• Anderson4D.primitiveCopiedPrimitiveSum ε n hn = ∑ κ ∈ Anderson4D.primitiveFullPairings n, Anderson4D.primitiveCopiedReductionCellSum ε n hn κ

theorem Anderson4D.primitiveCopiedPrimitiveSum_eq_ofReal (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) : primitiveCopiedPrimitiveSum ε n hn = ENNReal.ofReal (primitiveCopiedPrimitiveRealSum ε n hn)

theorem Anderson4D.primitiveCopiedPrimitiveSum_le_ofReal_sum_primitiveAcross {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) : primitiveCopiedPrimitiveSum ε n hn ≤ ENNReal.ofReal (∑ A : Finset (Fin (2 * n - 1 + 1)), primitiveAcrossLatticeSum (primitiveCopiedBoxRadius ε) (2 * n - 1) A)

Analytic boundary

The finite step is lossless. A direct proof of the paper's cell estimate (5.3) uses primitiveCopiedReductionTuple n hn y, while retaining the endpoint support predicate supplied by the endpoint-fixed integral. The current theorem primitiveInsertedIntegrand_fiber_exhaustive_order instead produces primitiveUnwrappedReductionTuple; its weight cannot be transported to the copied tuple uniformly because path unwrapping destroys literal pairing. sum_copiedLabels_filter_eq_boundedPairing_filter is the corresponding finite regrouping identity.