Masses Torsion Forcing

The forced torsion values

In Recognition Science, the masses of the three known particle generations are not free parameters. They are encoded as offsets, called torsion values, on a ladder of powers of the golden ratio. Torsion forcing is the proof that only three such offsets can exist, and that they must be 0, 11, and 17.

The argument starts with a recognition cycle: a discrete record of events where each of eight states is visited exactly once, forming a Hamiltonian cycle on a three-dimensional cube. At each step of this cycle, one edge is active while 11 others are passive, and 6 faces sit on the skeleton. The framework's composition law, which governs how recognition costs combine, turns these counts into additive contributions to the torsion.

The key constraint comes from the topology of the cube. A face cannot be coupled without its boundary edges, a fact about CW complexes that is not a dynamical assumption. This single rule eliminates the profile that would couple faces but not edges, which would otherwise give a torsion of 6. The remaining profiles, no coupling, edges only, and edges plus faces, produce exactly the values 0, 11, and 17.

In Recognition Science, the framework's machine-checked library of formal theorems proves that these are the unique possibilities. The theorem rcl_forced_torsion_unique establishes that any torsion assignment satisfying the forced conditions must equal the canonical one. The theorem admissible_torsion_values shows that any coupling profile respecting the CW prerequisite yields one of the three values. A separate result, jcost_ground, confirms that the zero torsion state has zero cost, making it the natural ground state.

What this establishes is that the mass spectrum is not a list of inputs but a consequence of the recognition cycle's structure. The three values are not fitted; they are forced by the combination of the cycle, the topology, and the composition law. This turns the previously assumed torsion values into a derived result.

/-- The three admissible profiles yield exactly {0, 11, 17}. -/
theorem admissible_torsion_values :
    ∀ p : CouplingProfile, CWPrerequisite p →
      profileTorsion D p = 0 ∨ profileTorsion D p = 11 ∨ profileTorsion D p = 17 := by
  intro p hp
  rcases cw_prerequisite_forces_three p hp with rfl | rfl | rfl
  · exact Or.inl profileTorsion_ground
  · exact Or.inr (Or.inl profileTorsion_edges)
  · exact Or.inr (Or.inr profileTorsion_edges_faces)

/-- **Main Theorem**: RCL-forced torsion on Q₃ is unique and equals
    the canonical `generationTorsion` = {0, 11, 17}.

    This theorem derives the torsion schedule from:
    - T5 (RCL uniqueness): additive channel composition
    - T7 (8-tick Hamiltonian cycle): passive geometry partition
    - CW topology of Q₃: boundary prerequisite
    - Variational dynamics: ground state at zero
    - T8 (D = 3): three generations from face-pairs -/
theorem rcl_forced_torsion_unique (τ : Generation → ℤ)
    (h : RCLForcedTorsion D τ) :
    τ = generationTorsion := by
  obtain ⟨profiles, _, h1, h2, h3, hτ⟩ := h
  funext g
  rw [hτ g]
  cases g with
  | first =>
    rw [h1]; simp [profileTorsion, generationTorsion]
  | second =>
    rw [h2]
    simp [profileTorsion, passiveAtLevel, generationTorsion,
          passive_field_edges, cube_edges, active_edges_per_tick, D]
  | third =>
    rw [h3]
    simp [profileTorsion, passiveAtLevel, generationTorsion,
          passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]

/-- Ground-state J-cost is zero: J(φ⁰) = J(1) = 0. -/
theorem jcost_ground : Jcost (phi ^ (0 : ℤ)) = 0 := by
  simp [zpow_zero, Jcost_unit0]

What this page does not claim

This module does not derive the numerical values of the particle masses themselves, only the torsion offsets. The CW prerequisite is a topological fact about the cube, not a dynamical assumption about recognition. The uniqueness theorem applies to the torsion schedule, not to the full mass spectrum.

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/TorsionForcing.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: