IndisputableMonolith.Masses.GenerationTorsionBridge

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Masses.BaselineDerivation
   5import IndisputableMonolith.Foundation.GroundStateDynamics
   6import IndisputableMonolith.Foundation.ParticleGenerations
   7import IndisputableMonolith.Foundation.WindingCharges
   8import IndisputableMonolith.RecogSpec.RSLedger
   9
  10/-!
  11# Generation Torsion Bridge — Geometric Source of Truth
  12
  13This module provides the single authoritative derivation of charged-generation
  14torsion {0, 11, 17} from Q₃ cube geometry, and proves it matches every
  15other representation in the codebase.
  16
  17## Derivation Chain
  18
  19The torsion schedule is defined entirely from D=3 cube combinatorics:
  20- Gen 1 (ground): τ₁ = 0 (no geometric coupling)
  21- Gen 2 (edge-dressed): τ₂ = E_passive(D) = cube_edges(D) − 1 = 11
  22- Gen 3 (face+edge-dressed): τ₃ = W_endo(D) = E_passive(D) + cube_faces(D) = 17
  23
  24The endogenous third-generation value `W_endo(3) = 11 + 6 = 17` numerically
  25coincides with the crystallographic wallpaper-group count (Fedorov, 1891).
  26That coincidence is proved by `BaselineDerivation.W_endo_at_D3` but is NOT
  27the primary source of the integer here; the primary route is
  28`E_passive + F`, which is forced by cube arithmetic alone.
  29
  30## What This Module Certifies
  31
  321. **No raw numerals**: `cubeGeometricTorsion` contains zero literal integers.
  332. **Agreement with Anchor.Integers.tau**: pointwise equality.
  343. **Agreement with RecogSpec.generationTorsion**: pointwise equality.
  354. **Forcing predicate**: an explicit structural predicate `CubeAdmissibleTorsion`
  36   whose unique solution is the canonical schedule.
  37
  38## Remaining Premise
  39
  40The predicate `CubeAdmissibleTorsion` encodes the physical assignment rule
  41(ground / passive-edge / face+edge modes). This rule is a structural
  42premise about how fermion generations couple to cube features, NOT a
  43consequence of the cost functional alone. Until that coupling is derived
  44from the RCL, this module upgrades the gap from "hardcoded numerals" to
  45"explicit structural premise with a uniqueness proof."
  46
  47See `ExcitationOrdering.lean` for a stronger route: the CW-filtration of
  48Q₃ derives the edge-before-face ordering from subcell dimension and proves
  49J-cost strict ordering on φ-power ratios.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Masses
  54namespace GenerationTorsionBridge
  55
  56open IndisputableMonolith.Constants.AlphaDerivation
  57open IndisputableMonolith.Masses.BaselineDerivation
  58open IndisputableMonolith.Foundation
  59open IndisputableMonolith.Foundation.VariationalDynamics
  60open IndisputableMonolith.RecogSpec
  61
  62/-! ## Part 1: The Geometric Torsion Schedule -/
  63
  64/-- Charged-generation torsion defined from Q₃ cube geometry alone.
  65    No raw numerals; every branch is a cube-combinatorial function of D. -/
  66def cubeGeometricTorsion : Generation → ℤ
  67  | .first  => 0
  68  | .second => (passive_field_edges D : ℤ)
  69  | .third  => (W_endo D : ℤ)
  70
  71@[simp] lemma cubeGeoTorsion_first : cubeGeometricTorsion .first = 0 := rfl
  72
  73@[simp] lemma cubeGeoTorsion_second : cubeGeometricTorsion .second = (passive_field_edges D : ℤ) := rfl
  74
  75@[simp] lemma cubeGeoTorsion_third : cubeGeometricTorsion .third = (W_endo D : ℤ) := rfl
  76
  77/-- Numeric verification: the geometric schedule evaluates to {0, 11, 17}. -/
  78theorem cubeGeoTorsion_values :
  79    cubeGeometricTorsion .first = 0 ∧
  80    cubeGeometricTorsion .second = 11 ∧
  81    cubeGeometricTorsion .third = 17 := by
  82  refine ⟨rfl, ?_, ?_⟩
  83  · simp [cubeGeometricTorsion, passive_field_edges, cube_edges, active_edges_per_tick, D]
  84  · simp [cubeGeometricTorsion, W_endo, passive_field_edges, cube_edges,
  85          active_edges_per_tick, cube_faces, D]
  86
  87/-! ## Part 2: Agreement with RecogSpec.generationTorsion -/
  88
  89/-- The geometric schedule equals the RecogSpec definition pointwise. -/
  90theorem cubeGeoTorsion_eq_generationTorsion :
  91    cubeGeometricTorsion = generationTorsion := by
  92  funext g
  93  cases g with
  94  | first => rfl
  95  | second =>
  96    simp [cubeGeometricTorsion, generationTorsion,
  97          passive_field_edges, cube_edges, active_edges_per_tick, D]
  98  | third =>
  99    simp [cubeGeometricTorsion, generationTorsion,
 100          W_endo, passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
 101
 102/-- Pointwise: second generation. -/
 103theorem cubeGeoTorsion_second_eq :
 104    cubeGeometricTorsion .second = generationTorsion .second := by
 105  simp [cubeGeometricTorsion, generationTorsion,
 106        passive_field_edges, cube_edges, active_edges_per_tick, D]
 107
 108/-- Pointwise: third generation. -/
 109theorem cubeGeoTorsion_third_eq :
 110    cubeGeometricTorsion .third = generationTorsion .third := by
 111  simp [cubeGeometricTorsion, generationTorsion,
 112        W_endo, passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
 113
 114/-! ## Part 3: Agreement with Masses.Integers.tau -/
 115
 116/-- The geometric schedule matches `Integers.tau` at generation index 0. -/
 117theorem cubeGeoTorsion_matches_tau_0 :
 118    cubeGeometricTorsion .first = Integers.tau 0 := by
 119  simp [cubeGeometricTorsion, Integers.tau]
 120
 121/-- The geometric schedule matches `Integers.tau` at generation index 1. -/
 122theorem cubeGeoTorsion_matches_tau_1 :
 123    cubeGeometricTorsion .second = Integers.tau 1 := by
 124  simp [cubeGeometricTorsion, Integers.tau, Anchor.E_passive]
 125
 126/-- The geometric schedule matches `Integers.tau` at generation index 2. -/
 127theorem cubeGeoTorsion_matches_tau_2 :
 128    cubeGeometricTorsion .third = Integers.tau 2 := by
 129  simp [cubeGeometricTorsion, Integers.tau, Anchor.W, W_endo,
 130        passive_field_edges, cube_edges, active_edges_per_tick,
 131        cube_faces, D, wallpaper_groups]
 132
 133/-! ## Part 4: Structural Provenance -/
 134
 135/-- The second-generation torsion is the passive edge count of Q₃. -/
 136theorem second_gen_is_passive_edges :
 137    cubeGeometricTorsion .second = ↑(cube_edges D - active_edges_per_tick) := by
 138  simp [cubeGeometricTorsion, passive_field_edges]
 139
 140/-- The third-generation torsion is E_passive + F (endogenous wallpaper route). -/
 141theorem third_gen_is_Epass_plus_F :
 142    cubeGeometricTorsion .third = ↑(passive_field_edges D + cube_faces D) := by
 143  simp [cubeGeometricTorsion, W_endo]
 144
 145/-- The endogenous wallpaper count coincides with the crystallographic constant. -/
 146theorem endogenous_matches_crystallographic :
 147    (W_endo D : ℤ) = (wallpaper_groups : ℤ) := by
 148  have := W_endo_at_D3
 149  exact_mod_cast this
 150
 151/-- The torsion step from gen 2 to gen 3 equals the face count of Q₃. -/
 152theorem gen3_minus_gen2_is_faces :
 153    cubeGeometricTorsion .third - cubeGeometricTorsion .second =
 154      (cube_faces D : ℤ) := by
 155  simp [cubeGeometricTorsion, W_endo]
 156
 157/-! ## Part 5: Cube-Admissible Torsion — Forcing Predicate -/
 158
 159/-- A torsion schedule is cube-admissible if it assigns:
 160    - Ground mode (gen 1): zero coupling → τ = 0
 161    - Edge mode (gen 2): passive-edge coupling → τ = E_passive
 162    - Face+edge mode (gen 3): passive-edge + face coupling → τ = E_passive + F
 163
 164    This is a STRUCTURAL PREMISE about how fermion generations couple to
 165    cube features. It is explicitly stated rather than buried in comments. -/
 166structure CubeAdmissibleTorsion (d : ℕ) (τ : Generation → ℤ) : Prop where
 167  ground_is_zero : τ .first = 0
 168  edge_mode : τ .second = (passive_field_edges d : ℤ)
 169  face_edge_mode : τ .third = (passive_field_edges d + cube_faces d : ℤ)
 170
 171/-- The geometric torsion schedule is cube-admissible at D=3. -/
 172theorem cubeGeoTorsion_admissible : CubeAdmissibleTorsion D cubeGeometricTorsion where
 173  ground_is_zero := rfl
 174  edge_mode := rfl
 175  face_edge_mode := by simp [cubeGeometricTorsion, W_endo]
 176
 177/-- `generationTorsion` is cube-admissible at D=3. -/
 178theorem generationTorsion_admissible : CubeAdmissibleTorsion D generationTorsion := by
 179  rw [← cubeGeoTorsion_eq_generationTorsion]
 180  exact cubeGeoTorsion_admissible
 181
 182/-- Any cube-admissible schedule at dimension d equals the geometric schedule at d. -/
 183theorem cubeAdmissible_unique (d : ℕ) (τ : Generation → ℤ)
 184    (h : CubeAdmissibleTorsion d τ) :
 185    τ = fun g => match g with
 186      | .first  => 0
 187      | .second => (passive_field_edges d : ℤ)
 188      | .third  => (passive_field_edges d + cube_faces d : ℤ) := by
 189  funext g
 190  cases g with
 191  | first => exact h.ground_is_zero
 192  | second => exact h.edge_mode
 193  | third => exact h.face_edge_mode
 194
 195/-- At D=3, any cube-admissible schedule equals the canonical `generationTorsion`. -/
 196theorem cubeAdmissible_forces_canonical (τ : Generation → ℤ)
 197    (h : CubeAdmissibleTorsion D τ) :
 198    τ = generationTorsion := by
 199  rw [← cubeGeoTorsion_eq_generationTorsion]
 200  funext g
 201  cases g with
 202  | first => exact h.ground_is_zero
 203  | second => exact h.edge_mode
 204  | third =>
 205    simp only [cubeGeometricTorsion, W_endo]
 206    exact h.face_edge_mode
 207
 208/-- Torsion ordering follows from cube arithmetic (no native_decide needed). -/
 209theorem cubeAdmissible_ordered (d : ℕ) (τ : Generation → ℤ) (hd : 2 ≤ d)
 210    (h : CubeAdmissibleTorsion d τ) :
 211    τ .first < τ .second ∧ τ .second < τ .third := by
 212  constructor
 213  · rw [h.ground_is_zero, h.edge_mode]
 214    have := (generation_ordering_general d hd).1
 215    exact_mod_cast this
 216  · rw [h.edge_mode, h.face_edge_mode]
 217    have : 0 < cube_faces d := by unfold cube_faces; omega
 218    linarith [show (0 : ℤ) < (cube_faces d : ℤ) from by exact_mod_cast this]
 219
 220/-! ## Part 6: Ground State from Variational Dynamics -/
 221
 222/-- The one-channel configuration whose ratio is `φ^n`. -/
 223noncomputable def phiRatioConfig (n : ℤ) : InitialCondition.Configuration 1 :=
 224  GroundStateDynamics.ratioConfig (IndisputableMonolith.Constants.phi ^ n)
 225    (zpow_pos IndisputableMonolith.Constants.phi_pos n)
 226
 227/-- If a φ-power ratio equals 1, its exponent is zero. -/
 228theorem phi_zpow_eq_one_iff (n : ℤ) :
 229    IndisputableMonolith.Constants.phi ^ n = 1 ↔ n = 0 := by
 230  constructor
 231  · intro h
 232    by_cases hn : n = 0
 233    · exact hn
 234    · rcases lt_or_gt_of_ne hn with hneg | hpos
 235      · have hlt : (1 : ℝ) < IndisputableMonolith.Constants.phi ^ (-n) := by
 236          exact one_lt_zpow₀ IndisputableMonolith.Constants.one_lt_phi (by omega)
 237        have hone : IndisputableMonolith.Constants.phi ^ (-n) = 1 := by
 238          calc
 239            IndisputableMonolith.Constants.phi ^ (-n)
 240                = 1 * IndisputableMonolith.Constants.phi ^ (-n) := by ring
 241            _ = IndisputableMonolith.Constants.phi ^ n * IndisputableMonolith.Constants.phi ^ (-n) := by
 242                  rw [h]
 243            _ = IndisputableMonolith.Constants.phi ^ (n + (-n)) := by
 244                  rw [zpow_add₀ IndisputableMonolith.Constants.phi_ne_zero]
 245            _ = 1 := by simp
 246        have hcontra : False := by
 247          rw [hone] at hlt
 248          exact (not_lt_of_ge (show (1 : ℝ) ≤ 1 by rfl)) hlt
 249        exact False.elim hcontra
 250      · have hlt : (1 : ℝ) < IndisputableMonolith.Constants.phi ^ n := by
 251          exact one_lt_zpow₀ IndisputableMonolith.Constants.one_lt_phi hpos
 252        have hcontra : False := by
 253          rw [h] at hlt
 254          exact (not_lt_of_ge (show (1 : ℝ) ≤ 1 by rfl)) hlt
 255        exact False.elim hcontra
 256  · intro hn
 257    simp [hn]
 258
 259/-- A torsion schedule is ground-state compatible if its first generation,
 260when realized as a one-channel φ-power ratio, is a neutral equilibrium of
 261the variational dynamics. -/
 262def GroundStateCompatibleTorsion (τ : Generation → ℤ) : Prop :=
 263  IsEquilibrium (phiRatioConfig (τ .first)) ∧
 264    log_charge (phiRatioConfig (τ .first)) = 0
 265
 266/-- Variational stability in the neutral sector forces the ground exponent to zero. -/
 267theorem groundStateCompatible_forces_ground_zero (τ : Generation → ℤ)
 268    (h : GroundStateCompatibleTorsion τ) :
 269    τ .first = 0 := by
 270  rcases h with ⟨hEq, hCharge⟩
 271  have hRatio :
 272      IndisputableMonolith.Constants.phi ^ (τ .first) = 1 :=
 273    GroundStateDynamics.stable_zero_charge_ratio_eq_one
 274      (IndisputableMonolith.Constants.phi ^ (τ .first))
 275      (zpow_pos IndisputableMonolith.Constants.phi_pos _)
 276      hEq hCharge
 277  exact (phi_zpow_eq_one_iff (τ .first)).mp hRatio
 278
 279/-! ## Part 7: Incremental Filtration and Slot Count -/
 280
 281/-- Increment-only version of cube admissibility.
 282
 283This removes the mode labels and keeps only the cumulative step data:
 284- ground state sits at zero torsion;
 285- the first jump adds the passive-edge count;
 286- the second jump adds the face count.
 287
 288This is a more algebraic statement of the same structural premise. -/
 289structure IncrementalCubeTorsion (d : ℕ) (τ : Generation → ℤ) : Prop where
 290  ground_is_zero : τ .first = 0
 291  edge_increment :
 292    τ .second - τ .first = (passive_field_edges d : ℤ)
 293  face_increment :
 294    τ .third - τ .second = (cube_faces d : ℤ)
 295
 296/-- Cube admissibility is equivalent to the incremental two-step filtration. -/
 297theorem cubeAdmissible_iff_incremental (d : ℕ) (τ : Generation → ℤ) :
 298    CubeAdmissibleTorsion d τ ↔ IncrementalCubeTorsion d τ := by
 299  constructor
 300  · intro h
 301    refine ⟨h.ground_is_zero, ?_, ?_⟩
 302    · rw [h.ground_is_zero, h.edge_mode]
 303      ring
 304    · rw [h.edge_mode, h.face_edge_mode]
 305      ring
 306  · intro h
 307    refine ⟨h.ground_is_zero, ?_, ?_⟩
 308    · simpa [h.ground_is_zero] using h.edge_increment
 309    · have hSecond : τ .second = (passive_field_edges d : ℤ) := by
 310        simpa [h.ground_is_zero] using h.edge_increment
 311      calc
 312        τ .third = (τ .third - τ .second) + τ .second := by ring
 313        _ = (cube_faces d : ℤ) + (passive_field_edges d : ℤ) := by
 314          rw [h.face_increment, hSecond]
 315        _ = (passive_field_edges d + cube_faces d : ℤ) := by ring
 316
 317/-- The canonical geometric torsion schedule also satisfies the incremental view. -/
 318theorem cubeGeoTorsion_incremental : IncrementalCubeTorsion D cubeGeometricTorsion := by
 319  exact (cubeAdmissible_iff_incremental D cubeGeometricTorsion).mp cubeGeoTorsion_admissible
 320
 321/-- `generationTorsion` satisfies the incremental cube filtration. -/
 322theorem generationTorsion_incremental : IncrementalCubeTorsion D generationTorsion := by
 323  exact (cubeAdmissible_iff_incremental D generationTorsion).mp generationTorsion_admissible
 324
 325/-- The incremental cube filtration is enough to force canonical torsion. -/
 326theorem incremental_forces_canonical (τ : Generation → ℤ)
 327    (h : IncrementalCubeTorsion D τ) :
 328    τ = generationTorsion := by
 329  exact cubeAdmissible_forces_canonical τ
 330    ((cubeAdmissible_iff_incremental D τ).mpr h)
 331
 332/-- Number of generation slots inherited from the D=3 cube face-pair count. -/
 333def generationSlotCount : ℕ := ParticleGenerations.face_pairs D
 334
 335/-- The cube contributes exactly three generation slots. -/
 336theorem generationSlotCount_eq_three : generationSlotCount = 3 := by
 337  simpa [generationSlotCount, D] using ParticleGenerations.face_pairs_at_D3
 338
 339/-- The generation slot count equals the number of independent Q₃ loops. -/
 340theorem generationSlotCount_eq_loopCount :
 341    generationSlotCount = WindingCharges.independent_loop_count 3 := by
 342  unfold generationSlotCount
 343  simpa [D] using WindingCharges.loops_eq_face_pairs_D3.symm
 344
 345/-- Pack the current strongest structural explanation of charged-generation torsion.
 346
 347At the present theorem surface, this is the sharpest honest statement:
 348- the cube contributes exactly three generation slots;
 349- those slots coincide with the three independent Q₃ loops / face-pairs;
 350- torsion accumulates by an edge increment followed by a face increment.
 351
 352What still remains open is deriving this filtration from the cost functional
 353rather than taking it as a geometric premise. -/
 354structure CubeGenerationFiltration (τ : Generation → ℤ) : Prop where
 355  slot_count : generationSlotCount = 3
 356  loop_facepair_unification :
 357    generationSlotCount = WindingCharges.independent_loop_count 3
 358  torsion_steps : IncrementalCubeTorsion D τ
 359
 360/-- The canonical schedule has the full cube-generation filtration package. -/
 361theorem generationTorsion_has_cube_filtration :
 362    CubeGenerationFiltration generationTorsion where
 363  slot_count := generationSlotCount_eq_three
 364  loop_facepair_unification := generationSlotCount_eq_loopCount
 365  torsion_steps := generationTorsion_incremental
 366
 367/-- Any torsion schedule with the cube-generation filtration is canonical. -/
 368theorem cubeFiltration_forces_canonical (τ : Generation → ℤ)
 369    (h : CubeGenerationFiltration τ) :
 370    τ = generationTorsion :=
 371  incremental_forces_canonical τ h.torsion_steps
 372
 373/-! ## Part 8: Minimal Loop Excitation Between Generations -/
 374
 375/-- Cumulative count of independent Q₃ loop-layers excited by each generation. -/
 376def canonicalLoopExcitation : Generation → ℕ
 377  | .first => 0
 378  | .second => 1
 379  | .third => 2
 380
 381/-- Minimal excitation profile: each later generation activates exactly one
 382new independent loop layer, and the third generation exhausts the available
 383three-loop budget of Q₃. -/
 384structure MinimalLoopExcitation (ℓ : Generation → ℕ) : Prop where
 385  ground_level : ℓ .first = 0
 386  second_adds_one : ℓ .second = ℓ .first + 1
 387  third_adds_one : ℓ .third = ℓ .second + 1
 388  exhausts_cube_loops : ℓ .third + 1 = WindingCharges.independent_loop_count 3
 389
 390/-- The canonical loop excitation profile satisfies the minimal-step theorem. -/
 391theorem canonicalLoopExcitation_minimal :
 392    MinimalLoopExcitation canonicalLoopExcitation where
 393  ground_level := rfl
 394  second_adds_one := rfl
 395  third_adds_one := rfl
 396  exhausts_cube_loops := by
 397    simp [canonicalLoopExcitation, WindingCharges.three_independent_loops_D3]
 398
 399/-- Minimal one-new-loop-per-generation-step excitation is unique. -/
 400theorem minimalLoopExcitation_unique (ℓ : Generation → ℕ)
 401    (h : MinimalLoopExcitation ℓ) :
 402    ℓ = canonicalLoopExcitation := by
 403  funext g
 404  cases g with
 405  | first =>
 406      exact h.ground_level
 407  | second =>
 408      calc
 409        ℓ .second = ℓ .first + 1 := h.second_adds_one
 410        _ = 0 + 1 := by rw [h.ground_level]
 411        _ = canonicalLoopExcitation .second := by simp [canonicalLoopExcitation]
 412  | third =>
 413      calc
 414        ℓ .third = ℓ .second + 1 := h.third_adds_one
 415        _ = (ℓ .first + 1) + 1 := by rw [h.second_adds_one]
 416        _ = (0 + 1) + 1 := by rw [h.ground_level]
 417        _ = canonicalLoopExcitation .third := by simp [canonicalLoopExcitation]
 418
 419/-- There is exactly one minimal loop-excitation profile on the three generations. -/
 420theorem one_new_independent_loop_per_generation_step :
 421    ∃! ℓ : Generation → ℕ, MinimalLoopExcitation ℓ := by
 422  refine ⟨canonicalLoopExcitation, canonicalLoopExcitation_minimal, ?_⟩
 423  intro ℓ hℓ
 424  exact minimalLoopExcitation_unique ℓ hℓ
 425
 426/-- The minimal loop-excitation profile matches the generation slot count. -/
 427theorem minimalLoopExcitation_matches_generation_slots (ℓ : Generation → ℕ)
 428    (h : MinimalLoopExcitation ℓ) :
 429    ℓ .third + 1 = generationSlotCount := by
 430  rw [h.exhausts_cube_loops, generationSlotCount_eq_loopCount.symm]
 431
 432/-! ## Part 9: Direct RSLedger Integration -/
 433
 434/-- An RSLedger whose torsion is cube-admissible at D=3 has canonical torsion.
 435    This replaces the bare hypothesis `L.torsion = generationTorsion` with
 436    a structural premise. -/
 437theorem rsLedger_torsion_from_cube (L : RSLedger)
 438    (h : CubeAdmissibleTorsion D L.torsion) :
 439    L.torsion = generationTorsion :=
 440  cubeAdmissible_forces_canonical L.torsion h
 441
 442end GenerationTorsionBridge
 443end Masses
 444end IndisputableMonolith
 445