IndisputableMonolith.Masses.ExcitationOrdering

   1import Mathlib
   2import IndisputableMonolith.Masses.GenerationTorsionBridge
   3
   4/-!
   5# Excitation Ordering from CW-Filtration of Q₃
   6
   7This module derives the edge-before-face excitation ordering for fermion
   8generation torsion from the CW-complex structure of the D=3 cube, combined
   9with J-cost monotonicity on φ-power ratios.
  10
  11## The Argument
  12
  13The 3-cube Q₃ has a natural CW-filtration by subcell dimension:
  14- 0-skeleton: 8 vertices (CW-dim 0)
  15- 1-skeleton: 12 edges, 11 passive (CW-dim 1)
  16- 2-skeleton: 6 faces (CW-dim 2)
  17
  18When generation excitations couple to subcells in order of CW dimension,
  19the cumulative torsion schedule {0, 11, 17} emerges:
  20- Gen 1 (ground): couples to 0-skeleton only → τ = 0
  21- Gen 2 (first excitation): adds 1-cells → τ = passive_field_edges = 11
  22- Gen 3 (second excitation): adds 2-cells → τ = 11 + cube_faces = 17
  23
  24The J-cost monotonicity on φ-power ratios then guarantees strict cost ordering:
  25  J(φ⁰) = 0 < J(φ¹¹) < J(φ¹⁷)
  26
  27## What This Proves
  28
  29IF excitations couple to Q₃ subcells in order of CW dimension, THEN:
  301. The first nontrivial excitation is edge-supported (dim 1)
  312. The next independent excitation is face-supported (dim 2)
  323. The resulting torsion schedule equals the canonical one
  334. J-cost respects this ordering strictly
  34
  35The CW-dimensional ordering (dim 1 < dim 2) is a geometric fact about the
  36cube. It provides the structural reason why edges come before faces, which
  37is otherwise an unexplained feature of `CubeAdmissibleTorsion`.
  38
  39## Remaining Premise
  40
  41The statement "excitations couple in order of CW dimension" is the filtration
  42principle. It replaces the mode labels (ground/edge/face) in
  43`CubeAdmissibleTorsion` with a single geometric principle, but it is still
  44a structural premise about the coupling mechanism rather than a consequence
  45of the RCL alone.
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Masses
  50namespace ExcitationOrdering
  51
  52open IndisputableMonolith.Constants
  53open IndisputableMonolith.Constants.AlphaDerivation
  54open IndisputableMonolith.Cost
  55open IndisputableMonolith.Masses.GenerationTorsionBridge
  56open IndisputableMonolith.RecogSpec
  57
  58/-! ## Part 1: CW-Complex Structure of Q_D -/
  59
  60/-- Subcell types of the D-dimensional hypercube Q_D, restricted to the
  61    dimensions relevant for fermion generation coupling (0, 1, 2). -/
  62inductive CubeCell (d : ℕ) where
  63  | vertex : CubeCell d
  64  | edge   : CubeCell d
  65  | face   : CubeCell d
  66  deriving DecidableEq
  67
  68/-- The CW dimension of a subcell type. -/
  69def CubeCell.cwDim {d : ℕ} : CubeCell d → ℕ
  70  | .vertex => 0
  71  | .edge   => 1
  72  | .face   => 2
  73
  74/-- Total subcell count of each type in Q_d. -/
  75def subcellCount (d : ℕ) : CubeCell d → ℕ
  76  | .vertex => cube_vertices d
  77  | .edge   => cube_edges d
  78  | .face   => cube_faces d
  79
  80@[simp] theorem subcellCount_vertex : subcellCount D .vertex = 8 := by native_decide
  81@[simp] theorem subcellCount_edge   : subcellCount D .edge   = 12 := by native_decide
  82@[simp] theorem subcellCount_face   : subcellCount D .face   = 6 := by native_decide
  83
  84/-- CW-dimensional ordering: edges are strictly lower-dimensional than faces. -/
  85theorem edge_dim_lt_face_dim :
  86    CubeCell.cwDim (.edge : CubeCell D) < CubeCell.cwDim (.face : CubeCell D) := by
  87  decide
  88
  89/-- Vertices are strictly lower-dimensional than edges. -/
  90theorem vertex_dim_lt_edge_dim :
  91    CubeCell.cwDim (.vertex : CubeCell D) < CubeCell.cwDim (.edge : CubeCell D) := by
  92  decide
  93
  94/-! ## Part 2: Passive Coupling Per CW Level -/
  95
  96/-- The number of subcells available for passive coupling at each CW level.
  97    Vertices do not contribute (ground state couples trivially).
  98    Edges contribute `cube_edges - 1` (one edge is the active transition).
  99    All faces participate. -/
 100def passiveCoupling (d : ℕ) : CubeCell d → ℕ
 101  | .vertex => 0
 102  | .edge   => passive_field_edges d
 103  | .face   => cube_faces d
 104
 105@[simp] theorem passiveCoupling_vertex : passiveCoupling D .vertex = 0 := rfl
 106@[simp] theorem passiveCoupling_edge   : passiveCoupling D .edge   = 11 := by native_decide
 107@[simp] theorem passiveCoupling_face   : passiveCoupling D .face   = 6 := by native_decide
 108
 109theorem passiveCoupling_edge_pos : 0 < passiveCoupling D .edge := by native_decide
 110theorem passiveCoupling_face_pos : 0 < passiveCoupling D .face := by native_decide
 111
 112/-! ## Part 3: CW-Cumulative Torsion -/
 113
 114/-- Torsion schedule derived from cumulative CW-filtration.
 115
 116    Generation g couples to all subcells of CW dimension ≤ (g - 1):
 117    - Gen 1 (ground): dim ≤ -1 → nothing → τ = 0
 118    - Gen 2: dim ≤ 0 already covered, new: dim 1 → adds edge coupling
 119    - Gen 3: dim ≤ 1 already covered, new: dim 2 → adds face coupling -/
 120def cwCumulativeTorsion (d : ℕ) : Generation → ℤ
 121  | .first  => 0
 122  | .second => (passiveCoupling d .edge : ℤ)
 123  | .third  => (passiveCoupling d .edge + passiveCoupling d .face : ℤ)
 124
 125@[simp] theorem cwTorsion_first  : cwCumulativeTorsion D .first  = 0 := rfl
 126@[simp] theorem cwTorsion_second : cwCumulativeTorsion D .second = 11 := by native_decide
 127@[simp] theorem cwTorsion_third  : cwCumulativeTorsion D .third  = 17 := by native_decide
 128
 129/-- CW-cumulative torsion at D=3 equals the canonical `generationTorsion`. -/
 130theorem cwTorsion_eq_generationTorsion :
 131    cwCumulativeTorsion D = generationTorsion := by
 132  funext g
 133  cases g with
 134  | first => rfl
 135  | second =>
 136    simp [cwCumulativeTorsion, generationTorsion, passiveCoupling,
 137          passive_field_edges, cube_edges, active_edges_per_tick, D]
 138  | third =>
 139    simp [cwCumulativeTorsion, generationTorsion, passiveCoupling,
 140          passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
 141
 142/-- The first excitation increment equals the passive edge count. -/
 143theorem first_increment_is_passive_edges :
 144    cwCumulativeTorsion D .second - cwCumulativeTorsion D .first =
 145      (passive_field_edges D : ℤ) := by
 146  simp [cwCumulativeTorsion, passiveCoupling]
 147
 148/-- The second excitation increment equals the face count. -/
 149theorem second_increment_is_faces :
 150    cwCumulativeTorsion D .third - cwCumulativeTorsion D .second =
 151      (cube_faces D : ℤ) := by
 152  simp [cwCumulativeTorsion, passiveCoupling,
 153        passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
 154
 155/-- The CW-cumulative torsion is cube-admissible. -/
 156theorem cwTorsion_cubeAdmissible :
 157    CubeAdmissibleTorsion D (cwCumulativeTorsion D) := by
 158  rw [cwTorsion_eq_generationTorsion]
 159  exact generationTorsion_admissible
 160
 161/-! ## Part 4: J-Cost Monotonicity on [1, ∞) -/
 162
 163/-- J-cost is strictly increasing on [1, ∞).
 164
 165    Proof: write `J(x) = (x + 1/x)/2 - 1` and show `x + 1/x` is strictly
 166    increasing for `x ≥ 1` via the identity
 167      `(y + 1/y) - (x + 1/x) = (y - x)(xy - 1)/(xy)`,
 168    which is positive when `1 ≤ x < y`. -/
 169theorem Jcost_strict_mono_pos {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
 170    (hx1 : 1 ≤ x) (hxy : x < y) :
 171    Jcost x < Jcost y := by
 172  have hx0 : x ≠ 0 := ne_of_gt hx
 173  have hy0 : y ≠ 0 := ne_of_gt hy
 174  simp only [Jcost]
 175  suffices h : x + x⁻¹ < y + y⁻¹ by linarith
 176  have hxy_pos : 0 < x * y := mul_pos hx hy
 177  have hyx : 0 < y - x := sub_pos.mpr hxy
 178  have hxy1 : 0 < x * y - 1 := by nlinarith
 179  have key : y + y⁻¹ - (x + x⁻¹) = (y - x) * (x * y - 1) / (x * y) := by
 180    field_simp
 181    ring
 182  linarith [div_pos (mul_pos hyx hxy1) hxy_pos]
 183
 184/-! ## Part 5: Excitation Cost and Ordering -/
 185
 186/-- Excitation cost: the J-cost of the φ-power ratio at integer torsion τ. -/
 187noncomputable def excitationCost (τ : ℤ) : ℝ := Jcost (phi ^ τ)
 188
 189/-- Ground state (τ = 0) has zero excitation cost. -/
 190theorem excitationCost_ground : excitationCost 0 = 0 := by
 191  simp [excitationCost, Jcost_unit0]
 192
 193/-- Any nonzero torsion has positive excitation cost. -/
 194theorem excitationCost_pos_of_ne_zero (τ : ℤ) (hτ : τ ≠ 0) :
 195    0 < excitationCost τ := by
 196  apply Jcost_pos_of_ne_one
 197  · exact zpow_pos phi_pos τ
 198  · exact fun h => hτ ((phi_zpow_eq_one_iff τ).mp h)
 199
 200/-- Excitation cost is strictly monotone for non-negative torsion:
 201    0 ≤ τ₁ < τ₂ implies J(φ^τ₁) < J(φ^τ₂). -/
 202theorem excitationCost_strictMono {τ₁ τ₂ : ℤ} (h1 : 0 ≤ τ₁) (h2 : τ₁ < τ₂) :
 203    excitationCost τ₁ < excitationCost τ₂ := by
 204  apply Jcost_strict_mono_pos (zpow_pos phi_pos τ₁) (zpow_pos phi_pos τ₂)
 205  · rcases eq_or_lt_of_le h1 with rfl | hpos
 206    · simp
 207    · exact le_of_lt (one_lt_zpow₀ one_lt_phi hpos)
 208  · exact zpow_lt_zpow_right₀ one_lt_phi h2
 209
 210/-- The three generation torsion values have strictly ordered J-costs. -/
 211theorem excitation_cost_ordering :
 212    excitationCost 0 = 0 ∧
 213    0 < excitationCost 11 ∧
 214    excitationCost 11 < excitationCost 17 :=
 215  ⟨excitationCost_ground,
 216   excitationCost_pos_of_ne_zero 11 (by omega),
 217   excitationCost_strictMono (by omega) (by omega)⟩
 218
 219/-! ## Part 6: The Excitation Ordering Theorem -/
 220
 221/-- **The Excitation Ordering Theorem for Q₃.**
 222
 223    Among neutral-to-excited admissible ledger transitions on Q₃:
 224
 225    1. **Edge-before-face (dimensional)**: The first nontrivial excitation is
 226       edge-supported (CW dimension 1), and the next independent excitation
 227       is face-supported (CW dimension 2).
 228
 229    2. **Cost ordering**: J-cost respects the CW filtration strictly —
 230       ground costs zero, edge excitation costs less than face+edge.
 231
 232    3. **Increment provenance**: The first increment equals the passive edge
 233       count and the second equals the face count of Q₃.
 234
 235    4. **Canonical forcing**: The CW-cumulative schedule matches `generationTorsion`.
 236
 237    This derives the `E_passive` / `cube_faces` increments from the CW
 238    structure of Q₃ combined with J-cost monotonicity, rather than taking
 239    them as unexplained mode labels. -/
 240structure ExcitationOrderingTheorem : Prop where
 241  edge_lower_dim_than_face :
 242    CubeCell.cwDim (.edge : CubeCell D) < CubeCell.cwDim (.face : CubeCell D)
 243  cw_torsion_is_canonical :
 244    cwCumulativeTorsion D = generationTorsion
 245  ground_zero_cost :
 246    excitationCost (cwCumulativeTorsion D .first) = 0
 247  edge_cheaper_than_face_edge :
 248    excitationCost (cwCumulativeTorsion D .second) <
 249      excitationCost (cwCumulativeTorsion D .third)
 250  first_increment_is_edges :
 251    cwCumulativeTorsion D .second - cwCumulativeTorsion D .first =
 252      (passive_field_edges D : ℤ)
 253  second_increment_is_faces :
 254    cwCumulativeTorsion D .third - cwCumulativeTorsion D .second =
 255      (cube_faces D : ℤ)
 256
 257/-- The excitation ordering theorem holds for Q₃. -/
 258theorem excitation_ordering_holds : ExcitationOrderingTheorem where
 259  edge_lower_dim_than_face := edge_dim_lt_face_dim
 260  cw_torsion_is_canonical := cwTorsion_eq_generationTorsion
 261  ground_zero_cost := by simp [cwCumulativeTorsion, excitationCost, Jcost_unit0]
 262  edge_cheaper_than_face_edge := by
 263    show excitationCost (cwCumulativeTorsion D .second) <
 264      excitationCost (cwCumulativeTorsion D .third)
 265    simp only [cwTorsion_second, cwTorsion_third]
 266    exact excitationCost_strictMono (by omega) (by omega)
 267  first_increment_is_edges := first_increment_is_passive_edges
 268  second_increment_is_faces := second_increment_is_faces
 269
 270/-! ## Part 7: Variational Selection — Edge Is Minimal Nontrivial Excitation -/
 271
 272/-- Among all subcell types with nonzero passive coupling, edges have the
 273    smallest CW dimension. The variational principle (selecting cheapest
 274    excitation) therefore selects edge modes first. -/
 275theorem edge_is_minimal_nontrivial_excitation :
 276    ∀ (cell : CubeCell D),
 277    0 < passiveCoupling D cell →
 278    CubeCell.cwDim (.edge : CubeCell D) ≤ CubeCell.cwDim cell := by
 279  intro cell hpos
 280  cases cell with
 281  | vertex => simp [passiveCoupling] at hpos
 282  | edge => exact le_refl _
 283  | face => exact Nat.le_of_lt edge_dim_lt_face_dim
 284
 285/-- The CW-ordering is *dimensional*, not numerical: face coupling (6) is
 286    numerically smaller than edge coupling (11), but edges come first because
 287    dim(edge) = 1 < dim(face) = 2.
 288
 289    This makes explicit that generation ordering cannot be explained by
 290    "smallest torsion increment first" — it requires the geometric notion
 291    of subcell dimension. -/
 292theorem ordering_is_dimensional_not_numerical :
 293    (cube_faces D : ℤ) < (passive_field_edges D : ℤ) ∧
 294    CubeCell.cwDim (.edge : CubeCell D) < CubeCell.cwDim (.face : CubeCell D) := by
 295  constructor
 296  · simp [cube_faces, passive_field_edges, cube_edges, active_edges_per_tick, D]
 297  · exact edge_dim_lt_face_dim
 298
 299/-! ## Part 8: Connection to Existing Filtration -/
 300
 301/-- The CW torsion satisfies the incremental cube filtration. -/
 302theorem cwTorsion_incremental :
 303    IncrementalCubeTorsion D (cwCumulativeTorsion D) := by
 304  rw [cwTorsion_eq_generationTorsion]
 305  exact generationTorsion_incremental
 306
 307/-- The CW torsion satisfies the full cube-generation filtration package. -/
 308theorem cwTorsion_has_filtration :
 309    CubeGenerationFiltration (cwCumulativeTorsion D) := by
 310  rw [cwTorsion_eq_generationTorsion]
 311  exact generationTorsion_has_cube_filtration
 312
 313/-- From `ExcitationOrderingTheorem` we recover `CubeGenerationFiltration`. -/
 314theorem excitation_ordering_implies_filtration
 315    (h : ExcitationOrderingTheorem) :
 316    CubeGenerationFiltration generationTorsion := by
 317  rw [← h.cw_torsion_is_canonical]
 318  exact cwTorsion_has_filtration
 319
 320/-! ## Part 9: Excitation Ordering Certificate -/
 321
 322/-- Full certificate summarizing the CW-filtration route to generation torsion.
 323
 324    **Proved**:
 325    - CW-dimensional ordering: dim(edge) < dim(face)
 326    - CW-cumulative torsion matches canonical schedule
 327    - J-cost strict ordering: ground < edge < face+edge
 328    - First increment = passive edges of Q₃
 329    - Second increment = faces of Q₃
 330    - Edge modes are the minimal nontrivial excitation (by CW dimension)
 331    - Ordering is dimensional (not numerical): 6 < 11 but edges come first
 332    - CW route recovers the full CubeGenerationFiltration package
 333
 334    **Structural premise**: Excitations couple in order of CW dimension.
 335    This is a geometric principle about the cube rather than a mode label,
 336    but it is not yet derived from the cost functional. -/
 337theorem excitation_ordering_certificate :
 338    ExcitationOrderingTheorem ∧
 339    CubeGenerationFiltration generationTorsion ∧
 340    (∀ (cell : CubeCell D), 0 < passiveCoupling D cell →
 341      CubeCell.cwDim (.edge : CubeCell D) ≤ CubeCell.cwDim cell) ∧
 342    ((cube_faces D : ℤ) < (passive_field_edges D : ℤ)) :=
 343  ⟨excitation_ordering_holds,
 344   excitation_ordering_implies_filtration excitation_ordering_holds,
 345   edge_is_minimal_nontrivial_excitation,
 346   ordering_is_dimensional_not_numerical.1⟩
 347
 348end ExcitationOrdering
 349end Masses
 350end IndisputableMonolith
 351