module module high

`IndisputableMonolith.Masses.GenerationTorsionBridge`

Charged-generation torsion is defined purely from the combinatorics of the 3-cube Q₃, with no bare numerals: every branch is a cube-combinatorial function of dimension D. Mass theorists cite it to replace ad-hoc generation offsets by geometric counts. The module equates those geometric values to the standard generation-torsion triple and checks they match the known τ ladder steps.

claimCharged-generation torsion is a function of the $D=3$ cube $Q_3$ alone: each generation index is assigned a torsion value built from cube edge/face combinatorics (no free integers). The resulting triple equals the standard generation torsion, and the three values match the $\tau$-ladder steps used in the mass formula.

background

Recognition Science places fermion masses on a $\varphi$-ladder whose generation offsets (torsion) were historically boundary data. This module sits in the Masses domain and redefines those offsets from the geometry of the 3-cube $Q_3$, consistent with the forcing chain that fixes $D=3$ spatial dimensions and the eight-tick octave on the cube.

Upstream, BaselineDerivation already upgrades baseline rungs, octave offset, and generation ordering from $Q_3$ combinatorics. ParticleGenerations supplies the P-001 count of three fermion generations; WindingCharges gives the topological charge mechanism on lattice paths. Anchor centralises the parameter-free mass constants; GroundStateDynamics constrains equilibria in the variational ledger.

The module doc states the design rule: charged-generation torsion comes from $Q_3$ geometry alone, and every branch is a cube-combinatorial function of $D$, so no raw numerals appear in the definitions.

proof idea

The module introduces cube-geometric torsion as a combinatorial function of the 3-cube, then specialises to the first, second, and third generation branches. Equalities identify those geometric values with the existing generation-torsion constants and with the three $\tau$-ladder match points. A separate lemma records that the second generation corresponds to passive edges. The argument is definitional plus direct equational checks against the cube counts and the already-derived generation data, not a long tactic script.

why it matters in Recognition Science

Without a geometry-only bridge, generation torsion remains an inserted triple and blocks a fully derived mass ladder. This module supplies that bridge so downstream work can treat ${0,11,17}$-style offsets as cube data rather than inputs.

ExcitationOrdering imports it to derive edge-before-face excitation ordering for fermion generation torsion from the CW-filtration of $Q_3$ plus $J$-cost monotonicity on $\varphi$-power ratios. TorsionForcing imports it to close the structural gap: the generation torsion values are the unique ones compatible with the 8-tick Hamiltonian cycle on $Q_3$ projected onto the $\varphi$-ladder through the Recognition Composition Law. Together they advance the mass manuscripts from boundary assumptions toward derived status along the $D=3$ and eight-tick landmarks.

scope and limits

Does not prove experimental mass agreement or fit PDG values.
Does not derive the full mass formula; only the generation-torsion bridge.
Does not treat neutral or non-charged sectors beyond the charged-generation definitions.
Does not re-prove three generations or $D=3$; those are imported.
Does not establish uniqueness of torsion; that is left to TorsionForcing.

used by (2)

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

IndisputableMonolith.Masses.ExcitationOrdering module_import
IndisputableMonolith.Masses.TorsionForcing module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.GroundStateDynamics module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.WindingCharges module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.BaselineDerivation module_import
IndisputableMonolith.RecogSpec.RSLedger module_import

declarations in this module (43)

def cubeGeometricTorsion L66
lemma cubeGeoTorsion_first L71
lemma cubeGeoTorsion_second L73
lemma cubeGeoTorsion_third L75
theorem cubeGeoTorsion_values L78
theorem cubeGeoTorsion_eq_generationTorsion L90
theorem cubeGeoTorsion_second_eq L103
theorem cubeGeoTorsion_third_eq L109
theorem cubeGeoTorsion_matches_tau_0 L117
theorem cubeGeoTorsion_matches_tau_1 L122
theorem cubeGeoTorsion_matches_tau_2 L127
theorem second_gen_is_passive_edges L136
theorem third_gen_is_Epass_plus_F L141
theorem endogenous_matches_crystallographic L146
theorem gen3_minus_gen2_is_faces L152
structure CubeAdmissibleTorsion L166
theorem cubeGeoTorsion_admissible L172
theorem generationTorsion_admissible L178
theorem cubeAdmissible_unique L183
theorem cubeAdmissible_forces_canonical L196
theorem cubeAdmissible_ordered L209
def phiRatioConfig L223
theorem phi_zpow_eq_one_iff L228
def GroundStateCompatibleTorsion L262
theorem groundStateCompatible_forces_ground_zero L267
structure IncrementalCubeTorsion L289
theorem cubeAdmissible_iff_incremental L297
theorem cubeGeoTorsion_incremental L318
theorem generationTorsion_incremental L322
theorem incremental_forces_canonical L326
def generationSlotCount L333
theorem generationSlotCount_eq_three L336
theorem generationSlotCount_eq_loopCount L340
structure CubeGenerationFiltration L354
theorem generationTorsion_has_cube_filtration L361
theorem cubeFiltration_forces_canonical L368
def canonicalLoopExcitation L376
structure MinimalLoopExcitation L384
theorem canonicalLoopExcitation_minimal L391
theorem minimalLoopExcitation_unique L400
theorem one_new_independent_loop_per_generation_step L420
theorem minimalLoopExcitation_matches_generation_slots L427
theorem rsLedger_torsion_from_cube L437