IndisputableMonolith.Gravity.SevenGaps.Gap2FreudenthalPeriodDoubling4D

   1import IndisputableMonolith.Geometry.PeriodicFreudenthalTorus4D
   2import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   3
   4/-!
   5# Gap 2 / 4D carrier track: period-doubling on the Freudenthal 4-torus
   6
   7The 4D mirror of `Gap2FreudenthalPeriodDoubling` (3D), built on the typed
   84D carrier of `Geometry/PeriodicFreudenthalTorus4D`. It supplies the
   9level-to-level maps the 4D `MetricRefinementFamily` will need at the typed
  10skeleton:
  11
  12* the mod-`N` vertex projection `periodDoublingVertexMap4D` from the
  13  side-`(2*N)` 4-torus to the side-`N` 4-torus, intertwining the periodic
  14  bit-translations of the Kuhn skeleton;
  15* the class-copying edge projection `periodDoublingEdgeMap4D` (keeps the
  16  `Fin 15` displacement class), with endpoint commutation;
  17* simpliciality of the projection on Kuhn 4-simplices: the image of every
  18  fine Kuhn simplex is the coarse Kuhn simplex of the same index at the
  19  projected cell, with five distinct vertices when `1 < N`;
  20* the coarse-to-fine section `liftEdgeDoubled4D` and the section theorem
  21  `liftEdge4D_is_section`, proved by cases via four `reduceMod_of_lt`
  22  facts, mirroring the 3D proof structure;
  23* the bridge theorems verifying that the fifteen classes of this carrier
  24  are bit-for-bit the fifteen classes of `ReggeEdgeStencil4D`, and that the
  25  squared lengths agree (`dispWeight4` is `classWeightNat`).
  26
  27Scope and honesty boundary (same discipline as the 3D module):
  28* THEOREM: every named result below, on the typed periodic skeleton.
  29  Class-copy is class-label bookkeeping on the skeleton, not a
  30  `MetricDecoration.sqEdge` pullback; Config-level coarsen, decoration
  31  pullback, and action step control are the next worker's 4D-instance job.
  32* This module does not touch `BoundedComplex` and does not assemble a
  33  `MetricRefinementFamily`.
  34
  35Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Gravity
  40namespace SevenGaps
  41namespace Gap2FreudenthalPeriodDoubling4D
  42
  43open Geometry.PeriodicFreudenthalTorus4D
  44open Analysis.ReggeEdgeStencil4D
  45
  46noncomputable section
  47
  48/-! ## §1. Side-doubling vertex projection -/
  49
  50instance instNeZero_two_mul (N : ℕ) [NeZero N] : NeZero (2 * N) :=
  51  ⟨Nat.mul_ne_zero (by decide : (2 : ℕ) ≠ 0) (NeZero.ne N)⟩
  52
  53/-- Coordinatewise reduction `Fin (2*N) → Fin N`. -/
  54def reduceMod (N : ℕ) [NeZero N] (i : Fin (2 * N)) : Fin N :=
  55  ⟨i.val % N, Nat.mod_lt _ (Nat.pos_of_neZero N)⟩
  56
  57theorem reduceMod_val (N : ℕ) [NeZero N] (i : Fin (2 * N)) :
  58    (reduceMod N i).val = i.val % N :=
  59  rfl
  60
  61/-- Reduction mod `N` intertwines the one-step periodic bit translation. -/
  62theorem reduceMod_addBit (N : ℕ) [NeZero N] (i : Fin (2 * N)) (b : Bool) :
  63    reduceMod N (addBit i b) = addBit (reduceMod N i) b := by
  64  ext
  65  change ((i.val + bit b) % (2 * N)) % N = (i.val % N + bit b) % N
  66  have hdiv : N ∣ 2 * N := ⟨2, by ring⟩
  67  have hmod2 : ((i.val + bit b) % (2 * N)) % N = (i.val + bit b) % N :=
  68    Nat.mod_mod_of_dvd _ hdiv
  69  have hsplit : (i.val + bit b) % N = (i.val % N + bit b) % N := by
  70    simp [Nat.add_mod]
  71  rw [hmod2, hsplit]
  72
  73/-- Reduction below the modulus is the identity embedding. -/
  74theorem reduceMod_of_lt (N : ℕ) [NeZero N] (i : Fin (2 * N)) (hi : i.val < N) :
  75    reduceMod N i = ⟨i.val, hi⟩ := by
  76  ext
  77  exact Nat.mod_eq_of_lt hi
  78
  79/-- The mod-`N` vertex projection from the side-`(2*N)` periodic 4-grid to
  80the side-`N` periodic 4-grid. -/
  81def periodDoublingVertexMap4D (N : ℕ) [NeZero N] :
  82    Vertex4 (2 * N) → Vertex4 N :=
  83  fun v =>
  84    (reduceMod N v.1, reduceMod N v.2.1, reduceMod N v.2.2.1,
  85      reduceMod N v.2.2.2)
  86
  87/-- The vertex projection intertwines four-axis bit translations. -/
  88theorem periodDoublingVertexMap4D_addBits4 (N : ℕ) [NeZero N]
  89    (v : Vertex4 (2 * N)) (dx dy dz dw : Bool) :
  90    periodDoublingVertexMap4D N (addBits4 v dx dy dz dw) =
  91      addBits4 (periodDoublingVertexMap4D N v) dx dy dz dw := by
  92  simp [periodDoublingVertexMap4D, addBits4, reduceMod_addBit]
  93
  94/-- The vertex projection intertwines the local 4-cube corner translations
  95used by every Kuhn 4-simplex. -/
  96theorem periodDoublingVertexMap4D_addVertexBits4 (N : ℕ) [NeZero N]
  97    (v : Vertex4 (2 * N)) (a : Fin 16) :
  98    periodDoublingVertexMap4D N (addVertexBits4 v a) =
  99      addVertexBits4 (periodDoublingVertexMap4D N v) a := by
 100  simp [addVertexBits4, periodDoublingVertexMap4D_addBits4]
 101
 102/-- **Headline (vertex map).** The mod-`N` map is a well-defined map on
 103periodic 4-vertices intertwining the periodic identifications encoded by
 104`addBits4` and `addVertexBits4`. -/
 105theorem freudenthal4D_period_doubling_vertex_map (N : ℕ) [NeZero N]
 106    (v : Vertex4 (2 * N)) (dx dy dz dw : Bool) (a : Fin 16) :
 107    periodDoublingVertexMap4D N (addBits4 v dx dy dz dw) =
 108        addBits4 (periodDoublingVertexMap4D N v) dx dy dz dw ∧
 109      periodDoublingVertexMap4D N (addVertexBits4 v a) =
 110        addVertexBits4 (periodDoublingVertexMap4D N v) a :=
 111  ⟨periodDoublingVertexMap4D_addBits4 N v dx dy dz dw,
 112    periodDoublingVertexMap4D_addVertexBits4 N v a⟩
 113
 114/-! ## §2. Edge projection and the class-copy property -/
 115
 116/-- Edge projection: send the fine base vertex through the vertex map and
 117keep the positive displacement class. -/
 118def periodDoublingEdgeMap4D (N : ℕ) [NeZero N] :
 119    PeriodicEdge4 (2 * N) → PeriodicEdge4 N :=
 120  fun e => { base := periodDoublingVertexMap4D N e.base, disp := e.disp }
 121
 122/-- Endpoints of a fine 4-edge project to the endpoints of its image. -/
 123theorem periodDoublingEdgeMap4D_endpoints (N : ℕ) [NeZero N]
 124    (e : PeriodicEdge4 (2 * N)) :
 125    (periodDoublingEdgeMap4D N e).endpoints =
 126      (periodDoublingVertexMap4D N e.endpoints.1,
 127        periodDoublingVertexMap4D N e.endpoints.2) := by
 128  cases e with
 129  | mk base disp =>
 130      let d := dispBits4 disp
 131      have h := periodDoublingVertexMap4D_addBits4 N base d.1 d.2.1 d.2.2.1 d.2.2.2
 132      simp only [periodDoublingEdgeMap4D, PeriodicEdge4.endpoints, d] at h ⊢
 133      exact Prod.ext rfl h.symm
 134
 135/-- Squared displacement of the image equals that of the fine edge, because
 136the displacement class is preserved. -/
 137theorem periodDoublingEdgeMap4D_dispSq_eq (N : ℕ) [NeZero N]
 138    (e : PeriodicEdge4 (2 * N)) :
 139    periodicDispSqEdge4 (periodDoublingEdgeMap4D N e).disp =
 140      periodicDispSqEdge4 e.disp := by
 141  rfl
 142
 143/-- **Headline (class copy).** The edge projection keeps the displacement
 144class, so the squared lattice displacement of the image is definitionally
 145equal to that of the fine edge, and the endpoints commute with the
 146projection. This is class-label bookkeeping on the typed skeleton (the
 147carrier-level analog of the 3D `decoration_pullback_class_copy`); the
 148Config-level decoration pullback is the 4D instance's job. -/
 149theorem freudenthal4D_period_doubling_edge_control (N : ℕ) [NeZero N]
 150    (e : PeriodicEdge4 (2 * N)) :
 151    periodicDispSqEdge4 (periodDoublingEdgeMap4D N e).disp ≤
 152      periodicDispSqEdge4 e.disp ∧
 153      (periodDoublingEdgeMap4D N e).endpoints =
 154        (periodDoublingVertexMap4D N e.endpoints.1,
 155          periodDoublingVertexMap4D N e.endpoints.2) :=
 156  ⟨le_of_eq (periodDoublingEdgeMap4D_dispSq_eq N e),
 157    periodDoublingEdgeMap4D_endpoints N e⟩
 158
 159/-! ## §3. Simpliciality of the projection on Kuhn 4-simplices -/
 160
 161/-- Vertex set of a periodic Kuhn 4-simplex. -/
 162def kuhnVertexSet {N : ℕ} [NeZero N] (cell : Vertex4 N) (σ : Fin 24) :
 163    Finset (Vertex4 N) :=
 164  Finset.univ.image fun k : Fin 5 => addVertexBits4 cell (kuhnVerts σ k)
 165
 166theorem kuhnVertexSet_card (N : ℕ) [NeZero N] (hN : 1 < N)
 167    (cell : Vertex4 N) (σ : Fin 24) :
 168    (kuhnVertexSet cell σ).card = 5 := by
 169  unfold kuhnVertexSet
 170  have hf : Function.Injective (fun k : Fin 5 => addVertexBits4 cell (kuhnVerts σ k)) :=
 171    kuhn_corners_injective N hN cell σ
 172  rw [Finset.card_image_of_injective _ hf]
 173  simp
 174
 175/-- **Headline (simplicial map).** The mod-`N` projection is simplicial on
 176the Kuhn skeleton: the image of every fine Kuhn 4-simplex is the coarse
 177Kuhn 4-simplex of the same local index at the projected cell, as an
 178equality of vertex sets. When `1 < N` the image has five distinct
 179vertices. -/
 180theorem freudenthal4D_period_doubling_simplicial_map (N : ℕ) [NeZero N]
 181    (hN : 1 < N) (cell : Vertex4 (2 * N)) (σ : Fin 24) :
 182    (kuhnVertexSet cell σ).image (periodDoublingVertexMap4D N) =
 183        kuhnVertexSet (periodDoublingVertexMap4D N cell) σ ∧
 184      (kuhnVertexSet (periodDoublingVertexMap4D N cell) σ).card = 5 := by
 185  constructor
 186  · ext v
 187    constructor
 188    · intro hv
 189      rcases Finset.mem_image.mp hv with ⟨w, hw, rfl⟩
 190      rcases Finset.mem_image.mp hw with ⟨k, _, rfl⟩
 191      refine Finset.mem_image.mpr ⟨k, Finset.mem_univ k, ?_⟩
 192      exact (periodDoublingVertexMap4D_addVertexBits4 N cell (kuhnVerts σ k)).symm
 193    · intro hv
 194      rcases Finset.mem_image.mp hv with ⟨k, _, rfl⟩
 195      refine Finset.mem_image.mpr
 196        ⟨addVertexBits4 cell (kuhnVerts σ k), ?_, ?_⟩
 197      · exact Finset.mem_image.mpr ⟨k, Finset.mem_univ k, rfl⟩
 198      · exact periodDoublingVertexMap4D_addVertexBits4 N cell (kuhnVerts σ k)
 199  · exact kuhnVertexSet_card N hN (periodDoublingVertexMap4D N cell) σ
 200
 201/-- Explicit coarse 4-simplex witnessing simpliciality. Holds at every `N`;
 202nondegeneracy of the coarse simplex is `kuhnVertexSet_card` (`1 < N`). -/
 203theorem freudenthal4D_period_doubling_simplicial_witness (N : ℕ) [NeZero N]
 204    (cell : Vertex4 (2 * N)) (σ : Fin 24) :
 205    ∃ τ : PeriodicSimplex4 N,
 206      ∀ k : Fin 5,
 207        periodDoublingVertexMap4D N (addVertexBits4 cell (kuhnVerts σ k)) =
 208          addVertexBits4 τ.1 (kuhnVerts τ.2 k) :=
 209  ⟨(periodDoublingVertexMap4D N cell, σ), fun k =>
 210    periodDoublingVertexMap4D_addVertexBits4 N cell (kuhnVerts σ k)⟩
 211
 212/-! ## §4. The coarse-to-fine section -/
 213
 214/-- Embed a coarse coordinate into the doubled side by value. -/
 215def embedDouble (N : ℕ) [NeZero N] (i : Fin N) : Fin (2 * N) :=
 216  ⟨i.val, by
 217    have hi := i.isLt
 218    have hN : 0 < N := Nat.pos_of_neZero N
 219    omega⟩
 220
 221/-- Canonical edge section: same displacement class, base embedded into the
 222doubled lattice by value. -/
 223def liftEdgeDoubled4D (N : ℕ) [NeZero N] (e : PeriodicEdge4 N) :
 224    PeriodicEdge4 (2 * N) where
 225  base :=
 226    (embedDouble N e.base.1, embedDouble N e.base.2.1,
 227      embedDouble N e.base.2.2.1, embedDouble N e.base.2.2.2)
 228  disp := e.disp
 229
 230theorem liftEdgeDoubled4D_disp (N : ℕ) [NeZero N] (e : PeriodicEdge4 N) :
 231    (liftEdgeDoubled4D N e).disp = e.disp := rfl
 232
 233/-- **MAJOR headline (section).** `liftEdgeDoubled4D` is a section of the
 234period-doubling edge projection: project the lift, recover the edge. Proved
 235by cases through four `reduceMod_of_lt` facts, mirroring the 3D
 236`liftEdge_is_section`. -/
 237theorem liftEdge4D_is_section (N : ℕ) [NeZero N] (e : PeriodicEdge4 N) :
 238    periodDoublingEdgeMap4D N (liftEdgeDoubled4D N e) = e := by
 239  cases e with
 240  | mk base disp =>
 241    cases base with
 242    | mk x yzw =>
 243      cases yzw with
 244      | mk y zw =>
 245        cases zw with
 246        | mk z w =>
 247          have hx : x.val < N := x.isLt
 248          have hy : y.val < N := y.isLt
 249          have hz : z.val < N := z.isLt
 250          have hw : w.val < N := w.isLt
 251          have hx2 : x.val < 2 * N := by
 252            have := Nat.pos_of_neZero N; omega
 253          have hy2 : y.val < 2 * N := by
 254            have := Nat.pos_of_neZero N; omega
 255          have hz2 : z.val < 2 * N := by
 256            have := Nat.pos_of_neZero N; omega
 257          have hw2 : w.val < 2 * N := by
 258            have := Nat.pos_of_neZero N; omega
 259          simp only [liftEdgeDoubled4D, periodDoublingEdgeMap4D,
 260            periodDoublingVertexMap4D, embedDouble]
 261          refine congrArg (fun b => PeriodicEdge4.mk b disp) ?_
 262          refine Prod.ext ?_ (Prod.ext ?_ (Prod.ext ?_ ?_))
 263          · exact reduceMod_of_lt N ⟨x.val, hx2⟩ hx
 264          · exact reduceMod_of_lt N ⟨y.val, hy2⟩ hy
 265          · exact reduceMod_of_lt N ⟨z.val, hz2⟩ hz
 266          · exact reduceMod_of_lt N ⟨w.val, hw2⟩ hw
 267
 268/-- The section is injective (distinct coarse edges lift to distinct fine
 269edges). -/
 270theorem liftEdgeDoubled4D_injective (N : ℕ) [NeZero N] :
 271    Function.Injective (liftEdgeDoubled4D N) := by
 272  intro a b h
 273  have ha := liftEdge4D_is_section N a
 274  have hb := liftEdge4D_is_section N b
 275  rw [h] at ha
 276  exact ha.symm.trans hb
 277
 278/-- **Class copy through the section.** The round trip through the
 279projection keeps the displacement class exactly; the squared lattice
 280displacement agrees on the nose. -/
 281theorem periodDoubling4D_class_copy (N : ℕ) [NeZero N] (e : PeriodicEdge4 N) :
 282    (periodDoublingEdgeMap4D N (liftEdgeDoubled4D N e)).disp = e.disp ∧
 283      periodicDispSqEdge4
 284          (periodDoublingEdgeMap4D N (liftEdgeDoubled4D N e)).disp =
 285        periodicDispSqEdge4 e.disp := by
 286  rw [liftEdge4D_is_section]
 287  exact ⟨rfl, rfl⟩
 288
 289/-! ## §5. Bridge to the Regge 4D stencil (the count verification) -/
 290
 291/-- **Bridge (class enumeration verified).** The fifteen displacement
 292classes of this carrier are bit-for-bit the fifteen classes of
 293`ReggeEdgeStencil4D`: coordinate `i` of class `d` is bit `i` of the mask
 294`d.val + 1` on both sides. -/
 295theorem dispBits4_eq_classBit (d : Fin 15) :
 296    dispBits4 d =
 297      (classBit d 0, classBit d 1, classBit d 2, classBit d 3) := by
 298  fin_cases d <;> decide
 299
 300/-- The Hamming weights agree class-by-class with the stencil. -/
 301theorem dispWeight4_eq_classWeightNat (d : Fin 15) :
 302    dispWeight4 d = classWeightNat d := by
 303  fin_cases d <;> decide
 304
 305/-- The carrier's squared class lengths are the stencil's squared class
 306lengths (`classDispSq`), hence sit on the recognition ladder by
 307`Gap1ClassLengths.classLength_in_recognition_ladder` (proved in
 308`Gap1ClassLengthsFromRecognitionCost`). -/
 309theorem periodicDispSqEdge4_eq_classDispSq (d : Fin 15) :
 310    periodicDispSqEdge4 d = classDispSq d := by
 311  rw [classDispSq_eq_weight]
 312  unfold periodicDispSqEdge4
 313  exact_mod_cast dispWeight4_eq_classWeightNat d
 314
 315/-! ## §6. Package (real Props from the headline theorems) -/
 316
 317/-- The headline facts assembled as a single Prop, under the side-length
 318hypothesis `1 < N` required for non-collapse of simplex images. Each
 319conjunct other than the side-length hypothesis is proved by a named theorem
 320of this module. -/
 321def freudenthal4D_period_doubling_package (N : ℕ) [NeZero N] : Prop :=
 322  1 < N ∧
 323    (∀ (v : Vertex4 (2 * N)) (dx dy dz dw : Bool) (a : Fin 16),
 324        periodDoublingVertexMap4D N (addBits4 v dx dy dz dw) =
 325            addBits4 (periodDoublingVertexMap4D N v) dx dy dz dw ∧
 326          periodDoublingVertexMap4D N (addVertexBits4 v a) =
 327            addVertexBits4 (periodDoublingVertexMap4D N v) a) ∧
 328      (∀ (cell : Vertex4 (2 * N)) (σ : Fin 24),
 329        (kuhnVertexSet cell σ).image (periodDoublingVertexMap4D N) =
 330            kuhnVertexSet (periodDoublingVertexMap4D N cell) σ ∧
 331          (kuhnVertexSet (periodDoublingVertexMap4D N cell) σ).card = 5) ∧
 332      (∀ e : PeriodicEdge4 (2 * N),
 333        periodicDispSqEdge4 (periodDoublingEdgeMap4D N e).disp ≤
 334            periodicDispSqEdge4 e.disp ∧
 335          (periodDoublingEdgeMap4D N e).endpoints =
 336            (periodDoublingVertexMap4D N e.endpoints.1,
 337              periodDoublingVertexMap4D N e.endpoints.2))
 338
 339theorem freudenthal4D_period_doubling_package_holds (N : ℕ) [NeZero N]
 340    (hN : 1 < N) : freudenthal4D_period_doubling_package N :=
 341  ⟨hN,
 342    fun v dx dy dz dw a => freudenthal4D_period_doubling_vertex_map N v dx dy dz dw a,
 343    fun cell σ => freudenthal4D_period_doubling_simplicial_map N hN cell σ,
 344    fun e => freudenthal4D_period_doubling_edge_control N e⟩
 345
 346#print axioms liftEdge4D_is_section
 347#print axioms freudenthal4D_period_doubling_edge_control
 348#print axioms freudenthal4D_period_doubling_simplicial_map
 349#print axioms freudenthal4D_period_doubling_vertex_map
 350#print axioms periodDoubling4D_class_copy
 351#print axioms dispBits4_eq_classBit
 352#print axioms periodicDispSqEdge4_eq_classDispSq
 353#print axioms freudenthal4D_period_doubling_package_holds
 354
 355end
 356
 357end Gap2FreudenthalPeriodDoubling4D
 358end SevenGaps
 359end Gravity
 360end IndisputableMonolith
 361