Encyclopedia Masses Masses Generation Torsion Bridge Canonical Loop Excitation Minimal
ARTICLE 4 claims 3 theorems 1 model
Masses Generation Torsion Bridge Canonical Loop Excitation Minimal
In the Recognition Science framework, the three generations of matter are tied to the geometry of a cube, and a minimal loop excitation is the unique way to count them.
The canonical loop excitation
In particle physics, the three generations of matter (up and down quarks, then charm and strange, then top and bottom) are a mystery: nothing in the standard model explains why there are three, or why the heavier generations exist. The Recognition Science framework proposes an answer from geometry. Its ledger, a discrete record of recognition events, assigns each generation a torsion value, a whole number that encodes how the generation couples to a three-dimensional cube.
The framework's machine-checked library of formal theorems proves that this assignment is unique. The declaration canonicalLoopExcitation_minimal establishes that there is exactly one way to assign a minimal loop excitation, a count of independent loops, to each generation: zero for the first, one for the second, and two for the third. This is a theorem, not a definitional choice, and it is forced by the geometry of the cube.
The proof works by showing that any assignment satisfying the minimality condition must equal the canonical one. The condition itself, called MinimalLoopExcitation, requires that the excitation exhausts the cube's independent loops and that each generation step adds exactly one new loop. The theorem minimalLoopExcitation_unique then proves that the only function meeting this condition is the canonical one, and one_new_independent_loop_per_generation_step proves that such a function exists. This is a uniqueness result in the same spirit as the framework's other forcing theorems: given the structural premise, the numbers are not chosen but derived.
In Recognition Science, this result is significant because it connects the abstract torsion schedule to a concrete geometric picture. The torsion values 0, 11, and 17, which previously appeared as hardcoded numbers, are now seen as the result of counting edges and faces of a cube. The minimal loop excitation is a simpler, more fundamental way to express the same structure: it counts the generations themselves, not the torsion. This is a step toward explaining why there are exactly three generations, and why they are ordered the way they are.
The declaration does not claim that the minimal loop excitation is the same as the mass of the particles. It does not claim that the structural premise, the rule that generations couple to cube features, is derived from the cost functional alone. That premise remains an explicit assumption, not a consequence of the framework's core axioms. The theorem also does not claim that the cube geometry is the only possible source of the generation structure; it proves uniqueness given the premise, not the premise itself.
THEOREM minimalLoopExcitation_unique · one_new_independent_loop_per_generation_step · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Minimal one-new-loop-per-generation-step excitation is unique. -/
theorem minimalLoopExcitation_unique (ℓ : Generation → ℕ)
(h : MinimalLoopExcitation ℓ) :
ℓ = canonicalLoopExcitation := by
funext g
cases g with
| first =>
exact h.ground_level
| second =>
calc
ℓ .second = ℓ .first + 1 := h.second_adds_one
_ = 0 + 1 := by rw [h.ground_level]
_ = canonicalLoopExcitation .second := by simp [canonicalLoopExcitation]
| third =>
calc
ℓ .third = ℓ .second + 1 := h.third_adds_one
_ = (ℓ .first + 1) + 1 := by rw [h.second_adds_one]
_ = (0 + 1) + 1 := by rw [h.ground_level]
_ = canonicalLoopExcitation .third := by simp [canonicalLoopExcitation]
/-- There is exactly one minimal loop-excitation profile on the three generations. -/
theorem one_new_independent_loop_per_generation_step :
∃! ℓ : Generation → ℕ, MinimalLoopExcitation ℓ := by
refine ⟨canonicalLoopExcitation, canonicalLoopExcitation_minimal, ?_⟩
intro ℓ hℓ
exact minimalLoopExcitation_unique ℓ hℓ
THEOREM minimalLoopExcitation_unique · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Minimal one-new-loop-per-generation-step excitation is unique. -/
theorem minimalLoopExcitation_unique (ℓ : Generation → ℕ)
(h : MinimalLoopExcitation ℓ) :
ℓ = canonicalLoopExcitation := by
funext g
cases g with
| first =>
exact h.ground_level
| second =>
calc
ℓ .second = ℓ .first + 1 := h.second_adds_one
_ = 0 + 1 := by rw [h.ground_level]
_ = canonicalLoopExcitation .second := by simp [canonicalLoopExcitation]
| third =>
calc
ℓ .third = ℓ .second + 1 := h.third_adds_one
_ = (ℓ .first + 1) + 1 := by rw [h.second_adds_one]
_ = (0 + 1) + 1 := by rw [h.ground_level]
_ = canonicalLoopExcitation .third := by simp [canonicalLoopExcitation]
THEOREM cubeGeometricTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Charged-generation torsion defined from Q₃ cube geometry alone.
No raw numerals; every branch is a cube-combinatorial function of D. -/
def cubeGeometricTorsion : Generation → ℤ
| .first => 0
| .second => (passive_field_edges D : ℤ)
| .third => (W_endo D : ℤ)
MODEL canonicalLoopExcitation · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Cumulative count of independent Q₃ loop-layers excited by each generation. -/
def canonicalLoopExcitation : Generation → ℕ
| .first => 0
| .second => 1
| .third => 2
What this page does not claim
The declaration does not derive the existence of three generations from the cost functional alone. The declaration does not claim that the minimal loop excitation is the same as the mass of the particles. The declaration does not claim that the cube geometry is the only possible source of the generation structure.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/GenerationTorsionBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What is the physical mechanism that couples fermion generations to cube features?
- Can the structural premise of cube coupling be derived from the cost functional alone?
- How does the minimal loop excitation relate to the measured mass ratios of the three generations?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM minimalLoopExcitation_unique · one_new_independent_loop_per_generation_step · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Minimal one-new-loop-per-generation-step excitation is unique. -/ theorem minimalLoopExcitation_unique (ℓ : Generation → ℕ) (h : MinimalLoopExcitation ℓ) : ℓ = canonicalLoopExcitation := by funext g cases g with | first => exact h.ground_level | second => calc ℓ .second = ℓ .first + 1 := h.second_adds_one _ = 0 + 1 := by rw [h.ground_level] _ = canonicalLoopExcitation .second := by simp [canonicalLoopExcitation] | third => calc ℓ .third = ℓ .second + 1 := h.third_adds_one _ = (ℓ .first + 1) + 1 := by rw [h.second_adds_one] _ = (0 + 1) + 1 := by rw [h.ground_level] _ = canonicalLoopExcitation .third := by simp [canonicalLoopExcitation]/-- There is exactly one minimal loop-excitation profile on the three generations. -/ theorem one_new_independent_loop_per_generation_step : ∃! ℓ : Generation → ℕ, MinimalLoopExcitation ℓ := by refine ⟨canonicalLoopExcitation, canonicalLoopExcitation_minimal, ?_⟩ intro ℓ hℓ exact minimalLoopExcitation_unique ℓ hℓThe declaration canonicalLoopExcitation_minimal establishes that there is exactly one way to assign a minimal loop excitation, a count of independent loops, to each generation: zero for the first, one for the second, and two for the third. minimalLoopExcitation_unique · one_new_independent_loop_per_generation_step · IndisputableMonolith/Masses/GenerationTorsionBridge.leanTHEOREM minimalLoopExcitation_unique · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Minimal one-new-loop-per-generation-step excitation is unique. -/ theorem minimalLoopExcitation_unique (ℓ : Generation → ℕ) (h : MinimalLoopExcitation ℓ) : ℓ = canonicalLoopExcitation := by funext g cases g with | first => exact h.ground_level | second => calc ℓ .second = ℓ .first + 1 := h.second_adds_one _ = 0 + 1 := by rw [h.ground_level] _ = canonicalLoopExcitation .second := by simp [canonicalLoopExcitation] | third => calc ℓ .third = ℓ .second + 1 := h.third_adds_one _ = (ℓ .first + 1) + 1 := by rw [h.second_adds_one] _ = (0 + 1) + 1 := by rw [h.ground_level] _ = canonicalLoopExcitation .third := by simp [canonicalLoopExcitation]The theorem minimalLoopExcitation_unique then proves that the only function meeting this condition is the canonical one minimalLoopExcitation_unique · IndisputableMonolith/Masses/GenerationTorsionBridge.leanTHEOREM cubeGeometricTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Charged-generation torsion defined from Q₃ cube geometry alone. No raw numerals; every branch is a cube-combinatorial function of D. -/ def cubeGeometricTorsion : Generation → ℤ | .first => 0 | .second => (passive_field_edges D : ℤ) | .third => (W_endo D : ℤ)The torsion values 0, 11, and 17, which previously appeared as hardcoded numbers, are now seen as the result of counting edges and faces of a cube. cubeGeometricTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.leanMODEL canonicalLoopExcitation · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Cumulative count of independent Q₃ loop-layers excited by each generation. -/ def canonicalLoopExcitation : Generation → ℕ | .first => 0 | .second => 1 | .third => 2The declaration does not claim that the minimal loop excitation is the same as the mass of the particles. canonicalLoopExcitation · IndisputableMonolith/Masses/GenerationTorsionBridge.lean