module module moderate

`IndisputableMonolith.Masses.ExcitationOrdering`

Defines the 0-, 1-, and 2-dimensional subcells of the hypercube Q_D used for fermion generation coupling, with counts and a passive-coupling weight on each type. Mass and torsion authors cite it when ranking excitations by geometric dimension before projecting onto the φ-ladder. The module is mostly definitions plus elementary dimension and positivity lemmas.

claimOn the $D$-dimensional hypercube $Q_D$, the subcell types relevant to fermion generation coupling are vertices ($0$-cells), edges ($1$-cells), and faces ($2$-cells). Each type has a combinatorial count and a passive coupling weight; edge dimension is strictly less than face dimension, and vertex dimension is strictly less than edge dimension.

background

Recognition Science ties charged-generation structure to the geometry of the cube $Q_3$ (and more generally $Q_D$). The upstream Generation Torsion Bridge module is the authoritative source that charged-generation torsion values ${0, 11, 17}$ arise from that cube geometry and match every other representation in the codebase.

This module isolates the subcell vocabulary needed before torsion is forced: a CubeCell classification restricted to dimensions $0,1,2$, the corresponding subcell counts, and a passive coupling assigned to each type. Those objects sit between raw cube combinatorics and the later ranking of excitations that feed mass and torsion arguments.

Notation is elementary: dimension comparisons are ordinary inequalities on cell dimension, and passive coupling is a nonnegative weight used to order how strongly a subcell type participates in generation coupling.

proof idea

Definition-heavy module. It introduces the subcell type, count functions for vertex/edge/face, and passive-coupling weights, then proves the expected dimension inequalities (vertex $<$ edge $<$ face in dimension) and positivity of the edge passive coupling by direct case analysis on the finite type. No deep analytic argument; the content is combinatorial bookkeeping for downstream forcing.

why it matters in Recognition Science

Supplies the geometric ordering layer that TorsionForcing imports when it closes the structural gap: generation torsion ${0, 11, 17}$ as the unique values compatible with the 8-tick Hamiltonian cycle on $Q_3$ projected onto the $\varphi$-ladder through the Recognition Composition Law. Without a clean vertex/edge/face stratification and passive weights, that uniqueness argument has no ranked excitation input.

In the broader chain this sits under the eight-tick octave (T7) and the cube geometry that sources generation structure, feeding mass-side torsion rather than the J-uniqueness or $D=3$ forcing steps themselves.

scope and limits

Does not derive torsion values {0, 11, 17}; only subcell types and couplings.
Does not prove uniqueness under the 8-tick cycle or RCL; that is TorsionForcing.
Does not treat cells of dimension greater than 2 for generation coupling.
Does not assign particle masses or φ-ladder rungs; only geometric ordering data.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Masses.TorsionForcing module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.GenerationTorsionBridge module_import

declarations in this module (35)

inductive CubeCell L62
def subcellCount L75
theorem subcellCount_vertex L80
theorem subcellCount_edge L81
theorem subcellCount_face L82
theorem edge_dim_lt_face_dim L85
theorem vertex_dim_lt_edge_dim L90
def passiveCoupling L100
theorem passiveCoupling_vertex L105
theorem passiveCoupling_edge L106
theorem passiveCoupling_face L107
theorem passiveCoupling_edge_pos L109
theorem passiveCoupling_face_pos L110
def cwCumulativeTorsion L120
theorem cwTorsion_first L125
theorem cwTorsion_second L126
theorem cwTorsion_third L127
theorem cwTorsion_eq_generationTorsion L130
theorem first_increment_is_passive_edges L143
theorem second_increment_is_faces L149
theorem cwTorsion_cubeAdmissible L156
theorem Jcost_strict_mono_pos L169
def excitationCost L187
theorem excitationCost_ground L190
theorem excitationCost_pos_of_ne_zero L194
theorem excitationCost_strictMono L202
theorem excitation_cost_ordering L211
structure ExcitationOrderingTheorem L240
theorem excitation_ordering_holds L258
theorem edge_is_minimal_nontrivial_excitation L275
theorem ordering_is_dimensional_not_numerical L292
theorem cwTorsion_incremental L302
theorem cwTorsion_has_filtration L308
theorem excitation_ordering_implies_filtration L314
theorem excitation_ordering_certificate L337