Masses Excitation Ordering Excitation Ordering Implies Filtration

Excitation Ordering

In the Recognition Science framework, particle generations are described as excitations of a three-dimensional cube. The cube has a natural structure: eight vertices, twelve edges, and six faces. The framework's ledger, a discrete record of recognition events, assigns a torsion value to each generation. The ground generation has torsion zero. The first excitation adds the number of passive edges, eleven. The second excitation adds the number of faces, six, for a total of seventeen.

The theorem excitation_ordering_implies_filtration states a conditional result. If excitations couple to the cube's subcells in order of their dimension, then the resulting torsion schedule is exactly the canonical one. This means the first nontrivial excitation is edge-supported, the next independent excitation is face-supported, and the resulting schedule is the one the framework already uses. The ordering is a geometric fact: edges have dimension one, faces have dimension two, and one is less than two.

The framework also proves that the cost function J, which measures the cost of recognition, respects this ordering. The cost of the ground state is zero, the cost of the edge excitation is positive, and the cost of the face excitation is strictly greater. This is shown through the monotonicity of J on powers of the golden ratio. The theorem demonstrates that the numerical schedule is not arbitrary but follows from a structural principle about the cube's geometry.

In Recognition Science, this result replaces the mode labels ground, edge, and face with a single geometric principle: excitations couple in order of CW dimension. The theorem does not prove that this coupling principle is true. It remains a structural premise about the coupling mechanism, not a consequence of the recognition cost law alone. The framework's library, a machine-checked collection of formal theorems, verifies the conditional statement and the cost ordering, but the premise itself is an assumption.

/-- From `ExcitationOrderingTheorem` we recover `CubeGenerationFiltration`. -/
theorem excitation_ordering_implies_filtration
    (h : ExcitationOrderingTheorem) :
    CubeGenerationFiltration generationTorsion := by
  rw [← h.cw_torsion_is_canonical]
  exact cwTorsion_has_filtration

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

What this page does not claim

The theorem does not prove that excitations actually couple in order of CW dimension. The theorem does not derive the coupling principle from the recognition cost law alone. The theorem does not establish the physical reality of the cube's subcells.

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: