Masses Generation Torsion Bridge Cube Geo Torsion Eq Generation Torsion

The geometric torsion schedule

In particle physics, the three generations of matter (electron, muon, tau, and their neutrino partners) are distinguished by mass and flavor, but the standard model offers no explanation for why there are exactly three or what integer labels them. The Recognition Science framework proposes an answer: each generation carries a torsion integer, and those integers are forced by the geometry of a three-dimensional cube. The declaration cubeGeoTorsion_eq_generationTorsion is the formal bridge that proves the geometric count and the framework's canonical schedule are the same object.

The geometric schedule is built from plain cube arithmetic. The ground generation gets torsion 0, meaning no geometric coupling. The second generation gets the number of passive field edges of a cube, which is 11. The third gets that same edge count plus the number of faces, 11 + 6 = 17. The declaration proves this three-number schedule equals the framework's generation torsion schedule pointwise, for every generation. A separate theorem shows the schedule is unique: any assignment satisfying the structural predicate CubeAdmissibleTorsion (ground is zero, second is passive edges, third is passive edges plus faces) must equal the canonical one. The proof is machine-checked in the framework's library of formal theorems.

The number 17 also coincides with the count of crystallographic wallpaper groups, classified by Fedorov in 1891. The framework proves this coincidence but is explicit that it is not the source of the integer; the primary route is the cube arithmetic itself. What the declaration does not claim is that the physical coupling rule is derived from the cost functional. The predicate CubeAdmissibleTorsion encodes a structural premise about how generations attach to cube features, and until that coupling is derived from the recognition cost ledger, the framework has upgraded the gap from hardcoded numerals to an explicit structural premise with a uniqueness proof.

What the declaration changes is the status of the generation labels. They are no longer three arbitrary numbers; they are the unique solution to a stated geometric condition. The remaining open question is whether that condition itself follows from the deeper recognition dynamics, which the framework leaves as a target.

/-- The geometric schedule matches `Integers.tau` at generation index 0. -/
theorem cubeGeoTorsion_matches_tau_0 :
    cubeGeometricTorsion .first = Integers.tau 0 := by
  simp [cubeGeometricTorsion, Integers.tau]

@[simp] lemma cubeGeoTorsion_first : cubeGeometricTorsion .first = 0 := rfl

@[simp] lemma cubeGeoTorsion_second : cubeGeometricTorsion .second = (passive_field_edges D : ℤ) := rfl

/-- The third-generation torsion is E_passive + F (endogenous wallpaper route). -/
theorem third_gen_is_Epass_plus_F :
    cubeGeometricTorsion .third = ↑(passive_field_edges D + cube_faces D) := by
  simp [cubeGeometricTorsion, W_endo]

/-- At D=3, any cube-admissible schedule equals the canonical `generationTorsion`. -/
theorem cubeAdmissible_forces_canonical (τ : Generation → ℤ)
    (h : CubeAdmissibleTorsion D τ) :
    τ = generationTorsion := by
  rw [← cubeGeoTorsion_eq_generationTorsion]
  funext g
  cases g with
  | first => exact h.ground_is_zero
  | second => exact h.edge_mode
  | third =>
    simp only [cubeGeometricTorsion, W_endo]
    exact h.face_edge_mode

What this page does not claim

The physical coupling rule is derived from the cost functional; it remains a structural premise. The coincidence with the wallpaper group count is the source of the integer 17. The framework explains why the cube's passive edges number 11 rather than some other value.

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: