bits_bijection
plain-language theorem explainer
The bijection establishes that decomposing any index in the 8-tick cycle into its three-bit pattern and reconstructing the index recovers the original value exactly. Physicists deriving the three fermion generations from the 8-tick by 3D structure in Recognition Science would cite this to anchor the discrete parity patterns. The proof reduces to unfolding the bit maps, extensionality on the finite index, and omega arithmetic.
Claim. For every tick index $t$ in the finite set Fin 8, the composition of bit reconstruction after bit decomposition satisfies bitsToTick(tickToBits($t$)) = $t$.
background
TickIndex is the abbreviation Fin 8 for the 8-tick cycle arising from the period-8 structure. The sibling functions tickToBits and bitsToTick decompose each index into a 3-bit tuple with one bit per spatial dimension. The module derives the three generations of fermions from parity patterns across these dimensions in the 8-tick cycle times 3D space, as stated in the SM-011 documentation on why three generations appear from this structure.
proof idea
The term-mode proof first simplifies using the definitions of tickToBits and bitsToTick, then applies extensionality to reduce to componentwise equality on the finite index, followed by simplification and the omega tactic to discharge the resulting arithmetic.
why it matters
This bijection grounds the mapping from the 8-tick cycle to three-dimensional bit patterns that produces exactly three generations. It supports the three_generations and dimensionToGeneration declarations in the same module and connects to the eight-tick octave (T7) together with D = 3 (T8) in the UnifiedForcingChain. The module documentation frames the result as a step toward deriving the generation number, an open puzzle in the Standard Model, with a noted PRL paper possibility if the physical assignment holds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.