Encyclopedia Masses Masses Generation Torsion Bridge Ground State Compatible Forces Ground Zero
ARTICLE 3 claims 3 theorems
Masses Generation Torsion Bridge Ground State Compatible Forces Ground Zero
A machine-checked proof shows that the first generation of matter must carry zero torsion, a geometric charge, if it is to be a stable ground state.
The ground state's zero
In particle physics, generations are the three families of matter: the electron, muon, and tau, each with its own neutrino. Recognition Science models each generation with a number called its torsion, a geometric charge that encodes how the generation couples to the shape of a cube. The declaration groundStateCompatible_forces_ground_zero proves that the first generation, the ground state, must have torsion exactly zero.
The proof starts from a condition called ground-state compatibility: the configuration must be an equilibrium and its logarithmic charge must be zero. From these two premises, the library derives that the golden ratio raised to the first generation's torsion must equal one. Since the golden ratio is not a root of unity, the only way this can hold is if the torsion itself is zero. The theorem is a formal derivation in the framework's machine-checked library of formal theorems.
This result is part of a larger derivation chain. The full torsion schedule for the three generations is {0, 11, 17}, where the second and third generations are built from the cube's edges and faces. The ground-state theorem isolates the first step of that schedule: it forces the starting point to be zero, independent of the later steps. It does not, by itself, derive the 11 or the 17.
The theorem's importance is that it anchors the generation ladder at a fixed origin. Without a zero, the ratios between generations would be free parameters. With the zero proven, the first rung of the ladder is not an assumption but a consequence of stability and charge balance.
THEOREM groundStateCompatible_forces_ground_zero · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Variational stability in the neutral sector forces the ground exponent to zero. -/
theorem groundStateCompatible_forces_ground_zero (τ : Generation → ℤ)
(h : GroundStateCompatibleTorsion τ) :
τ .first = 0 := by
rcases h with ⟨hEq, hCharge⟩
have hRatio :
IndisputableMonolith.Constants.phi ^ (τ .first) = 1 :=
GroundStateDynamics.stable_zero_charge_ratio_eq_one
(IndisputableMonolith.Constants.phi ^ (τ .first))
(zpow_pos IndisputableMonolith.Constants.phi_pos _)
hEq hCharge
exact (phi_zpow_eq_one_iff (τ .first)).mp hRatio
THEOREM GroundStateCompatibleTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- A torsion schedule is ground-state compatible if its first generation,
when realized as a one-channel φ-power ratio, is a neutral equilibrium of
the variational dynamics. -/
def GroundStateCompatibleTorsion (τ : Generation → ℤ) : Prop :=
IsEquilibrium (phiRatioConfig (τ .first)) ∧
log_charge (phiRatioConfig (τ .first)) = 0
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 : ℤ)
What this page does not claim
The theorem does not derive the second and third generation torsion values 11 and 17. The theorem does not claim that the first generation has zero mass. The theorem does not establish that the ground-state compatibility condition is itself derived from the cost functional.
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 physical principle selects the cube as the geometric source of the torsion schedule?
- How does the ground-state zero connect to the measured masses of the first-generation particles?
- Does the framework derive the 11 and 17 from the same stability condition, or from a separate premise?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM groundStateCompatible_forces_ground_zero · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- Variational stability in the neutral sector forces the ground exponent to zero. -/ theorem groundStateCompatible_forces_ground_zero (τ : Generation → ℤ) (h : GroundStateCompatibleTorsion τ) : τ .first = 0 := by rcases h with ⟨hEq, hCharge⟩ have hRatio : IndisputableMonolith.Constants.phi ^ (τ .first) = 1 := GroundStateDynamics.stable_zero_charge_ratio_eq_one (IndisputableMonolith.Constants.phi ^ (τ .first)) (zpow_pos IndisputableMonolith.Constants.phi_pos _) hEq hCharge exact (phi_zpow_eq_one_iff (τ .first)).mp hRatioThe declaration groundStateCompatible_forces_ground_zero proves that the first generation must have torsion exactly zero. groundStateCompatible_forces_ground_zero · IndisputableMonolith/Masses/GenerationTorsionBridge.leanTHEOREM GroundStateCompatibleTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.lean
/-- A torsion schedule is ground-state compatible if its first generation, when realized as a one-channel φ-power ratio, is a neutral equilibrium of the variational dynamics. -/ def GroundStateCompatibleTorsion (τ : Generation → ℤ) : Prop := IsEquilibrium (phiRatioConfig (τ .first)) ∧ log_charge (phiRatioConfig (τ .first)) = 0The proof starts from a condition called ground-state compatibility: the configuration must be an equilibrium and its logarithmic charge must be zero. GroundStateCompatibleTorsion · 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 full torsion schedule for the three generations is {0, 11, 17}. cubeGeometricTorsion · IndisputableMonolith/Masses/GenerationTorsionBridge.lean