Encyclopedia Masses Masses Excitation Ordering

ARTICLE 5 claims 5 theorems

Masses Excitation Ordering

A geometric fact about a cube, edges before faces, explains why particle generations appear in a fixed order.

Excitation ordering

In particle physics, the three generations of fermions (electron, muon, tau, and their heavier cousins) are usually treated as unexplained facts. They have different masses, but no principle says why the second generation should be heavier than the first, or why the third should be heavier than the second. The standard model simply lists them. Recognition Science asks whether that ordering is forced by something more basic.

The framework's answer begins with a ledger, a discrete record of recognition events. Each event has a cost, a number measuring how expensive that recognition was. The cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain conditions, and it is strictly increasing for arguments above 1. That monotonicity means if one excitation has a larger cost than another, the ordering is strict: lower cost always comes first.

The framework then looks at the three-dimensional cube Q₃, the natural geometric object in three spatial dimensions. The cube has a standard structure called a CW-filtration, built from subcells of increasing dimension: 8 vertices (dimension 0), 12 edges (dimension 1), and 6 faces (dimension 2). The key premise is the filtration principle: excitations couple to subcells in order of CW dimension, so the first excited state couples only to vertices, the next to edges, the next to faces.

That single premise produces the canonical torsion schedule {0, 11, 17}. The ground state couples to vertices only, giving torsion 0. The first excitation adds the 11 passive edges, giving torsion 11. The second excitation adds the 6 faces, giving torsion 17. The framework proves these numbers are exactly the canonical generation torsion values, and it proves the strict cost ordering J(φ⁰) = 0 < J(φ¹¹) < J(φ¹⁷), where φ is the golden ratio. The geometric fact that edges have lower dimension than faces (dim 1 < dim 2) is what makes edges come before faces.

In plain language: if excitations attach to a cube's parts in order of their dimension, then edges must come before faces, and the resulting cost ordering is strict. The theorem excitation_ordering_certificate packages this: the ordering holds, the torsion schedule is canonical, the edge is the minimal nontrivial excitation, and the dimensional ordering is what drives it. The filtration principle itself remains a structural premise, not a consequence of the recognition cost law alone.

THEOREM Jcost_strict_mono_pos · IndisputableMonolith/Masses/ExcitationOrdering.lean
/-- J-cost is strictly increasing on [1, ∞).

    Proof: write `J(x) = (x + 1/x)/2 - 1` and show `x + 1/x` is strictly
    increasing for `x ≥ 1` via the identity
      `(y + 1/y) - (x + 1/x) = (y - x)(xy - 1)/(xy)`,
    which is positive when `1 ≤ x < y`. -/
theorem Jcost_strict_mono_pos {x y : ℝ} (hx : 0 < x) (hy : 0 < y)
    (hx1 : 1 ≤ x) (hxy : x < y) :
    Jcost x < Jcost y := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  have hy0 : y ≠ 0 := ne_of_gt hy
  simp only [Jcost]
  suffices h : x + x⁻¹ < y + y⁻¹ by linarith
  have hxy_pos : 0 < x * y := mul_pos hx hy
  have hyx : 0 < y - x := sub_pos.mpr hxy
  have hxy1 : 0 < x * y - 1 := by nlinarith
  have key : y + y⁻¹ - (x + x⁻¹) = (y - x) * (x * y - 1) / (x * y) := by
    field_simp
    ring
  linarith [div_pos (mul_pos hyx hxy1) hxy_pos]
THEOREM cwTorsion_second · IndisputableMonolith/Masses/ExcitationOrdering.lean
@[simp] theorem cwTorsion_first  : cwCumulativeTorsion D .first  = 0 := rfl
@[simp] theorem cwTorsion_second : cwCumulativeTorsion D .second = 11 := by native_decide
THEOREM cwTorsion_third · IndisputableMonolith/Masses/ExcitationOrdering.lean
@[simp] theorem cwTorsion_first  : cwCumulativeTorsion D .first  = 0 := rfl
@[simp] theorem cwTorsion_second : cwCumulativeTorsion D .second = 11 := by native_decide
@[simp] theorem cwTorsion_third  : cwCumulativeTorsion D .third  = 17 := by native_decide
THEOREM excitation_cost_ordering · IndisputableMonolith/Masses/ExcitationOrdering.lean
/-- The three generation torsion values have strictly ordered J-costs. -/
theorem excitation_cost_ordering :
    excitationCost 0 = 0 ∧
    0 < excitationCost 11 ∧
    excitationCost 11 < excitationCost 17 :=
  ⟨excitationCost_ground,
   excitationCost_pos_of_ne_zero 11 (by omega),
   excitationCost_strictMono (by omega) (by omega)⟩
THEOREM edge_dim_lt_face_dim · IndisputableMonolith/Masses/ExcitationOrdering.lean
/-- CW-dimensional ordering: edges are strictly lower-dimensional than faces. -/
theorem edge_dim_lt_face_dim :
    CubeCell.cwDim (.edge : CubeCell D) < CubeCell.cwDim (.face : CubeCell D) := by
  decide

What this page does not claim

The filtration principle is proved from the recognition cost law alone; it remains a structural premise. The framework derives the actual mass values of the fermions, only their excitation ordering. The framework applies to dimensions other than three without further argument.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND