bitsToTick
plain-language theorem explainer
The definition converts a triple of bits into an index on the 8-tick cycle by treating the bits as binary digits weighted by powers of two. Researchers working on the origin of three fermion generations from the 8-tick structure in three dimensions would cite this map when establishing invertibility of the bit decomposition. The implementation forms the integer sum of the bit values and applies the omega tactic to certify the result lies inside Fin 8.
Claim. Let $b = (b_0, b_1, b_2)$ with each $b_i$ a value in Fin 2. Define the tick index $t = b_0 + 2 b_1 + 4 b_2$, which satisfies $t < 8$ and therefore belongs to the type Fin 8.
background
TickIndex is the abbreviation Fin 8, the discrete index set for the eight-tick cycle that arises from the self-similar fixed point and the period-2^3 structure. The module Physics.ThreeGenerations examines how this cycle, crossed with three spatial dimensions, produces exactly three generations of fermions, each generation corresponding to a distinct parity pattern across the three dimensions. The supplied definition supplies the reconstruction direction of the bit-to-index map, complementing the sibling decomposition that extracts the three bits from a given tick index.
proof idea
The definition builds the Fin 8 element by the standard binary weighting: the first component contributes its value, the second twice that value, and the third four times that value. The proof obligation that the resulting integer is strictly less than 8 is discharged by extracting the three separate bounds (each component value is less than 2) and invoking the omega tactic.
why it matters
This definition is the forward map required by the bijection theorem bits_bijection, which proves that every tick index recovers uniquely from its three-bit representation. It therefore supplies one half of the counting argument that exactly three generations arise from the 8-tick cycle distributed across three dimensions. The module doc-comment frames the construction as a step toward deriving the observed generation number directly from the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.