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
groundStateCompatible_forces_ground_zero · IndisputableMonolith/Masses/GenerationTorsionBridge.lean:266
/-- 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND