Masses Torsion Forcing Rcl Forced Torsion Exists Unique

The forced torsion schedule

In particle physics, the three generations of matter (up/down, charm/strange, top/bottom) differ by mass but share the same interactions. Recognition Science asks whether those mass differences could be forced by structure rather than chosen by hand. The declaration rcl_forced_torsion_exists_unique answers yes for a specific internal quantity: the torsion, or twist, that each generation carries in the framework's discrete record of events, its ledger.

The proof combines five ingredients. First, the framework's cost law, the Recognition Composition Law, forces independent contributions to add in the exponent of the golden ratio φ. Second, an 8-tick Hamiltonian cycle visits all 8 vertices of a cube graph, one edge active per tick, leaving 11 passive edges and 6 passive faces. Third, a topological fact about cube geometry: a face cannot be coupled without its boundary edges. Fourth, the ground state has zero torsion. Fifth, there are exactly three generations. Together these admit exactly three coupling profiles: no coupling (torsion 0), edges only (torsion 11), and edges plus faces (torsion 17).

The theorem rcl_forced_torsion_exists_unique states that there exists a unique function assigning torsion to each generation that satisfies all these constraints. Its companion rcl_forced_torsion_unique proves any such function must equal the canonical schedule {0, 11, 17}. The library also proves this schedule is ordered (0 < 11 < 17) and that the cost increases with torsion, so the ground state is cheapest.

What this does not claim: it does not derive the numerical values of particle masses. It derives torsion values, which are one ingredient in the framework's mass ladder, not masses themselves. It does not claim these are the only possible torsion values in all conceivable frameworks; the proof depends on the specific Hamiltonian cycle, the CW topology of the cube, and the cost law. It does not claim the physical bridge from torsion to measured masses is complete; that comparison remains a separate empirical check.

/-- The forcing is genuinely unique: there is exactly one RCL-forced schedule. -/
theorem rcl_forced_torsion_exists_unique :
    ∃! τ : Generation → ℤ, RCLForcedTorsion D τ := by
  refine ⟨generationTorsion, generationTorsion_is_rcl_forced, ?_⟩
  intro τ hτ
  exact rcl_forced_torsion_unique τ hτ

/-- **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]

/-- 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)

/-- The three forced torsion values are strictly ordered. -/
theorem forced_torsion_ordered : (0 : ℤ) < 11 ∧ (11 : ℤ) < 17 := by omega

/-- J-costs of the forced values are strictly ordered. -/
theorem forced_jcost_ordering :
    Jcost (phi ^ (0 : ℤ)) = 0 ∧
    0 < Jcost (phi ^ (11 : ℤ)) ∧
    Jcost (phi ^ (11 : ℤ)) < Jcost (phi ^ (17 : ℤ)) :=
  ⟨jcost_ground,
   jcost_positive_of_nonzero 11 (by omega),
   excitationCost_strictMono (by omega : (0 : ℤ) ≤ 11) (by omega : (11 : ℤ) < 17)⟩

What this page does not claim

The theorem derives torsion values, not particle masses themselves. The proof depends on the specific Hamiltonian cycle, CW topology, and cost law; it does not claim universality across all frameworks. The physical bridge from torsion to measured masses is not established by this declaration.

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: