Masses Torsion Forcing Faces Without Edges Violates Cw

The CW prerequisite

In the Recognition Science account of particle masses, a discrete record of events called the ledger tracks which parts of a three-dimensional cube are coupled into a generation. The cube's faces and edges can be coupled or not, giving four possible coupling profiles. One of those profiles, faces coupled but edges not, is impossible. The machine-checked theorem faces_without_edges_violates_cw proves exactly that: a coupling state that includes faces must include edges.

The reason is a topological fact about CW complexes, the standard way to build spaces from cells. A 2-cell (a face) is attached along its boundary, which consists of 1-cells (edges). You cannot have a face in the structure without its boundary edges. The theorem's proof is a two-line contradiction: assume the forbidden profile, derive that a face exists without an edge boundary, and the assumption collapses. The declaration cw_prerequisite_forces_three then shows the surviving profiles are exactly three: no coupling, edges only, and edges plus faces.

In Recognition Science, these three profiles map to the three observed particle generations. The forbidden profile would have produced a torsion value of 6, which the theorem six_is_not_admissible rules out. The admissible profiles yield torsion values 0, 11, and 17, and the theorem admissible_torsion_values confirms no other values are possible under the CW prerequisite. The framework's library of formal theorems establishes this as a structural constraint, not a dynamical assumption.

The declaration does not claim that the CW prerequisite alone determines particle masses. It only rules out one coupling profile. The full derivation of the torsion values 0, 11, and 17 requires additional ingredients: the 8-tick Hamiltonian cycle on the cube, the variational ground state at zero, and the bound of three generations. The theorem is a necessary condition, not a sufficient one.

/-- The eliminated profile ⟨false, true⟩ violates the CW prerequisite. -/
theorem faces_without_edges_violates_cw :
    ¬ CWPrerequisite ⟨false, true⟩ := by
  intro h; exact absurd (h rfl) (by decide)

/-- The CW prerequisite eliminates profile ⟨false, true⟩ (faces without edges).
    Exactly 3 profiles survive. -/
theorem cw_prerequisite_forces_three (p : CouplingProfile) (h : CWPrerequisite p) :
    p = ⟨false, false⟩ ∨ p = ⟨true, false⟩ ∨ p = ⟨true, true⟩ := by
  unfold CWPrerequisite at h
  rcases p with ⟨e, f⟩
  rcases e <;> rcases f <;> simp_all [CouplingProfile.mk.injEq]

/-- No other torsion values are possible: profile ⟨false, true⟩ would give
    τ = 6, but it is excluded by the CW prerequisite. -/
theorem six_is_not_admissible :
    profileTorsion D ⟨false, true⟩ = 6 ∧ ¬ CWPrerequisite ⟨false, true⟩ :=
  ⟨by simp [profileTorsion, passiveAtLevel, cube_faces, D],
   faces_without_edges_violates_cw⟩

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

What this page does not claim

The CW prerequisite alone determines the particle mass spectrum. The theorem proves that the three generations exist; it only constrains which coupling profiles are admissible. The declaration says nothing about the numerical values of particle masses, only about the torsion offsets.

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: