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:
- What physical mechanism would make excitations couple to cube subcells in order of CW dimension?
- Does the excitation ordering extend to higher-dimensional cubes beyond three dimensions?
- How does the torsion schedule {0, 11, 17} translate into the measured mass ratios of the three fermion generations?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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]The cost function J(x) = (x + 1/x)/2 - 1 is strictly increasing for arguments above 1. Jcost_strict_mono_pos · IndisputableMonolith/Masses/ExcitationOrdering.leanTHEOREM 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_decideThe first excitation couples to the 11 passive edges, giving torsion 11. cwTorsion_second · IndisputableMonolith/Masses/ExcitationOrdering.leanTHEOREM 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_decideThe second excitation adds the 6 faces, giving torsion 17. cwTorsion_third · IndisputableMonolith/Masses/ExcitationOrdering.leanTHEOREM 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)⟩The strict cost ordering J(φ⁰) = 0 < J(φ¹¹) < J(φ¹⁷) holds. excitation_cost_ordering · IndisputableMonolith/Masses/ExcitationOrdering.leanTHEOREM 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 decideEdges have lower CW dimension than faces, which is what makes edges come before faces. edge_dim_lt_face_dim · IndisputableMonolith/Masses/ExcitationOrdering.lean