module module high

`IndisputableMonolith.Physics.ThreeGenerations`

The module defines the 8-tick cycle indexed by Fin 8 equals Fin 2 cubed as the structural backbone for three generations in Recognition Science. Particle physicists modeling generational structure and mass hierarchies cite the TickIndex, Generation, and mass_from_phi_ladder definitions here. It consists of definitions, bijections, and direct mappings from the cycle to dimensions and phi-ladder rungs with no complex proofs.

claimThe 8-tick cycle is the finite set $Fin 8$ with $8=2^3$, equipped with bijections to bit strings, a Generation type with three elements, and maps from tick indices to spatial dimensions and mass ratios on the phi-ladder.

background

Recognition Science quantizes time in fundamental ticks with tau_0 equal to 1 tick. The 8-tick cycle implements the eight-tick octave of period 2 cubed, arising from the self-similar fixed point structure. This module introduces TickIndex as elements of Fin 8, tickToBits and bitsToTick conversions, the Generation enumeration, three_generations, dimensionsFromTicks, dimensionToGeneration, massRatio, massHierarchyPattern, and mass_from_phi_ladder that place masses at phi-exponent rungs offset by generation and gap(Z).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete 8-tick indexing that realizes T7 in the forcing chain and feeds the three-generations structure into mass and dimension calculations. It directly supports the mass formula yardstick times phi to the power of rung minus 8 plus gap(Z) by providing the rung assignments via mass_from_phi_ladder and the generational offsets.

scope and limits

Does not derive the value 8 or the number of generations from T0-T8 axioms.
Does not compute explicit numerical masses for quarks or leptons.
Does not model mixing angles or decay widths between generations.
Does not address gauge interactions or symmetry breaking.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (22)

abbrev TickIndex L50
def tickToBits L53
def bitsToTick L59
theorem bits_bijection L67
inductive Generation L77
theorem three_generations L84
def dimensionsFromTicks L90
theorem dimensions_from_log L93
def dimensionToGeneration L102
def massRatio L111
def massHierarchyPattern L120
theorem mass_from_phi_ladder L125
theorem why_exactly_three L134
theorem no_fourth_generation L141
structure CKMElement L148
theorem ckm_from_phase_overlap L158
def cabibboAngle L162
structure PMNSElement L168
theorem neutrino_generations_match L178
def experimentalTests L188
structure GenerationFalsifier L202
def experimentalStatus L209