module module moderate

`IndisputableMonolith.Masses.TorsionForcing`

Forces fermion generation torsion from the Hamiltonian cycle on the 3-cube together with J-cost additivity under the Recognition Composition Law. It records passive coupling at each CW level of Q3 and the torsion values that order excitations. Mass/weak eigenstate bases and the CKM-from-cube derivation import this module. The argument pairs Gray-code cycle geometry with RCL identities and positivity of J away from the ground state.

claimThe 3-cube $Q_3$ admits a Hamiltonian cycle of length $8$ visiting every vertex. Passive coupling at CW levels $0,1,2,3$ matches the generation torsion bridge. Under the Recognition Composition Law, the J-cost of summed windings is additive in the torsion charges; $J$ vanishes only at the ground state and is strictly positive for nonzero torsion.

background

Recognition Science places fermion generations on the 3-cube $Q_3$ (eight vertices, forced by T8: $D=3$). Upstream, ParticleGenerations answers why there are exactly three families; WindingCharges supplies the topological mechanism (conservation from winding numbers of lattice paths). ExcitationOrdering derives edge-before-face ordering from the CW-filtration of $Q_3$ plus J-cost monotonicity on $\varphi$-power ratios.

The J-cost is the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ fixed by T5 and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Generation torsion lives on the Gray-code cycle of the cube; passive subcells at each filtration level encode which couplings a generation feels.

This module sits between that geometric/combinatorial layer and the mass formulae: it packages the cycle existence, level-wise passive coupling, and RCL-additive torsion so downstream mass and mixing constructions can cite a single source.

proof idea

Not a single theorem: a short forcing package. Cycle facts establish a Hamiltonian tour on $Q_3$ with period equal to the vertex count (eight-tick octave geometry). Passive-at-level definitions for filtration degrees $0$--$3$ are checked against the generation torsion bridge coupling table. RCL lemmas reduce the cost of summed torsion charges to an additive identity in $J$, with ground-state vanishing and strict positivity off zero. Imports from Cost, GrayCycle, GenerationTorsionBridge, and ExcitationOrdering supply the algebraic and combinatorial lemmas; the module wires them into the torsion-forcing interface used by masses.

why it matters in Recognition Science

Without forced torsion and level-wise passive coupling, mass eigenstates on $Q_3$ and the CKM overlap have no geometric source. Downstream, MassWeakBases defines mass eigenstates from CW-level coupling (which passive subcells each generation couples to) and weak eigenstates from the SU(2) action; their overlap is the CKM matrix. CKMFromCube derives that matrix from $Q_3$, generation torsion ${0,11,17}$, and Gray-code chirality $[4,2,2]$.

The module therefore closes the bridge from cube combinatorics and RCL cost to the Standard Model mixing sector. It sits on the masses side of the forcing chain after T7 (eight-tick) and T8 ($D=3$), and feeds the weak-basis and CKM constructions rather than the bare mass ladder itself.

scope and limits

Does not derive numerical fermion masses or the phi-ladder yardstick formula.
Does not prove the measured CKM entries; only supplies torsion and passive-coupling inputs.
Does not establish alpha inverse or close the open infrared boundary condition on alpha.
Does not treat lepton PMNS mixing; downstream use here is quark-side (CKM).
Does not replace ExcitationOrdering or WindingCharges; it consumes them.

used by (2)

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

IndisputableMonolith.Foundation.MassWeakBases module_import
IndisputableMonolith.StandardModel.CKMFromCube module_import

depends on (8)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.WindingCharges module_import
IndisputableMonolith.Masses.ExcitationOrdering module_import
IndisputableMonolith.Masses.GenerationTorsionBridge module_import
IndisputableMonolith.Patterns.GrayCycle module_import

declarations in this module (38)

theorem hamiltonian_cycle_on_Q3 L89
theorem cycle_period_eq_vertices L94
def passiveAtLevel L111
theorem passiveAtLevel_0 L117
theorem passiveAtLevel_1 L118
theorem passiveAtLevel_2 L119
theorem passiveAtLevel_3 L120
theorem passiveAtLevel_matches_passiveCoupling L123
theorem rcl_additive_torsion L139
theorem rcl_jcost_of_sum L144
theorem jcost_ground L149
theorem jcost_positive_of_nonzero L153
structure CouplingProfile L173
def CWPrerequisite L188
theorem face_has_edge_boundary L195
def all_profiles L204
theorem all_profiles_complete L207
theorem cw_prerequisite_forces_three L215
theorem faces_without_edges_violates_cw L222
def profileTorsion L235
theorem profileTorsion_ground L239
theorem profileTorsion_edges L242
theorem profileTorsion_edges_faces L246
theorem admissible_torsion_values L252
theorem six_is_not_admissible L263
def RCLForcedTorsion L283
theorem generationTorsion_is_rcl_forced L292
theorem rcl_forced_torsion_unique L318
theorem rcl_forced_torsion_exists_unique L337
theorem rcl_forced_implies_cubeAdmissible L349
theorem rcl_forced_implies_incremental L356
theorem rcl_forced_implies_filtration L363
theorem cw_prerequisite_is_essential L372
theorem forced_torsion_ordered L382
theorem forced_jcost_ordering L385
theorem rsLedger_torsion_from_rcl L400
structure TorsionForcingCert L434
theorem torsion_forcing_certificate L448