IndisputableMonolith.Masses.GenerationTorsionBridge
IndisputableMonolith/Masses/GenerationTorsionBridge.lean · 445 lines · 43 declarations
show as:
view math explainer →
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