Masses Excitation Ordering Excitation Ordering Certificate

The ordering certificate

The declaration excitation_ordering_certificate is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It packages a conditional result about the three known generations of fermions, the matter particles that make up atoms. The result is conditional because it rests on a premise about how excitations couple to the geometry of a three-dimensional cube. The theorem says: if excitations attach to the cube's subcells in order of their dimension, then the first excitation is edge-supported, the second is face-supported, and the resulting torsion schedule, a number attached to each generation, equals the canonical one {0, 11, 17}.

The cube in question is the ordinary three-dimensional cube, which has 8 vertices (points), 12 edges, and 6 faces. The framework models each generation as an excitation that couples to subcells of a certain dimension. The ground generation couples only to vertices, contributing torsion 0. The first excitation adds edges, contributing 11. The second adds faces, contributing 6 more, for a total of 17. The certificate proves that this ordering is dimensional, not numerical: the number of edges (12) is not smaller than the number of faces (6), yet edges come first because their dimension (1) is less than that of faces (2).

The certificate also proves a strict cost ordering. Each torsion value feeds into a cost function J, which the framework derives from first principles. The theorem shows J(φ⁰) = 0 < J(φ¹¹) < J(φ¹⁷), where φ is the golden ratio. This means the ground state costs nothing, the first excitation costs more, and the second costs more still. The cost function is strictly monotonic, so the ordering is guaranteed by the mathematics, not by fitting.

In Recognition Science, this certificate is significant because it replaces unexplained mode labels with a single geometric principle: the filtration principle. The premise that excitations couple in order of CW dimension is a structural assumption about the coupling mechanism. It is not a consequence of the framework's core postulates alone. The certificate is a theorem about what follows from that premise, not a proof that the premise itself is true.

What the certificate does not claim is equally important. It does not prove that the filtration principle holds in nature. It does not derive the values 11 and 17 from scratch; those numbers come from the cube's geometry (12 edges minus 1 active, and 6 faces). It does not claim that the cost function J is the only possible cost function, though that uniqueness is proved elsewhere in the framework. The certificate is a precise conditional: if the premise holds, the ordering follows. The physical question of whether the premise holds remains open.

/-- Full certificate summarizing the CW-filtration route to generation torsion.

    **Proved**:
    - CW-dimensional ordering: dim(edge) < dim(face)
    - CW-cumulative torsion matches canonical schedule
    - J-cost strict ordering: ground < edge < face+edge
    - First increment = passive edges of Q₃
    - Second increment = faces of Q₃
    - Edge modes are the minimal nontrivial excitation (by CW dimension)
    - Ordering is dimensional (not numerical): 6 < 11 but edges come first
    - CW route recovers the full CubeGenerationFiltration package

    **Structural premise**: Excitations couple in order of CW dimension.
    This is a geometric principle about the cube rather than a mode label,
    but it is not yet derived from the cost functional. -/
theorem excitation_ordering_certificate :
    ExcitationOrderingTheorem ∧
    CubeGenerationFiltration generationTorsion ∧
    (∀ (cell : CubeCell D), 0 < passiveCoupling D cell →
      CubeCell.cwDim (.edge : CubeCell D) ≤ CubeCell.cwDim cell) ∧
    ((cube_faces D : ℤ) < (passive_field_edges D : ℤ)) :=
  ⟨excitation_ordering_holds,
   excitation_ordering_implies_filtration excitation_ordering_holds,
   edge_is_minimal_nontrivial_excitation,
   ordering_is_dimensional_not_numerical.1⟩

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

/-- Full certificate summarizing the CW-filtration route to generation torsion.

    **Proved**:
    - CW-dimensional ordering: dim(edge) < dim(face)
    - CW-cumulative torsion matches canonical schedule
    - J-cost strict ordering: ground < edge < face+edge
    - First increment = passive edges of Q₃
    - Second increment = faces of Q₃
    - Edge modes are the minimal nontrivial excitation (by CW dimension)
    - Ordering is dimensional (not numerical): 6 < 11 but edges come first
    - CW route recovers the full CubeGenerationFiltration package

    **Structural premise**: Excitations couple in order of CW dimension.
    This is a geometric principle about the cube rather than a mode label,
    but it is not yet derived from the cost functional. -/
theorem excitation_ordering_certificate :
    ExcitationOrderingTheorem ∧
    CubeGenerationFiltration generationTorsion ∧
    (∀ (cell : CubeCell D), 0 < passiveCoupling D cell →
      CubeCell.cwDim (.edge : CubeCell D) ≤ CubeCell.cwDim cell) ∧
    ((cube_faces D : ℤ) < (passive_field_edges D : ℤ)) :=
  ⟨excitation_ordering_holds,
   excitation_ordering_implies_filtration excitation_ordering_holds,
   edge_is_minimal_nontrivial_excitation,
   ordering_is_dimensional_not_numerical.1⟩

What this page does not claim

The certificate does not prove the filtration principle is true in nature. The certificate does not derive the numbers 11 and 17 from first principles; they come from the cube's geometry. The certificate does not claim that the cost function J is the only possible cost function.

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: