Period-lift reindexing for the primitive lattice reduction

The compatible-cell proof unwraps consecutive torus cells by integral period blocks. Consequently copied endpoints of a covariance pair need no longer be literally equal as points of Z4; they are equal modulo the compatible cell count. This file records that loss exactly.

It also supplies the missing lossless conversion from an arbitrary full PartialPairing to an AcrossPairing over its canonical lower-endpoint half. Thus the only remaining obstruction to feeding the unwrapped sum to primitiveAcrossLatticeSum is the nonzero period defect, not a mismatch between the two pairing representations.

Congruence modulo period-cell blocks

def Anderson4D.PeriodCongruent (q : ℤ) (a b : Z4) : Prop

Two lattice labels differ by an integral number of q-cell period blocks in every coordinate.

Equations

• Anderson4D.PeriodCongruent q a b = ∃ (k : Anderson4D.Z4), a = Anderson4D.translateCellIndex q k b

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidablePeriodCongruent (q : ℤ) (a b : Z4) : Decidable (PeriodCongruent q a b)

Equations

• Anderson4D.instDecidablePeriodCongruent q a b = Classical.propDecidable (Anderson4D.PeriodCongruent q a b)

theorem Anderson4D.periodCongruent_refl (q : ℤ) (a : Z4) : PeriodCongruent q a a

theorem Anderson4D.periodCongruent_symm {q : ℤ} {a b : Z4} (h : PeriodCongruent q a b) : PeriodCongruent q b a

theorem Anderson4D.periodCongruent_trans {q : ℤ} {a b c : Z4} (hab : PeriodCongruent q a b) (hbc : PeriodCongruent q b c) : PeriodCongruent q a c

theorem Anderson4D.periodCongruent_iff {q : ℤ} {a b : Z4} : PeriodCongruent q a b ↔ PeriodCongruent q b a

def Anderson4D.IsPeriodLift {m : ℕ} (q : ℤ) (u y : Fin m → Z4) : Prop

Pointwise period lift of a lattice tuple.

Equations

• Anderson4D.IsPeriodLift q u y = ∀ (i : Fin m), Anderson4D.PeriodCongruent q (u i) (y i)

def Anderson4D.RespectsPairingModuloPeriod {m : ℕ} (q : ℤ) (κ : PartialPairing (Fin m)) (u : Fin m → Z4) : Prop

Pairing compatibility after forgetting integral period blocks.

Equations

• Anderson4D.RespectsPairingModuloPeriod q κ u = ∀ (i : Fin m), Anderson4D.PeriodCongruent q (u (κ i)) (u i)

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidableRespectsPairingModuloPeriod {m : ℕ} (q : ℤ) (κ : PartialPairing (Fin m)) (u : Fin m → Z4) : Decidable (RespectsPairingModuloPeriod q κ u)

Equations

• Anderson4D.instDecidableRespectsPairingModuloPeriod q κ u = Anderson4D.instDecidableRespectsPairingModuloPeriod._aux_1 q κ u

theorem Anderson4D.IsPeriodLift.respectsPairingModuloPeriod {m : ℕ} {q : ℤ} {κ : PartialPairing (Fin m)} {u y : Fin m → Z4} (hu : IsPeriodLift q u y) (hy : RespectsPairing κ y) : RespectsPairingModuloPeriod q κ u

theorem Anderson4D.nearestPeriodTranslate_periodCongruent (q : ℤ) (a b : Z4) : PeriodCongruent q (nearestPeriodTranslate q a b) b

theorem Anderson4D.unwrapLatticePath_forall₂_periodCongruent (q : ℤ) (a : Z4) (ys : List Z4) : List.Forall₂ (PeriodCongruent q) (unwrapLatticePath q a ys) ys

Recursive path unwrapping is pointwise a period lift of the original path. No positivity or nonvanishing hypothesis is needed.

theorem Anderson4D.primitiveUnwrappedCellList_forall₂_periodCongruent (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : List.Forall₂ (PeriodCongruent (compatibleCellCount ε)) (primitiveUnwrappedCellList ε n hn y) (primitiveOriginalCellList n hn y)

The complete primitive unwrapped path, including its fixed endpoints, is pointwise congruent to the canonical copied-cell path.

theorem Anderson4D.primitiveUnwrappedCellTuple_isPeriodLift (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : IsPeriodLift (compatibleCellCount ε) (primitiveUnwrappedCellTuple ε n hn y) y

Tuple form of the preceding period-lift statement.

theorem Anderson4D.primitiveUnwrappedCellTuple_respectsPairingModuloPeriod (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (y : Fin (2 * n) → Z4) (hy : RespectsPairing κ y) : RespectsPairingModuloPeriod (compatibleCellCount ε) κ (primitiveUnwrappedCellTuple ε n hn y)

The exact compatibility retained by the unwrapped tuple. This replaces the false claim that path unwrapping preserves RespectsPairing literally.

Full partial pairings as across pairings

def Anderson4D.pairingLowerHalf {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m)

Canonical choice of one endpoint from every pair: the smaller endpoint.

Equations

• Anderson4D.pairingLowerHalf κ = {i : Fin m | i < κ i}

@[simp]

theorem Anderson4D.mem_pairingLowerHalf {m : ℕ} {κ : PartialPairing (Fin m)} {i : Fin m} : i ∈ pairingLowerHalf κ ↔ i < κ i

theorem Anderson4D.apply_notMem_pairingLowerHalf {m : ℕ} (κ : PartialPairing (Fin m)) {i : Fin m} (hi : i ∈ pairingLowerHalf κ) : κ i ∉ pairingLowerHalf κ

theorem Anderson4D.apply_mem_pairingLowerHalf_of_notMem {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) {i : Fin m} (hi : i ∉ pairingLowerHalf κ) : κ i ∈ pairingLowerHalf κ

def Anderson4D.fullPairingToAcross {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : AcrossPairing (pairingLowerHalf κ)

A full pairing, oriented from each smaller endpoint to its larger mate.

Equations

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

theorem Anderson4D.acrossToPartialPairing_fullPairingToAcross {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : acrossToPartialPairing (pairingLowerHalf κ) (fullPairingToAcross κ hfull) = κ

Extending the canonical across pairing recovers the original full partial pairing literally.

theorem Anderson4D.fullPairingToAcross_isPrimitive {m : ℕ} {κ : PartialPairing (Fin m)} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : IsPrimitiveAcross (pairingLowerHalf κ) (fullPairingToAcross κ hfull)

theorem Anderson4D.fullPairingToAcross_mem_primitiveAcrossPairingFinset {m : ℕ} {κ : PartialPairing (Fin m)} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : fullPairingToAcross κ hfull ∈ primitiveAcrossPairingFinset (pairingLowerHalf κ)

theorem Anderson4D.sum_primitiveFullPairings_le_sum_across {m : ℕ} (F : PartialPairing (Fin m) → ℝ) (hF : ∀ (κ : PartialPairing (Fin m)), 0 ≤ F κ) : ∑ κ : PartialPairing (Fin m) with κ.IsFull ∧ IsPrimitive κ, F κ ≤ ∑ A : Finset (Fin m), ∑ κ ∈ primitiveAcrossPairingFinset A, F (acrossToPartialPairing A κ)

Every primitive full partial pairing occurs in the all-cuts across carrier. The map is injective because extending an across pairing recovers the source pairing.

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

The literal PartialPairing version of the bounded primitive lattice sum, before choosing a half for each full pairing.

Equations

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

theorem Anderson4D.primitivePartialLatticeSum_le_sum_primitiveAcrossLatticeSum (M q : ℕ) : primitivePartialLatticeSum M q ≤ ∑ A : Finset (Fin (q + 1)), primitiveAcrossLatticeSum M q A

Complete full-pairing-to-half assembly at lattice level. Summing over all cuts can only overcount, and every primitive full pairing is represented by its canonical lower-endpoint cut.

The finite period-lift image and its exact fibers

noncomputable def Anderson4D.primitiveCanonicalCellCarrier (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) : Finset (Fin (2 * n) → Z4)

Canonical copied-cell carrier for one partial pairing.

Equations

• Anderson4D.primitiveCanonicalCellCarrier ε n κ = Finset.filter (Anderson4D.RespectsPairing κ) (Fintype.piFinset fun (x : Fin (2 * n)) => Anderson4D.torusGrid (Anderson4D.compatibleMeshSize ε))

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

Image of the canonical copied-cell carrier under chain unwrapping.

Equations

• Anderson4D.primitivePeriodLiftImage ε n hn κ = Finset.image (Anderson4D.primitiveUnwrappedCellTuple ε n hn) (Anderson4D.primitiveCanonicalCellCarrier ε n κ)

@[simp]

theorem Anderson4D.mem_primitivePeriodLiftImage {ε : ℝ} {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} {u : Fin (2 * n) → Z4} : u ∈ primitivePeriodLiftImage ε n hn κ ↔ ∃ y ∈ primitiveCanonicalCellCarrier ε n κ, primitiveUnwrappedCellTuple ε n hn y = u

theorem Anderson4D.mem_primitivePeriodLiftImage_respectsModuloPeriod {ε : ℝ} {n : ℕ} {hn : 1 ≤ n} {κ : PartialPairing (Fin (2 * n))} {u : Fin (2 * n) → Z4} (hu : u ∈ primitivePeriodLiftImage ε n hn κ) : RespectsPairingModuloPeriod (compatibleCellCount ε) κ u

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

Cast a Fin (2n) tuple to the arithmetically equal carrier expected by reductionWeight (2n-1).

Equations

• Anderson4D.primitiveReductionTupleOfCellTuple n hn u i = u (Fin.cast ⋯ i)

@[simp]

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

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

Exact multiplicity of one unwrapped tuple in the finite canonical copied-cell carrier. Boundary representatives are intentionally retained, so this fiber need not have cardinality one.

Equations

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

theorem Anderson4D.primitiveUnwrappedReductionCellSum_eq_periodLiftFibers (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : primitiveUnwrappedReductionCellSum ε n hn κ = ∑ u ∈ primitivePeriodLiftImage ε n hn κ, ↑(primitivePeriodLiftFiberMultiplicity ε n hn κ u) * ENNReal.ofReal (reductionWeight (2 * n - 1) (primitiveReductionTupleOfCellTuple n hn u))

Exact finite fiber decomposition of the R-51 remainder. This is a real reindexing identity; it neither assumes injectivity at fundamental-domain boundaries nor replaces the desired estimate by a certificate.

theorem Anderson4D.exists_primitivePeriodLiftImage_bounded (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) : ∃ (M : ℕ), ∀ u ∈ primitivePeriodLiftImage ε n hn κ, u ∈ rdec_boundedTuples M (2 * n)

Although unwrapped representatives can leave every a priori fixed box, their finite image is contained in some honest rdec_boundedTuples box. The bound is extracted from the actual finite image, not postulated.