Masses Torsion Forcing Rcl Forced Implies Cube Admissible

The admissible torsion theorem

A cube has 8 corners, 12 edges, and 6 faces. In the Recognition Science framework, a ledger, a discrete record of events, assigns a number called torsion to each of three generations of particles. The theorem rcl_forced_implies_cubeAdmissible proves that if a torsion assignment obeys the framework's fundamental composition law, then it automatically satisfies the previously assumed "cube admissible" condition. The proof is machine-checked, meaning a computer verified every logical step.

The composition law, written J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), is the framework's core equation. It forces a specific structure: the allowed torsion values are exactly 0, 11, and 17. The theorem shows that any assignment following this law must be one of these three values, and it must be ordered from lowest to highest. This is not a numerical coincidence; it is a proved consequence of the law itself.

The proof works by showing that the law forces a particular pattern of "coupling" between edges and faces of the cube. A coupling state that includes faces must also include edges, a topological fact about how faces attach to edges. This restriction leaves only three possible configurations, corresponding to the three torsion values. The theorem closes a gap: what was once an explicit structural premise is now a derived result.

In Recognition Science, this result is significant because it shows that the framework's assumptions are not arbitrary. The three generations of particles, with their specific torsion values, are not put in by hand; they follow from the composition law. The theorem does not claim that these values match any physical measurement, nor does it claim that the composition law is the only possible starting point. It only establishes the logical consequence within the framework.

/-- RCL-forced torsion implies CubeAdmissibleTorsion. -/
theorem rcl_forced_implies_cubeAdmissible (τ : Generation → ℤ)
    (h : RCLForcedTorsion D τ) :
    CubeAdmissibleTorsion D τ := by
  rw [rcl_forced_torsion_unique τ h]
  exact generationTorsion_admissible

/-- 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 CW prerequisite is the reason profile ⟨false, true⟩ is excluded.
    Without it, a fourth "face-only" family with τ = 6 would be admissible,
    and the torsion schedule would not be forced. -/
theorem cw_prerequisite_is_essential :
    profileTorsion D ⟨false, true⟩ ∉ ({0, 11, 17} : Set ℤ) := by
  simp [profileTorsion, passiveAtLevel, cube_faces, D, Set.mem_insert_iff]

What this page does not claim

This theorem does not claim that the torsion values 0, 11, and 17 match any measured physical quantities. This theorem does not claim that the composition law is the only possible starting point for the framework. This theorem does not claim that the cube admissible condition is necessary for all possible torsion assignments, only those forced by the composition law.

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: