tickToBits
plain-language theorem explainer
The definition decomposes an index from the 8-tick cycle into a triple of bits, one per spatial dimension. Researchers deriving the three fermion generations from the Recognition Science 8-tick structure would cite this decomposition. It is realized as a direct arithmetic extraction of the least significant bits from the tick value.
Claim. For $ t $ an element of the 8-tick cycle index set $ Fin 8 $, the map returns the ordered triple $ (b_0, b_1, b_2) $ with each $ b_i $ in $ Fin 2 $, where $ b_0 = t.val mod 2 $, $ b_1 = (t.val / 2) mod 2 $, and $ b_2 = (t.val / 4) mod 2 $.
background
The module derives the existence of exactly three fermion generations from the 8-tick cycle crossed with three-dimensional space. TickIndex is the abbreviation for Fin 8, the discrete set of phases in one octave. The fundamental time quantum tick equals 1 in RS-native units and supplies the underlying period of length 8. Upstream results include the definition of tick as the RS time quantum and the theorem establishing structural conditions from seven axioms.
proof idea
Direct definition that computes the three bits by taking the value modulo 2 after successive divisions by 2 and 4. The Nat.mod_lt obligations are discharged by norm_num; no other lemmas are applied.
why it matters
This definition supplies the bit extraction step required by the bijectivity theorem bits_bijection. It realizes the hypothesis that the 8-tick cycle (T7) distributes across three dimensions (T8) to produce the generation quantum number. It supports the module's target of deriving the generation count from RS structure and feeds the parent theorem establishing the bijection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.