Masses Excitation Ordering Ordering Is Dimensional Not Numerical

The dimensional ordering

A cube has 8 vertices, 12 edges, and 6 faces. The numbers 12 and 6 might suggest that edges, being more numerous, cost more to excite than faces. The theorem ordering_is_dimensional_not_numerical in the Recognition Science library states the opposite: it proves that the first excitation is edge-supported and the next is face-supported, even though there are more edges than faces. The reason is dimensional, not numerical. Edges have dimension 1 and faces have dimension 2, and the framework's cost function, which assigns a recognition cost to each excitation, increases strictly with the torsion, a discrete count of passive subcells coupled to the excitation. Since dimension 1 is less than dimension 2, edges come before faces.

The proof rests on the CW-filtration of the 3-cube, a standard topological way to build the cube from lower-dimensional pieces: first the 8 vertices (dimension 0), then the 12 edges (dimension 1), then the 6 faces (dimension 2). The framework models generation excitations as coupling to these subcells in order of dimension. The ground state couples only to vertices, giving torsion 0. The first excitation adds the 11 passive edges, giving torsion 11. The second adds the 6 faces, giving torsion 17. The cost function J, which is zero at the ground state and strictly increasing in torsion, then forces the strict ordering 0 < J(11) < J(17). The theorem edge_is_minimal_nontrivial_excitation proves that the edge is the cheapest nontrivial excitation among all cell types.

The key insight is that the ordering is a geometric fact about the cube, not an arithmetic accident. The theorem edge_dim_lt_face_dim proves dimension 1 is less than dimension 2, and the theorem cube_faces_lt_passive_edges proves 6 is less than 11. The conjunction of these two facts, stated in ordering_is_dimensional_not_numerical, is what makes the excitation schedule {0, 11, 17} canonical. The framework's library shows this schedule satisfies the admissibility and filtration conditions that define a valid generation torsion.

In Recognition Science, this result replaces the unexplained mode labels ground, edge, and face with a single structural principle: excitations couple in order of CW dimension. The framework proves this ordering is strict and that the edge is the minimal nontrivial excitation. It does not prove that the coupling mechanism itself is forced by the recognition cost law alone. That coupling premise, called the filtration principle, remains a structural assumption about how excitations attach to the cube's subcells, not a consequence derived from the cost function.

/-- The CW-ordering is *dimensional*, not numerical: face coupling (6) is
    numerically smaller than edge coupling (11), but edges come first because
    dim(edge) = 1 < dim(face) = 2.

    This makes explicit that generation ordering cannot be explained by
    "smallest torsion increment first" — it requires the geometric notion
    of subcell dimension. -/
theorem ordering_is_dimensional_not_numerical :
    (cube_faces D : ℤ) < (passive_field_edges D : ℤ) ∧
    CubeCell.cwDim (.edge : CubeCell D) < CubeCell.cwDim (.face : CubeCell D) := by
  constructor
  · simp [cube_faces, passive_field_edges, cube_edges, active_edges_per_tick, D]
  · exact edge_dim_lt_face_dim

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

/-- Among all subcell types with nonzero passive coupling, edges have the
    smallest CW dimension. The variational principle (selecting cheapest
    excitation) therefore selects edge modes first. -/
theorem edge_is_minimal_nontrivial_excitation :
    ∀ (cell : CubeCell D),
    0 < passiveCoupling D cell →
    CubeCell.cwDim (.edge : CubeCell D) ≤ CubeCell.cwDim cell := by
  intro cell hpos
  cases cell with
  | vertex => simp [passiveCoupling] at hpos
  | edge => exact le_refl _
  | face => exact Nat.le_of_lt edge_dim_lt_face_dim

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

/-- Torsion schedule derived from cumulative CW-filtration.

    Generation g couples to all subcells of CW dimension ≤ (g - 1):
    - Gen 1 (ground): dim ≤ -1 → nothing → τ = 0
    - Gen 2: dim ≤ 0 already covered, new: dim 1 → adds edge coupling
    - Gen 3: dim ≤ 1 already covered, new: dim 2 → adds face coupling -/
def cwCumulativeTorsion (d : ℕ) : Generation → ℤ
  | .first  => 0
  | .second => (passiveCoupling d .edge : ℤ)
  | .third  => (passiveCoupling d .edge + passiveCoupling d .face : ℤ)

What this page does not claim

This theorem does not prove that the coupling mechanism itself is forced by the recognition cost law alone. This theorem does not claim that the numerical values 11 and 17 are derived from the cube's geometry without the coupling premise. This theorem does not establish any empirical connection to measured particle masses.

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: