pith. sign in
module module high

IndisputableMonolith.Physics.ThreeGenerations

show as:
view Lean formalization →

The module encodes the eight-tick octave of Recognition Science as indices in Fin 8, together with bit-string bijections, a Generation type, and phi-ladder mass assignments. Physicists modeling fermion spectra or the three-generation pattern would cite its definitions of three_generations and mass_from_phi_ladder. It is a definitions-only module with no internal theorems.

claimThe 8-tick cycle is indexed by $Fin 8 = Fin 2^3$, equipped with bijections $tickToBits$ and $bitsToTick$, a type $Generation$ of three values, and mass ratios $mass_from_phi_ladder$ placed on the $phi$-ladder.

background

The module imports the RS time quantum $tau_0 = 1$ tick from IndisputableMonolith.Constants. It introduces the 8-tick cycle required by the forcing chain (T7) and defines supporting objects: TickIndex as Fin 8, the bijection bits_bijection, Generation, three_generations, dimensionsFromTicks, dimensionToGeneration, and mass_from_phi_ladder. These realize the discrete time structure that yields three fermion generations and the spatial dimension count.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the eight-tick octave (T7) that realizes the period $2^3$ structure in the UnifiedForcingChain and supplies the indices used by mass_from_phi_ladder and dimensions_from_log. It therefore underpins the mass formula and the derivation of D=3. No downstream declarations are listed.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (22)