Periodic quotient graphs for the primitive permutation sum

For a full pairing, identify the two positions of every covariance pair. The linear word path descends to a connected multigraph on the n pair vertices. Its simple underlying graph has a spanning tree with n - 1 edges. Lifting labels along those tree edges makes every retained edge an ordinary no-wrap lattice edge; the other n word adjacencies are the genuine winding/cycle edges and must be treated as skipped edges.

This file develops that quotient interface without comparing a periodic edge pointwise to the canonical Euclidean edge.

Mapping connected graphs by a possibly non-injective function

theorem Anderson4D.SimpleGraph.reachable_map_function {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (f : V → W) {u v : V} (h : G.Reachable u v) : (SimpleGraph.map f G).Reachable (f u) (f v)

Mapping vertices may collapse an edge to a point. After deleting those loops, reachability is still preserved by SimpleGraph.map.

theorem Anderson4D.SimpleGraph.Connected.map_function {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (hG : G.Connected) (f : V → W) (hf : Function.Surjective f) : (SimpleGraph.map f G).Connected

A surjective image of a connected graph is connected even when some source edges collapse to loops.

The word path modulo a full pairing

@[reducible, inline]

abbrev Anderson4D.PairingVertex {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m)

Vertices of the quotient word graph: one canonical lower endpoint per pair.

Equations

• Anderson4D.PairingVertex κ = Anderson4D.pairingLowerHalf κ

def Anderson4D.pairingVertex {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (i : Fin m) : ↥(PairingVertex κ)

Quotient map from word positions to their covariance-pair vertex.

Equations

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

@[simp]

theorem Anderson4D.pairingVertex_apply {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (i : Fin m) : pairingVertex κ hfull (κ i) = pairingVertex κ hfull i

@[simp]

theorem Anderson4D.pairingVertex_lower {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (i : ↥(PairingVertex κ)) : pairingVertex κ hfull ↑i = i

theorem Anderson4D.pairingVertex_surjective {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Function.Surjective (pairingVertex κ hfull)

def Anderson4D.pairingQuotientGraph {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : SimpleGraph ↥(PairingVertex κ)

The simple graph obtained from the linear word path after identifying paired positions. Parallel word edges are deliberately forgotten here; they reappear below as distinct adjacency indices.

Equations

• Anderson4D.pairingQuotientGraph κ hfull = SimpleGraph.map (Anderson4D.pairingVertex κ hfull) (SimpleGraph.pathGraph m)

theorem Anderson4D.pairingQuotientGraph_connected {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : (pairingQuotientGraph κ hfull).Connected

noncomputable def Anderson4D.pairingQuotientTree {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : SimpleGraph ↥(PairingVertex κ)

A chosen spanning tree of the pairing quotient graph.

Equations

• Anderson4D.pairingQuotientTree hm κ hfull = Classical.choose ⋯

theorem Anderson4D.pairingQuotientTree_le {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : pairingQuotientTree hm κ hfull ≤ pairingQuotientGraph κ hfull

theorem Anderson4D.pairingQuotientTree_isTree {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : (pairingQuotientTree hm κ hfull).IsTree

theorem Anderson4D.pairingQuotientTree_edge_card {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : Nat.card ↑(pairingQuotientTree ⋯ κ hfull).edgeSet = n - 1

Choosing the n - 1 word edges of the quotient spanning tree

def Anderson4D.wordQuotientEdge {m : ℕ} (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (j : AdjacentIndex m) : Sym2 ↥(PairingVertex κ)

The unordered pair of quotient vertices carried by one adjacency of the original word. It may be diagonal when two paired occurrences are adjacent.

Equations

• Anderson4D.wordQuotientEdge κ hfull j = s(Anderson4D.pairingVertex κ hfull ↑j, Anderson4D.pairingVertex κ hfull (Anderson4D.adjacentSucc j))

theorem Anderson4D.exists_wordAdjacency_represents_treeEdge {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (e : ↑(pairingQuotientTree hm κ hfull).edgeSet) : ∃ (j : AdjacentIndex m), wordQuotientEdge κ hfull j = ↑e

Every edge of the quotient spanning tree is represented by at least one actual adjacency index of the original word.

noncomputable def Anderson4D.treeEdgeWordRepresentative {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (e : ↑(pairingQuotientTree hm κ hfull).edgeSet) : AdjacentIndex m

A deterministic representative word adjacency for a quotient-tree edge.

Equations

• Anderson4D.treeEdgeWordRepresentative hm κ hfull e = Classical.choose ⋯

theorem Anderson4D.treeEdgeWordRepresentative_spec {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (e : ↑(pairingQuotientTree hm κ hfull).edgeSet) : wordQuotientEdge κ hfull (treeEdgeWordRepresentative hm κ hfull e) = ↑e

theorem Anderson4D.treeEdgeWordRepresentative_injective {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Function.Injective (treeEdgeWordRepresentative hm κ hfull)

noncomputable def Anderson4D.quotientTreeWordEdges {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Finset (AdjacentIndex m)

The selected word adjacencies representing the quotient spanning tree.

Equations

• Anderson4D.quotientTreeWordEdges hm κ hfull = Finset.image (Anderson4D.treeEdgeWordRepresentative hm κ hfull) Finset.univ

theorem Anderson4D.card_quotientTreeWordEdges {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (quotientTreeWordEdges ⋯ κ hfull).card = n - 1

noncomputable def Anderson4D.quotientCycleWordEdges {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Finset (AdjacentIndex m)

The genuine winding/cycle adjacencies: every word edge not selected for the quotient spanning tree.

Equations

• Anderson4D.quotientCycleWordEdges hm κ hfull = Finset.univ \ Anderson4D.quotientTreeWordEdges hm κ hfull

theorem Anderson4D.card_quotientCycleWordEdges {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (quotientCycleWordEdges ⋯ κ hfull).card = n

A full pairing on 2n positions has exactly n cycle/skipped word edges after retaining a quotient spanning tree.

Rooted tree lifts of the pair labels

def Anderson4D.pairingQuotientRoot {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : ↥(PairingVertex κ)

Root pair vertex, chosen as the pair containing word position zero.

Equations

• Anderson4D.pairingQuotientRoot hm κ hfull = Anderson4D.pairingVertex κ hfull ⟨0, hm⟩

noncomputable def Anderson4D.pairingQuotientParent {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (v : ↥(PairingVertex κ)) : ↥(PairingVertex κ)

The chosen quotient-tree parent.

Equations

• Anderson4D.pairingQuotientParent hm κ hfull v = Anderson4D.SimpleGraph.parentTowardRoot (Anderson4D.pairingQuotientTree hm κ hfull) ⋯ (Anderson4D.pairingQuotientRoot hm κ hfull) v

@[simp]

theorem Anderson4D.pairingQuotientParent_root {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : pairingQuotientParent hm κ hfull (pairingQuotientRoot hm κ hfull) = pairingQuotientRoot hm κ hfull

theorem Anderson4D.pairingQuotientTree_adj_parent {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) {v : ↥(PairingVertex κ)} (hv : v ≠ pairingQuotientRoot hm κ hfull) : (pairingQuotientTree hm κ hfull).Adj v (pairingQuotientParent hm κ hfull v)

theorem Anderson4D.pairingQuotientTree_dist_parent_lt {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) {v : ↥(PairingVertex κ)} (hv : v ≠ pairingQuotientRoot hm κ hfull) : (pairingQuotientTree hm κ hfull).dist (pairingQuotientParent hm κ hfull v) (pairingQuotientRoot hm κ hfull) < (pairingQuotientTree hm κ hfull).dist v (pairingQuotientRoot hm κ hfull)

@[irreducible]

noncomputable def Anderson4D.quotientTreeLift {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (q : ℤ) (a : ↥(PairingVertex κ) → Z4) (v : ↥(PairingVertex κ)) : Z4

Lift one label per covariance pair recursively from the quotient root. Every non-root label is replaced by the whole-period translate nearest to its already lifted parent.

Equations

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

theorem Anderson4D.quotientTreeLift_eq_root {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (q : ℤ) (a : ↥(PairingVertex κ) → Z4) : quotientTreeLift hm κ hfull q a (pairingQuotientRoot hm κ hfull) = a (pairingQuotientRoot hm κ hfull)

theorem Anderson4D.quotientTreeLift_eq_nearest_parent {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (q : ℤ) (a : ↥(PairingVertex κ) → Z4) {v : ↥(PairingVertex κ)} (hv : v ≠ pairingQuotientRoot hm κ hfull) : quotientTreeLift hm κ hfull q a v = nearestPeriodTranslate q (quotientTreeLift hm κ hfull q a (pairingQuotientParent hm κ hfull v)) (a v)

theorem Anderson4D.latticeTorusCenter_quotientTreeLift {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) (v : ↥(PairingVertex κ)) : latticeTorusCenter δ (quotientTreeLift hm κ hfull q a v) = latticeTorusCenter δ (a v)

Every recursively lifted label has the same torus centre as its original pair label.

theorem Anderson4D.quotientTreeLift_parent_noWrap {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) {v : ↥(PairingVertex κ)} (hv : v ≠ pairingQuotientRoot hm κ hfull) : LatticeEdgeNoWrap δ (quotientTreeLift hm κ hfull q a (pairingQuotientParent hm κ hfull v)) (quotientTreeLift hm κ hfull q a v)

Every rooted quotient-tree edge is an exact no-wrap edge after lifting.

theorem Anderson4D.periodicCellEdgeWeight_quotientTreeLift_parent {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) {v : ↥(PairingVertex κ)} (hv : v ≠ pairingQuotientRoot hm κ hfull) : periodicCellEdgeWeight δ (quotientTreeLift hm κ hfull q a v) (quotientTreeLift hm κ hfull q a (pairingQuotientParent hm κ hfull v)) = latticeEdgeWeight (quotientTreeLift hm κ hfull q a v) (quotientTreeLift hm κ hfull q a (pairingQuotientParent hm κ hfull v))

Hence the periodic edge on a rooted tree edge is literally its ordinary lattice edge weight.

Parent-oriented word edges

def Anderson4D.nonrootPairingVertices {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Finset ↥(PairingVertex κ)

Non-root pair vertices, the natural carrier of rooted tree edges.

Equations

• Anderson4D.nonrootPairingVertices hm κ hfull = Finset.univ.erase (Anderson4D.pairingQuotientRoot hm κ hfull)

@[simp]

theorem Anderson4D.mem_nonrootPairingVertices {m : ℕ} {hm : 0 < m} {κ : PartialPairing (Fin m)} {hfull : κ.IsFull} {v : ↥(PairingVertex κ)} : v ∈ nonrootPairingVertices hm κ hfull ↔ v ≠ pairingQuotientRoot hm κ hfull

theorem Anderson4D.card_nonrootPairingVertices {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (nonrootPairingVertices ⋯ κ hfull).card = n - 1

theorem Anderson4D.exists_wordAdjacency_represents_parentEdge {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (v : ↥(PairingVertex κ)) (hv : v ≠ pairingQuotientRoot hm κ hfull) : ∃ (j : AdjacentIndex m), wordQuotientEdge κ hfull j = s(v, pairingQuotientParent hm κ hfull v)

Any rooted quotient-tree edge has an actual word-adjacency witness.

noncomputable def Anderson4D.parentEdgeWordRepresentative {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (v : ↥(nonrootPairingVertices hm κ hfull)) : AdjacentIndex m

Chosen word adjacency for a rooted quotient-tree edge.

Equations

• Anderson4D.parentEdgeWordRepresentative hm κ hfull v = Classical.choose ⋯

theorem Anderson4D.parentEdgeWordRepresentative_spec {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (v : ↥(nonrootPairingVertices hm κ hfull)) : wordQuotientEdge κ hfull (parentEdgeWordRepresentative hm κ hfull v) = s(↑v, pairingQuotientParent hm κ hfull ↑v)

theorem Anderson4D.parentEdgeWordRepresentative_injective {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Function.Injective (parentEdgeWordRepresentative hm κ hfull)

noncomputable def Anderson4D.quotientParentWordEdges {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Finset (AdjacentIndex m)

Parent-oriented selected word adjacencies.

Equations

• Anderson4D.quotientParentWordEdges hm κ hfull = Finset.image (Anderson4D.parentEdgeWordRepresentative hm κ hfull) (Anderson4D.nonrootPairingVertices hm κ hfull).attach

theorem Anderson4D.card_quotientParentWordEdges {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (quotientParentWordEdges ⋯ κ hfull).card = n - 1

noncomputable def Anderson4D.quotientParentCycleEdges {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) : Finset (AdjacentIndex m)

Cycle/skipped adjacencies for the parent-oriented lift.

Equations

• Anderson4D.quotientParentCycleEdges hm κ hfull = Finset.univ \ Anderson4D.quotientParentWordEdges hm κ hfull

theorem Anderson4D.card_quotientParentCycleEdges {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) : (quotientParentCycleEdges ⋯ κ hfull).card = n

The quotient-tree word and its skipped-chain comparison

noncomputable def Anderson4D.quotientTreeLiftedWord {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (q : ℤ) (a : ↥(PairingVertex κ) → Z4) : Fin m → Z4

Literal paired word obtained from the rooted whole-period lifts.

Equations

• Anderson4D.quotientTreeLiftedWord hm κ hfull q a i = Anderson4D.quotientTreeLift hm κ hfull q a (Anderson4D.pairingVertex κ hfull i)

theorem Anderson4D.quotientTreeLiftedWord_respectsPairing {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (q : ℤ) (a : ↥(PairingVertex κ) → Z4) : RespectsPairing κ (quotientTreeLiftedWord hm κ hfull q a)

theorem Anderson4D.quotientTreeLiftedWord_center {δ : ℝ} {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) (i : Fin m) : latticeTorusCenter δ (quotientTreeLiftedWord hm κ hfull q a i) = latticeTorusCenter δ (copiedPairingLabels κ hfull a i)

The quotient-tree word represents the same torus centres as the copied word before lifting.

noncomputable def Anderson4D.latticeWordChainWeightExcept {m : ℕ} (O : Finset (AdjacentIndex m)) (u : Fin m → Z4) : ℝ

Generic lattice chain product in which the edges in O are omitted.

Equations

• Anderson4D.latticeWordChainWeightExcept O u = ∏ j : Anderson4D.AdjacentIndex m, if j ∈ O then 1 else Anderson4D.latticeEdgeWeight (u ↑j) (u (Anderson4D.adjacentSucc j))

theorem Anderson4D.latticeWordChainWeightExcept_nonneg {m : ℕ} (O : Finset (AdjacentIndex m)) (u : Fin m → Z4) : 0 ≤ latticeWordChainWeightExcept O u

noncomputable def Anderson4D.periodicCopiedWordChainWeight {m : ℕ} (δ : ℝ) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) : ℝ

Periodic chain product on a copied-pair word.

Equations

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

theorem Anderson4D.periodicCellEdgeWeight_le_one {δ : ℝ} (hδ : 0 < δ) (x y : Z4) : periodicCellEdgeWeight δ x y ≤ 1

theorem Anderson4D.periodicCopiedEdge_eq_latticeLifted_of_mem_parentEdges {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) {j : AdjacentIndex m} (hj : j ∈ quotientParentWordEdges hm κ hfull) : periodicCellEdgeWeight δ (copiedPairingLabels κ hfull a ↑j) (copiedPairingLabels κ hfull a (adjacentSucc j)) = latticeEdgeWeight (quotientTreeLiftedWord hm κ hfull q a ↑j) (quotientTreeLiftedWord hm κ hfull q a (adjacentSucc j))

A selected parent edge has identical periodic and ordinary weights on the quotient-tree lift.

theorem Anderson4D.periodicCopiedWordChainWeight_le_quotientTreeLift {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) : periodicCopiedWordChainWeight δ κ hfull a ≤ latticeWordChainWeightExcept (quotientParentCycleEdges hm κ hfull) (quotientTreeLiftedWord hm κ hfull q a)

Periodic quotient-tree chain bridge.

The complete periodic copied chain is bounded by the ordinary lattice chain of a literal paired lift after skipping exactly the quotient cycle edges. There is no mesh-dependent multiplicative factor.

Uniform absorption of the canonical copied diameter

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

On the compatible mesh, the canonical torus-grid radius is no larger than the number of cells in one period.

theorem Anderson4D.primitiveCanonicalCellCarrier_abs_le_cellCount {ε : ℝ} (hε : 0 < ε) {n : ℕ} {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) (j : Fin (2 * n)) (i : Fin dim) : |y j i| ≤ compatibleCellCount ε

Coordinate bound for every label in the canonical copied carrier, expressed directly in terms of the period cell count.

theorem Anderson4D.znorm_sub_le_two_mul_int {q : ℤ} (hq : 0 < q) {x y : Z4} (hx : ∀ (i : Fin dim), |x i| ≤ q) (hy : ∀ (i : Fin dim), |y i| ≤ q) : znorm (x - y) ≤ 2 * ↑q

Sup-norm difference bound in an integer box whose half-width is a positive integer q.

theorem Anderson4D.primitiveCanonicalCellDiameter_le_cellCount {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : primitiveTupleDiameterBracketSq ⋯ y ≤ 1 + 4 * ↑(compatibleCellCount ε) ^ 2

The literal diameter of a tuple in the canonical copied carrier is quadratic in the period cell count, with no hidden box constant.

theorem Anderson4D.compatibleMesh_sq_mul_primitiveCopiedDiameter_le {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) {κ : PartialPairing (Fin (2 * n))} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : compatibleMeshSize ε ^ 2 * primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y) ≤ 20 * Real.pi ^ 2

Uniform diameter ledger. The cell-volume factor δ² absorbs the canonical copied diameter. The numerical constant is deliberately simple; most importantly, it is independent of both ε and the mesh cardinality.

The uniform primitive copied-weight bridge

theorem Anderson4D.listChainProduct_periodic_eq_terminal (δ : ℝ) (y e : Z4) (ys : List Z4) : listChainProduct (periodicCellEdgeWeight δ) (y :: (ys ++ [e])) = periodicTerminalPathWeight δ y e ys

List form of the periodic terminal path product.

theorem Anderson4D.periodicCopiedWordChainWeight_eq_terminal {δ : ℝ} {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) : periodicCopiedWordChainWeight δ κ hfull a = periodicTerminalPathWeight δ (primitiveFirstCell n hn (copiedPairingLabels κ hfull a)) (primitiveLastCell n hn (copiedPairingLabels κ hfull a)) (primitiveInternalCellLabels n hn (copiedPairingLabels κ hfull a))

The periodic word product is exactly the endpoint/internal-list product used by the copied-cell analytic estimate.

theorem Anderson4D.compatibleMesh_sq_mul_primitivePeriodicCopiedWeight_le_lift {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) (ha : copiedPairingLabels κ hfull a ∈ primitiveCanonicalCellCarrier ε n κ) : compatibleMeshSize ε ^ 2 * primitivePeriodicCopiedWeight ε n hn (copiedPairingLabels κ hfull a) ≤ 20 * Real.pi ^ 2 * latticeWordChainWeightExcept (quotientParentCycleEdges ⋯ κ hfull) (quotientTreeLiftedWord ⋯ κ hfull (compatibleCellCount ε) a)

Uniform pointwise estimate for a copied-pair label assignment. The mesh-volume factor δ² pays for the literal canonical diameter, while the quotient-tree lift leaves exactly n skipped word edges and no mesh-dependent multiplier.

theorem Anderson4D.compatibleMesh_sq_mul_primitivePeriodicCopiedWeight_le_quotientLift {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : compatibleMeshSize ε ^ 2 * primitivePeriodicCopiedWeight ε n hn y ≤ 20 * Real.pi ^ 2 * latticeWordChainWeightExcept (quotientParentCycleEdges ⋯ κ hfull) (quotientTreeLiftedWord ⋯ κ hfull (compatibleCellCount ε) (restrictToPairingLowerHalf κ ⟨y, ⋯⟩))

Carrier-facing form of the preceding theorem: any literal paired tuple is canonically restricted to one label per covariance pair before lifting.

Filtered sum and R-51 power ledgers

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

The exact quotient-lifted skipped-chain sum corresponding to a filtered periodic copied-cell sum. It retains the original canonical labels as the finite summation carrier, so this definition introduces neither a fiber multiplicity nor a carrier-cardinality factor.

Equations

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

theorem Anderson4D.primitivePeriodicQuotientLiftRealSum_nonneg (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : 0 ≤ primitivePeriodicQuotientLiftRealSum ε n hn κ hfull P

theorem Anderson4D.compatibleMesh_sq_mul_periodicFilteredRealSum_le_quotient {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : compatibleMeshSize ε ^ 2 * primitivePeriodicReductionFilteredRealSum ε n hn κ P ≤ 20 * Real.pi ^ 2 * primitivePeriodicQuotientLiftRealSum ε n hn κ hfull P

Sum-level quotient bridge with an arbitrary endpoint/support predicate. Its constant is uniform in the mesh and does not multiply by the cardinality of the canonical carrier.

theorem Anderson4D.compatibleMesh_pow_mul_periodicFilteredRealSum_le_quotient {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 2 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : compatibleMeshSize ε ^ (4 * n - 4) * primitivePeriodicReductionFilteredRealSum ε n ⋯ κ P ≤ 20 * Real.pi ^ 2 * compatibleMeshSize ε ^ (4 * n - 6) * primitivePeriodicQuotientLiftRealSum ε n ⋯ κ hfull P

The exact power shift required by the inserted R-51 cell estimate: δ² absorbs the copied diameter, leaving δ^(4n-6) and a universal constant. No quantity on the right grows with the compatible cell count.

theorem Anderson4D.compatibleMesh_pow_mul_periodicFilteredSum_le_quotient {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 2 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ENNReal.ofReal (compatibleMeshSize ε ^ (4 * n - 4)) * primitivePeriodicReductionFilteredSum ε n ⋯ κ P ≤ ENNReal.ofReal (20 * Real.pi ^ 2 * compatibleMeshSize ε ^ (4 * n - 6)) * ENNReal.ofReal (primitivePeriodicQuotientLiftRealSum ε n ⋯ κ hfull P)

Extended-real form of the uniform R-51 power ledger.

theorem Anderson4D.primitivePeriodicReductionFilteredSum_scalar_le_quotient {a b q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 2 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n ⋯ κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, ENNReal.ofReal q * (ENNReal.ofReal (a * compatibleMeshSize ε ^ (4 * n - 4) * primitivePeriodicReductionWeight ε n ⋯ u) + ENNReal.ofReal (b * compatibleMeshSize ε ^ (4 * n - 4) * primitivePeriodicReductionWeight ε n ⋯ u)) ≤ ENNReal.ofReal q * (ENNReal.ofReal a + ENNReal.ofReal b) * ENNReal.ofReal (20 * Real.pi ^ 2 * compatibleMeshSize ε ^ (4 * n - 6)) * ENNReal.ofReal (primitivePeriodicQuotientLiftRealSum ε n ⋯ κ hfull P)

Scalar-extracted form consumed by the endpoint cell estimate. The two nonnegative exhaustive-order coefficients are arbitrary; their common δ^(4n-4) factor is replaced by δ^(4n-6) and the universal quotient constant.

Direct endpoint-integral interface

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_periodicQuotientSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farBase := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R; have nearBase := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3); (∫⁻ (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) ≤ ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal farBase + ENNReal.ofReal nearBase) * ENNReal.ofReal (20 * Real.pi ^ 2 * δ ^ (4 * n - 6)) * ENNReal.ofReal (primitivePeriodicQuotientLiftRealSum ε n ⋯ κ ⋯ (primitiveCopiedEndpointSupported ρ ε n ⋯ z w))

Uniform R-51 quotient reduction.

This is the endpoint-fixed cell estimate with the false canonical pointwise comparison and the old carrier.card × windingBoxBase × windingBoxAmplification fallback removed. The only remaining finite sum is the literal quotient-tree lift with exactly n skipped edges.

Exact full-edge winding lift

The skipped-edge bridge above is useful as a topology ledger, but discarding all cycle factors is too coarse for the final critical scaling. The exact formula retains every cycle edge: relative to the quotient-tree lift, its right endpoint is translated by the nearest whole-period block.

noncomputable def Anderson4D.latticeWindingWordChainWeight {m : ℕ} (q : ℤ) (u : Fin m → Z4) : ℝ

An ordinary lattice chain in which every right endpoint is moved by the nearest period block relative to its left endpoint.

Equations

• Anderson4D.latticeWindingWordChainWeight q u = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.latticeEdgeWeight (u ↑j) (Anderson4D.nearestPeriodTranslate q (u ↑j) (u (Anderson4D.adjacentSucc j)))

theorem Anderson4D.latticeWindingWordChainWeight_nonneg {m : ℕ} (q : ℤ) (u : Fin m → Z4) : 0 ≤ latticeWindingWordChainWeight q u

theorem Anderson4D.periodicCellEdgeWeight_eq_lattice_nearestPeriodTranslate {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) (x y : Z4) : periodicCellEdgeWeight δ x y = latticeEdgeWeight x (nearestPeriodTranslate q x y)

A periodic edge is exactly the ordinary edge to the nearest centre-preserving period translate.

theorem Anderson4D.periodicCopiedWordChainWeight_eq_quotientWindingLift {δ : ℝ} (hδ : 0 < δ) {q : ℤ} (hq : PeriodCompatibleMesh δ q) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) : periodicCopiedWordChainWeight δ κ hfull a = latticeWindingWordChainWeight q (quotientTreeLiftedWord hm κ hfull q a)

Exact winding-chain identity. Unlike the skipped-edge inequality, this keeps all 2n-1 inverse-square factors and therefore preserves the critical R-51 power count.

theorem Anderson4D.primitivePeriodicCopiedWeight_copied_eq_quotientWindingLift {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (a : ↥(PairingVertex κ) → Z4) : primitivePeriodicCopiedWeight ε n hn (copiedPairingLabels κ hfull a) = primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn (copiedPairingLabels κ hfull a)) * latticeWindingWordChainWeight (compatibleCellCount ε) (quotientTreeLiftedWord ⋯ κ hfull (compatibleCellCount ε) a)

Exact full statistic for copied pair labels, with the literal diameter unchanged and every winding edge retained.

theorem Anderson4D.primitivePeriodicCopiedWeight_eq_quotientWindingLift {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalCellCarrier ε n κ) : primitivePeriodicCopiedWeight ε n hn y = primitiveTupleDiameterBracketSq ⋯ (primitiveCopiedReductionTuple n hn y) * latticeWindingWordChainWeight (compatibleCellCount ε) (quotientTreeLiftedWord ⋯ κ hfull (compatibleCellCount ε) fun (v : ↥(PairingVertex κ)) => y ↑v)

Carrier-facing exact winding identity.

Exact filtered winding sum

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

Full-edge winding version of the canonical filtered sum. In contrast to primitivePeriodicQuotientLiftRealSum, this retains both the diameter and every cycle factor.

Equations

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

theorem Anderson4D.primitivePeriodicQuotientWindingRealSum_nonneg (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : 0 ≤ primitivePeriodicQuotientWindingRealSum ε n hn κ hfull P

theorem Anderson4D.primitivePeriodicReductionFilteredRealSum_eq_quotientWinding {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredRealSum ε n hn κ P = primitivePeriodicQuotientWindingRealSum ε n hn κ hfull P

Lossless, arbitrary-filter periodic-to-winding reindexing.

theorem Anderson4D.primitivePeriodicReductionFilteredSum_eq_quotientWinding {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (κ : PartialPairing (Fin (2 * n))) (hfull : κ.IsFull) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : primitivePeriodicReductionFilteredSum ε n hn κ P = ENNReal.ofReal (primitivePeriodicQuotientWindingRealSum ε n hn κ hfull P)

Extended-real form of the exact winding reindexing.

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

Scalar extraction with the correct, unshifted δ^(4n-4) power.

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_periodicWindingSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farBase := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R; have nearBase := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3); (∫⁻ (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) ≤ ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal farBase + ENNReal.ofReal nearBase) * ENNReal.ofReal (δ ^ (4 * n - 4)) * ENNReal.ofReal (primitivePeriodicQuotientWindingRealSum ε n ⋯ κ ⋯ (primitiveCopiedEndpointSupported ρ ε n ⋯ z w))

Correct-scale endpoint R-51 reduction retaining all winding data.

def Anderson4D.r51CutRepresentative (q : ℕ) (c : Fin q) (x : ZMod q) : ℤ

Equations

• Anderson4D.r51CutRepresentative q c x = if x.val < ↑c then ↑x.val + ↑q else ↑x.val

theorem Anderson4D.r51CutRepresentative_ordered_sub {q : ℕ} [NeZero q] (c : Fin q) (x y : ZMod q) (hxy : x.val ≤ y.val) : |r51CutRepresentative q c x - r51CutRepresentative q c y| = if x.val < ↑c ∧ ↑c ≤ y.val then ↑q - (↑y.val - ↑x.val) else ↑y.val - ↑x.val

theorem Anderson4D.r51_card_ordered_separatingCuts {q : ℕ} [NeZero q] (x y : ZMod q) (_hxy : x.val ≤ y.val) : {c : Fin q | x.val < ↑c ∧ ↑c ≤ y.val}.card = y.val - x.val

def Anderson4D.r51ResidueGap {q : ℕ} (x y : ZMod q) : ℕ

Equations

• Anderson4D.r51ResidueGap x y = x.val.dist y.val

def Anderson4D.r51CyclicGap (q : ℕ) (x y : ZMod q) : ℕ

Equations

• Anderson4D.r51CyclicGap q x y = min (Anderson4D.r51ResidueGap x y) (q - Anderson4D.r51ResidueGap x y)

def Anderson4D.r51CutSeparates {q : ℕ} (c : Fin q) (x y : ZMod q) : Prop

Equations

• Anderson4D.r51CutSeparates c x y = (x.val < ↑c ∧ ↑c ≤ y.val ∨ y.val < ↑c ∧ ↑c ≤ x.val)

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidableR51CutSeparates {q : ℕ} (c : Fin q) (x y : ZMod q) : Decidable (r51CutSeparates c x y)

Equations

• Anderson4D.instDecidableR51CutSeparates c x y = Classical.propDecidable (Anderson4D.r51CutSeparates c x y)

theorem Anderson4D.r51CutRepresentative_sub_abs {q : ℕ} [NeZero q] (c : Fin q) (x y : ZMod q) : |r51CutRepresentative q c x - r51CutRepresentative q c y| = if r51CutSeparates c x y then ↑q - ↑(r51ResidueGap x y) else ↑(r51ResidueGap x y)

theorem Anderson4D.r51_card_separatingCuts {q : ℕ} [NeZero q] (x y : ZMod q) : {c : Fin q | r51CutSeparates c x y}.card = r51ResidueGap x y

def Anderson4D.r51CutIsLong {q : ℕ} (c : Fin q) (x y : ZMod q) : Prop

Equations

• Anderson4D.r51CutIsLong c x y = if Anderson4D.r51ResidueGap x y ≤ q - Anderson4D.r51ResidueGap x y then Anderson4D.r51CutSeparates c x y else ¬Anderson4D.r51CutSeparates c x y

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidableR51CutIsLong {q : ℕ} (c : Fin q) (x y : ZMod q) : Decidable (r51CutIsLong c x y)

Equations

• Anderson4D.instDecidableR51CutIsLong c x y = Classical.propDecidable (Anderson4D.r51CutIsLong c x y)

theorem Anderson4D.r51_card_longCuts {q : ℕ} [NeZero q] (x y : ZMod q) : {c : Fin q | r51CutIsLong c x y}.card = r51CyclicGap q x y

theorem Anderson4D.r51ResidueGap_lt {q : ℕ} [NeZero q] (x y : ZMod q) : r51ResidueGap x y < q

theorem Anderson4D.r51CyclicGap_mul_two_le {q : ℕ} [NeZero q] (x y : ZMod q) : 2 * r51CyclicGap q x y ≤ q

theorem Anderson4D.r51CyclicGap_eq_natAbs_valMinAbs {q : ℕ} [NeZero q] (x y : ZMod q) : r51CyclicGap q x y = (x - y).valMinAbs.natAbs

theorem Anderson4D.r51CutRepresentative_sub_abs_eq {q : ℕ} [NeZero q] (c : Fin q) (x y : ZMod q) : |r51CutRepresentative q c x - r51CutRepresentative q c y| = ↑(if r51CutIsLong c x y then q - r51CyclicGap q x y else r51CyclicGap q x y)

theorem Anderson4D.r51_log_long_ratio_average_le {q r : ℕ} (hq : 0 < q) (hr : 0 < r) (hrq : r ≤ q) : ↑r / ↑q * Real.log ((1 + ↑(q - r) ^ 2) / (1 + ↑r ^ 2)) ≤ 2

def Anderson4D.r51CyclicBracket (q : ℕ) (x y : ZMod q) : ℝ

Equations

• Anderson4D.r51CyclicBracket q x y = 1 + ↑(Anderson4D.r51CyclicGap q x y) ^ 2

def Anderson4D.r51CutBracket {q : ℕ} (c : Fin q) (x y : ZMod q) : ℝ

Equations

• Anderson4D.r51CutBracket c x y = 1 + ↑|Anderson4D.r51CutRepresentative q c x - Anderson4D.r51CutRepresentative q c y| ^ 2

def Anderson4D.r51LongBracket (q : ℕ) (x y : ZMod q) : ℝ

Equations

• Anderson4D.r51LongBracket q x y = 1 + ↑(q - Anderson4D.r51CyclicGap q x y) ^ 2

theorem Anderson4D.r51CyclicBracket_pos {q : ℕ} (x y : ZMod q) : 0 < r51CyclicBracket q x y

theorem Anderson4D.r51CutBracket_pos {q : ℕ} (c : Fin q) (x y : ZMod q) : 0 < r51CutBracket c x y

theorem Anderson4D.r51LongBracket_pos {q : ℕ} (x y : ZMod q) : 0 < r51LongBracket q x y

theorem Anderson4D.r51CutBracket_eq {q : ℕ} [NeZero q] (c : Fin q) (x y : ZMod q) : r51CutBracket c x y = if r51CutIsLong c x y then r51LongBracket q x y else r51CyclicBracket q x y

theorem Anderson4D.r51_log_cutBracket_div_cyclic {q : ℕ} [NeZero q] (c : Fin q) (x y : ZMod q) : Real.log (r51CutBracket c x y / r51CyclicBracket q x y) = if r51CutIsLong c x y then Real.log (r51LongBracket q x y / r51CyclicBracket q x y) else 0

theorem Anderson4D.r51_sum_log_cutBracket_div_cyclic {q : ℕ} [NeZero q] (x y : ZMod q) : ∑ c : Fin q, Real.log (r51CutBracket c x y / r51CyclicBracket q x y) = ↑(r51CyclicGap q x y) * Real.log (r51LongBracket q x y / r51CyclicBracket q x y)

theorem Anderson4D.r51_sum_log_cutBracket_div_cyclic_le {q : ℕ} [NeZero q] (x y : ZMod q) : ∑ c : Fin q, Real.log (r51CutBracket c x y / r51CyclicBracket q x y) ≤ 2 * ↑q

Four-dimensional cut lifts and canonical shortest lifts.

@[reducible, inline]

abbrev Anderson4D.R51Cut (q : ℕ) : Type

Equations

• Anderson4D.R51Cut q = (Fin 4 → Fin q)

def Anderson4D.r51CutLift (q : ℕ) (c : R51Cut q) (a : Z4) : Z4

Equations

• Anderson4D.r51CutLift q c a i = Anderson4D.r51CutRepresentative q (c i) ↑(a i)

def Anderson4D.r51MinimalDifference (q : ℕ) (a b : Z4) : Z4

Equations

• Anderson4D.r51MinimalDifference q a b i = (↑(a i - b i)).valMinAbs

def Anderson4D.r51MinimalTranslate (q : ℕ) (a b : Z4) : Z4

Equations

• Anderson4D.r51MinimalTranslate q a b = a - Anderson4D.r51MinimalDifference q a b

@[simp]

theorem Anderson4D.r51_sub_minimalTranslate (q : ℕ) (a b : Z4) : a - r51MinimalTranslate q a b = r51MinimalDifference q a b

theorem Anderson4D.r51MinimalTranslate_periodCongruent {q : ℕ} [NeZero q] (a b : Z4) : PeriodCongruent (↑q) (r51MinimalTranslate q a b) b

theorem Anderson4D.r51CutLift_periodCongruent {q : ℕ} [NeZero q] (c : R51Cut q) (a : Z4) : PeriodCongruent (↑q) (r51CutLift q c a) a

theorem Anderson4D.latticeTorusCenter_r51CutLift {δ : ℝ} {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (a : Z4) : latticeTorusCenter δ (r51CutLift q c a) = latticeTorusCenter δ a

theorem Anderson4D.latticeTorusCenter_r51MinimalTranslate {δ : ℝ} {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) (a b : Z4) : latticeTorusCenter δ (r51MinimalTranslate q a b) = latticeTorusCenter δ b

theorem Anderson4D.r51MinimalTranslate_edgeNoWrap {δ : ℝ} {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) (a b : Z4) : LatticeEdgeNoWrap δ a (r51MinimalTranslate q a b)

theorem Anderson4D.periodicCellEdgeWeight_eq_r51Minimal {δ : ℝ} (hδ : 0 < δ) {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) (a b : Z4) : periodicCellEdgeWeight δ a b = latticeEdgeWeight a (r51MinimalTranslate q a b)

theorem Anderson4D.r51MinimalDifference_coord_abs {q : ℕ} [NeZero q] (a b : Z4) (i : Fin 4) : |r51MinimalDifference q a b i| = ↑(r51CyclicGap q ↑(a i) ↑(b i))

theorem Anderson4D.r51CutLift_sub_coord_abs {q : ℕ} [NeZero q] (c : R51Cut q) (a b : Z4) (i : Fin 4) : |(r51CutLift q c a - r51CutLift q c b) i| = ↑(if r51CutIsLong (c i) ↑(a i) ↑(b i) then q - r51CyclicGap q ↑(a i) ↑(b i) else r51CyclicGap q ↑(a i) ↑(b i))

noncomputable def Anderson4D.r51CoordinateEdgeRatio {q : ℕ} (c : R51Cut q) (a b : Z4) (i : Fin 4) : ℝ

Equations

• Anderson4D.r51CoordinateEdgeRatio c a b i = Anderson4D.r51CutBracket (c i) ↑(a i) ↑(b i) / Anderson4D.r51CyclicBracket q ↑(a i) ↑(b i)

theorem Anderson4D.r51CoordinateEdgeRatio_pos {q : ℕ} (c : R51Cut q) (a b : Z4) (i : Fin 4) : 0 < r51CoordinateEdgeRatio c a b i

theorem Anderson4D.r51CoordinateEdgeRatio_one_le {q : ℕ} [NeZero q] (c : R51Cut q) (a b : Z4) (i : Fin 4) : 1 ≤ r51CoordinateEdgeRatio c a b i

theorem Anderson4D.r51CyclicBracket_eq_minimal_coord {q : ℕ} [NeZero q] (a b : Z4) (i : Fin 4) : r51CyclicBracket q ↑(a i) ↑(b i) = 1 + ↑(r51MinimalDifference q a b i) ^ 2

theorem Anderson4D.r51CutBracket_eq_cutLift_coord {q : ℕ} (c : R51Cut q) (a b : Z4) (i : Fin 4) : r51CutBracket (c i) ↑(a i) ↑(b i) = 1 + ↑((r51CutLift q c a - r51CutLift q c b) i) ^ 2

theorem Anderson4D.r51CyclicBracket_le_minimalBracket {q : ℕ} [NeZero q] (a b : Z4) (i : Fin 4) : r51CyclicBracket q ↑(a i) ↑(b i) ≤ latticeBracketSq a (r51MinimalTranslate q a b)

theorem Anderson4D.r51_latticeBracketSq_cutLift_le {q : ℕ} [NeZero q] (c : R51Cut q) (a b : Z4) : latticeBracketSq (r51CutLift q c a) (r51CutLift q c b) ≤ 4 * latticeBracketSq a (r51MinimalTranslate q a b) * ∏ i : Fin 4, r51CoordinateEdgeRatio c a b i

theorem Anderson4D.r51_vector_log_distortion_le {q : ℕ} [NeZero q] (c : R51Cut q) (a b : Z4) : Real.log (latticeBracketSq (r51CutLift q c a) (r51CutLift q c b) / latticeBracketSq a (r51MinimalTranslate q a b)) ≤ 4 + ∑ i : Fin 4, Real.log (r51CoordinateEdgeRatio c a b i)

theorem Anderson4D.r51_sum_coordinate_log_ratio_le {q : ℕ} [NeZero q] (a b : Z4) (i : Fin 4) : ∑ c : R51Cut q, Real.log (r51CoordinateEdgeRatio c a b i) ≤ 2 * ↑q ^ 4

theorem Anderson4D.r51_sum_vector_log_distortion_le {q : ℕ} [NeZero q] (a b : Z4) : ∑ c : R51Cut q, Real.log (latticeBracketSq (r51CutLift q c a) (r51CutLift q c b) / latticeBracketSq a (r51MinimalTranslate q a b)) ≤ 12 * ↑q ^ 4

The torus-correct diameter and whole-word statistics.

theorem Anderson4D.r51_minimalBracket_le_cutBracket {q : ℕ} [NeZero q] (c : R51Cut q) (a b : Z4) : latticeBracketSq a (r51MinimalTranslate q a b) ≤ latticeBracketSq (r51CutLift q c a) (r51CutLift q c b)

def Anderson4D.r51PeriodicTupleDiameterBracketSq {m : ℕ} (q : ℕ) (hm : 0 < m) (y : Fin m → Z4) : ℝ

Maximum shortest-lift lattice bracket. On a compatible mesh this is exactly 1 + δ⁻² times the squared torus diameter.

Equations

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

theorem Anderson4D.one_le_r51PeriodicTupleDiameterBracketSq {m q : ℕ} (hm : 0 < m) (y : Fin m → Z4) : 1 ≤ r51PeriodicTupleDiameterBracketSq q hm y

theorem Anderson4D.r51PeriodicTupleDiameterBracketSq_pos {m q : ℕ} (hm : 0 < m) (y : Fin m → Z4) : 0 < r51PeriodicTupleDiameterBracketSq q hm y

theorem Anderson4D.r51PeriodicTupleDiameterBracketSq_le_cutLift {m q : ℕ} [NeZero q] (hm : 0 < m) (c : R51Cut q) (y : Fin m → Z4) : r51PeriodicTupleDiameterBracketSq q hm y ≤ primitiveTupleDiameterBracketSq hm fun (i : Fin m) => r51CutLift q c (y i)

noncomputable def Anderson4D.r51PeriodicWordChainWeight {m : ℕ} (δ : ℝ) (y : Fin m → Z4) : ℝ

Equations

• Anderson4D.r51PeriodicWordChainWeight δ y = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.periodicCellEdgeWeight δ (y ↑j) (y (Anderson4D.adjacentSucc j))

noncomputable def Anderson4D.r51LatticeWordChainWeight {m : ℕ} (y : Fin m → Z4) : ℝ

Equations

• Anderson4D.r51LatticeWordChainWeight y = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.latticeEdgeWeight (y ↑j) (y (Anderson4D.adjacentSucc j))

noncomputable def Anderson4D.r51PeriodicReductionWeight {m : ℕ} (q : ℕ) (hm : 0 < m) (δ : ℝ) (y : Fin m → Z4) : ℝ

Equations

• Anderson4D.r51PeriodicReductionWeight q hm δ y = Anderson4D.r51PeriodicTupleDiameterBracketSq q hm y * Anderson4D.r51PeriodicWordChainWeight δ y

noncomputable def Anderson4D.r51LatticeReductionWeight {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) : ℝ

Equations

• Anderson4D.r51LatticeReductionWeight hm y = Anderson4D.primitiveTupleDiameterBracketSq hm y * Anderson4D.r51LatticeWordChainWeight y

theorem Anderson4D.r51PeriodicWordChainWeight_pos {m : ℕ} {δ : ℝ} (hδ : 0 < δ) (y : Fin m → Z4) : 0 < r51PeriodicWordChainWeight δ y

theorem Anderson4D.r51LatticeWordChainWeight_pos {m : ℕ} (y : Fin m → Z4) : 0 < r51LatticeWordChainWeight y

theorem Anderson4D.r51PeriodicReductionWeight_pos {m q : ℕ} (hm : 0 < m) {δ : ℝ} (hδ : 0 < δ) (y : Fin m → Z4) : 0 < r51PeriodicReductionWeight q hm δ y

theorem Anderson4D.r51LatticeReductionWeight_pos {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) : 0 < r51LatticeReductionWeight hm y

theorem Anderson4D.r51PeriodicWordChainWeight_div_cut_eq {m q : ℕ} [NeZero q] {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (y : Fin m → Z4) : (r51PeriodicWordChainWeight δ y / r51LatticeWordChainWeight fun (i : Fin m) => r51CutLift q c (y i)) = ∏ j : AdjacentIndex m, latticeBracketSq (r51CutLift q c (y ↑j)) (r51CutLift q c (y (adjacentSucc j))) / latticeBracketSq (y ↑j) (r51MinimalTranslate q (y ↑j) (y (adjacentSucc j)))

theorem Anderson4D.r51_log_periodicWordChain_div_cut_eq {m q : ℕ} [NeZero q] {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (y : Fin m → Z4) : Real.log (r51PeriodicWordChainWeight δ y / r51LatticeWordChainWeight fun (i : Fin m) => r51CutLift q c (y i)) = ∑ j : AdjacentIndex m, Real.log (latticeBracketSq (r51CutLift q c (y ↑j)) (r51CutLift q c (y (adjacentSucc j))) / latticeBracketSq (y ↑j) (r51MinimalTranslate q (y ↑j) (y (adjacentSucc j))))

theorem Anderson4D.r51_log_periodicReduction_div_cut_le {m q : ℕ} [NeZero q] (hm : 0 < m) {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (y : Fin m → Z4) : Real.log (r51PeriodicReductionWeight q hm δ y / r51LatticeReductionWeight hm fun (i : Fin m) => r51CutLift q c (y i)) ≤ ∑ j : AdjacentIndex m, Real.log (latticeBracketSq (r51CutLift q c (y ↑j)) (r51CutLift q c (y (adjacentSucc j))) / latticeBracketSq (y ↑j) (r51MinimalTranslate q (y ↑j) (y (adjacentSucc j))))

theorem Anderson4D.r51_sum_log_periodicReduction_div_cut_le {m q : ℕ} [NeZero q] (hm : 0 < m) {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (y : Fin m → Z4) : ∑ c : R51Cut q, Real.log (r51PeriodicReductionWeight q hm δ y / r51LatticeReductionWeight hm fun (i : Fin m) => r51CutLift q c (y i)) ≤ 12 * (↑m - 1) * ↑q ^ 4

Converting the logarithmic cut ledger into an arithmetic average.

theorem Anderson4D.r51_le_exp_mul_average_of_sum_log_div_le {ι : Type u_1} [Fintype ι] [Nonempty ι] {A K : ℝ} (hA : 0 < A) (B : ι → ℝ) (hB : ∀ (i : ι), 0 < B i) (hlog : ∑ i : ι, Real.log (A / B i) ≤ ↑(Fintype.card ι) * K) : A ≤ Real.exp K * ((∑ i : ι, B i) / ↑(Fintype.card ι))

theorem Anderson4D.r51PeriodicReductionWeight_le_cutAverage {m q : ℕ} [NeZero q] (hm : 0 < m) {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (y : Fin m → Z4) : r51PeriodicReductionWeight q hm δ y ≤ Real.exp (12 * (↑m - 1)) * ((∑ c : R51Cut q, r51LatticeReductionWeight hm fun (i : Fin m) => r51CutLift q c (y i)) / ↑q ^ 4)

Uniform finite fibers of a fixed cut lift

Inside the canonical box, two representatives of one residue differ by at most one period in either direction. The three-valued code below records which of the intervals [-q,0), [0,q), and {q} contains a coordinate. Together with its cut lift this code is injective. Consequently every tuple fiber has cardinality at most 3^(4m), uniformly in the mesh.

def Anderson4D.r51BoxCode (q : ℕ) (x : ℤ) : Fin 3

Equations

• Anderson4D.r51BoxCode q x = if x < 0 then 0 else if x < ↑q then 1 else 2

theorem Anderson4D.r51BoxCode_injective_of_dvd {q : ℕ} (hq : 0 < q) {x y : ℤ} (hx : |x| ≤ ↑q) (hy : |y| ≤ ↑q) (hdvd : ↑q ∣ x - y) (hcode : r51BoxCode q x = r51BoxCode q y) : x = y

@[simp]

theorem Anderson4D.r51CutLift_cast_zmod {q : ℕ} [NeZero q] (c : R51Cut q) (a : Z4) (i : Fin 4) : ↑(r51CutLift q c a i) = ↑(a i)

theorem Anderson4D.r51CutLift_code_injectiveOn_box {q m : ℕ} [NeZero q] (c : R51Cut q) : Set.InjOn (fun (y : Fin m → Z4) => (fun (j : Fin m) => r51CutLift q c (y j), fun (j : Fin m) (i : Fin dim) => r51BoxCode q (y j i))) {y : Fin m → Z4 | ∀ (j : Fin m) (i : Fin dim), |y j i| ≤ ↑q}

theorem Anderson4D.r51CutLift_fiber_card_le {q m : ℕ} [NeZero q] (c : R51Cut q) (s : Finset (Fin m → Z4)) (hbox : ∀ y ∈ s, ∀ (j : Fin m) (i : Fin dim), |y j i| ≤ ↑q) (u : Fin m → Z4) : {y ∈ s | (fun (j : Fin m) => r51CutLift q c (y j)) = u}.card ≤ (3 ^ 4) ^ m

theorem Anderson4D.r51_sum_cutLift_le_box_sum {q m : ℕ} [NeZero q] (c : R51Cut q) (s : Finset (Fin m → Z4)) (hbox : ∀ y ∈ s, ∀ (j : Fin m) (i : Fin dim), |y j i| ≤ ↑q) (B : Finset (Fin m → Z4)) (hmap : ∀ y ∈ s, (fun (j : Fin m) => r51CutLift q c (y j)) ∈ B) (F : (Fin m → Z4) → ℝ) (hF : ∀ (u : Fin m → Z4), 0 ≤ F u) : (∑ y ∈ s, F fun (j : Fin m) => r51CutLift q c (y j)) ≤ ↑((3 ^ 4) ^ m) * ∑ u ∈ B, F u

theorem Anderson4D.r51CutLift_coord_abs_le {q : ℕ} [NeZero q] (c : R51Cut q) (a : Z4) (i : Fin 4) : |r51CutLift q c a i| ≤ ↑(2 * q)

theorem Anderson4D.r51CutLift_tuple_mem_bounded {q m : ℕ} [NeZero q] (c : R51Cut q) (y : Fin m → Z4) : (fun (j : Fin m) => r51CutLift q c (y j)) ∈ rdec_boundedTuples (2 * q) m

theorem Anderson4D.r51CutLift_respectsPairing {q m : ℕ} [NeZero q] (c : R51Cut q) (κ : PartialPairing (Fin m)) (y : Fin m → Z4) (hy : RespectsPairing κ y) : RespectsPairing κ fun (j : Fin m) => r51CutLift q c (y j)

theorem Anderson4D.r51LatticeReductionWeight_eq_reductionWeight (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : r51LatticeReductionWeight ⋯ y = reductionWeight (2 * n - 1) (primitiveCopiedReductionTuple n hn y)

theorem Anderson4D.primitiveCopiedSourceTuple_injective (n : ℕ) (hn : 1 ≤ n) : Function.Injective (primitiveCopiedSourceTuple n hn)

theorem Anderson4D.r51_cutLift_cell_sum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) {n q : ℕ} (hn : 1 ≤ n) (hq : ↑q = compatibleCellCount ε) [NeZero q] {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (c : R51Cut q) : (∑ y ∈ primitiveCanonicalCellCarrier ε n κ, r51LatticeReductionWeight ⋯ fun (j : Fin (2 * n)) => r51CutLift q c (y j)) ≤ ↑((3 ^ 4) ^ (2 * n)) * primitiveAcrossLatticeSum (2 * q) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))

theorem Anderson4D.r51_periodic_cell_sum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) {n q : ℕ} (hn : 1 ≤ n) (hq : ↑q = compatibleCellCount ε) [NeZero q] {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : ∑ y ∈ primitiveCanonicalCellCarrier ε n κ, r51PeriodicReductionWeight q ⋯ (compatibleMeshSize ε) y ≤ Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * primitiveAcrossLatticeSum (2 * q) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ)))

The analytic insertion with the torus-correct diameter

The shortest-lift maximum controls the actual torus diameter of every compatible cell fiber. This is the point at which the valid Dper argument replaces the canonical-box diameter of the diagnostic routes above.

theorem Anderson4D.r51_minimalBracket_le_periodicTupleDiameter {m q : ℕ} (hm : 0 < m) (y : Fin m → Z4) (i j : Fin m) : latticeBracketSq (y i) (r51MinimalTranslate q (y i) (y j)) ≤ r51PeriodicTupleDiameterBracketSq q hm y

theorem Anderson4D.r51_torusTupleDiameterSq_le_periodicCellMaximum {m q : ℕ} [Nonempty (Fin m)] [NeZero q] (hm : 0 < m) {δ R : ℝ} (hδ : 0 < δ) (hR : 0 < R) (hq : PeriodCompatibleMesh δ ↑q) (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 + r51PeriodicTupleDiameterBracketSq q hm y)

theorem Anderson4D.r51_primitiveInsertedFactor_le_periodicCellMaximum {m q : ℕ} [Nonempty (Fin m)] [NeZero q] (hm : 0 < m) {ε R : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hR : 0 < R) (hq : PeriodCompatibleMesh (compatibleMeshSize ε) ↑q) (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 * r51PeriodicTupleDiameterBracketSq q hm y

theorem Anderson4D.exists_r51_primitiveInsertedIntegrand_copiedFiber_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 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (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 D := r51PeriodicTupleDiameterBracketSq q ⋯ y; 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 copied-fiber estimate with the shortest-lift periodic diameter. Its δ² factor is retained for the critical power ledger.

theorem Anderson4D.exists_r51_primitiveInsertedIntegrand_copiedFiber_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 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (z w : T4) (y : Fin (2 * n) → Z4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have D := r51PeriodicTupleDiameterBracketSq q ⋯ y; 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)

theorem Anderson4D.r51_primitiveCopiedCellMaximumTerminalLIntegral_exhaustive_order : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (q : ℕ) {ε : ℝ}, 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 D := r51PeriodicTupleDiameterBracketSq q ⋯ y; have W := periodicTerminalPathWeight δ (primitiveFirstCell n ⋯ y) (primitiveLastCell n ⋯ y) (primitiveInternalCellLabels 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)

theorem Anderson4D.r51_primitiveInsertedIntegrand_copiedFiber_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 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (z w : T4) (y : Fin (2 * n) → Z4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have D := r51PeriodicTupleDiameterBracketSq q ⋯ y; have W := periodicTerminalPathWeight δ (primitiveFirstCell n ⋯ y) (primitiveLastCell n ⋯ y) (primitiveInternalCellLabels 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))

theorem Anderson4D.r51PeriodicReductionWeight_eq_terminal (q : ℕ) (δ : ℝ) (n : ℕ) (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : r51PeriodicReductionWeight q ⋯ δ y = r51PeriodicTupleDiameterBracketSq q ⋯ y * periodicTerminalPathWeight δ (primitiveFirstCell n hn y) (primitiveLastCell n hn y) (primitiveInternalCellLabels n hn y)

theorem Anderson4D.r51_primitiveInsertedIntegrand_lintegral_le_periodicCopiedSum_filter (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (z w : T4) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [inst : DecidablePred P], (∀ y ∈ primitiveCanonicalCellCarrier ε n κ, ¬P (primitiveCopiedReductionTuple n ⋯ y) → primitiveCopiedFiberContribution ρ ε n ⋯ G κ z w y = 0) → have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (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) ≤ ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n ⋯ κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with P u, ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal (farCoeff * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n ⋯ u)) + ENNReal.ofReal (nearCoeff * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n ⋯ u)))

theorem Anderson4D.r51_primitiveInsertedIntegrand_lintegral_le_periodicEndpointSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (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) ≤ ∑ u ∈ Finset.filter (RespectsPairing (primitiveReductionPairing n ⋯ κ)) (rdec_boundedTuples (primitiveCopiedBoxRadius ε) (2 * n - 1 + 1)) with (primitiveCopiedEndpointSupported ρ ε n ⋯ z w) u, ENNReal.ofReal ((ε⁻¹ ^ dim * Ccov) ^ n) * (ENNReal.ofReal (farCoeff * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n ⋯ u)) + ENNReal.ofReal (nearCoeff * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n ⋯ u)))

Filtered periodic statistic and the P-5.10 interface

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

Equations

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

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

Equations

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

theorem Anderson4D.r51PeriodicReductionFilteredSum_eq_ofReal (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) {δ : ℝ} (hδ : 0 < δ) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : r51PeriodicReductionFilteredSum ε n hn q δ κ P = ENNReal.ofReal (r51PeriodicReductionFilteredRealSum ε n hn q δ κ P)

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

theorem Anderson4D.r51PeriodicReductionFilteredRealSum_le_full {ε : ℝ} (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) (δ : ℝ) (hδ : 0 < δ) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : r51PeriodicReductionFilteredRealSum ε n hn q δ κ P ≤ ∑ y ∈ primitiveCanonicalCellCarrier ε n κ, r51PeriodicReductionWeight q ⋯ δ y

theorem Anderson4D.r51PeriodicReductionFilteredSum_le_primitiveAcross {ε : ℝ} (hε : 0 < ε) {n q : ℕ} (hn : 1 ≤ n) (hq : ↑q = compatibleCellCount ε) [NeZero q] {κ : PartialPairing (Fin (2 * n))} (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : r51PeriodicReductionFilteredSum ε n hn q (compatibleMeshSize ε) κ P ≤ ENNReal.ofReal (Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * primitiveAcrossLatticeSum (2 * q) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n hn κ))))

theorem Anderson4D.r51PeriodicReductionFilteredSum_factor {a b Q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) (δ : ℝ) (κ : 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 * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n hn u)) + ENNReal.ofReal (b * r51PeriodicReductionWeight q ⋯ δ (primitiveCopiedSourceTuple n hn u))) = ENNReal.ofReal Q * (ENNReal.ofReal a + ENNReal.ofReal b) * r51PeriodicReductionFilteredSum ε n hn q δ κ P

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_periodicCutLatticeSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ κ ∈ primitiveFullPairings n, ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], ↑q = compatibleCellCount ε → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; have latticeBound := Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * primitiveAcrossLatticeSum (2 * q) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n ⋯ κ))); (∫⁻ (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) ≤ ENNReal.ofReal Q * (ENNReal.ofReal farCoeff + ENNReal.ofReal nearCoeff) * ENNReal.ofReal latticeBound

Terminal R-51 reduction for an explicit positive natural period count. The finite cut average and its uniform 3^(8n) fiber loss are absorbed into the displayed latticeBound; both analytic contributions retain the paper's critical factor δ^(4n-4).

theorem Anderson4D.primitiveInsertedIntegrand_lintegral_le_compatiblePeriodicCutLatticeSum (ρ : 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 q := (compatibleCellCount ε).toNat; have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; have latticeBound := Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * primitiveAcrossLatticeSum (2 * q) (2 * n - 1) (pairingLowerHalf (primitiveReductionPairing n ⋯ κ))); (∫⁻ (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) ≤ ENNReal.ofReal Q * (ENNReal.ofReal farCoeff + ENNReal.ofReal nearCoeff) * ENNReal.ofReal latticeBound

Canonical specialization of the terminal R-51 reduction. It chooses the natural-valued representative of compatibleCellCount ε, so callers do not need to provide the period count or its positivity instance.