bitNat
plain-language theorem explainer
Boolean-to-natural conversion: true maps to 1, false to 0. Anyone packing Pattern-3 axes or a record-time flag into a Fin 16 patch index cites this. It is a pure two-clause definition with a simp attribute; no proof content.
Claim. Define the map $\mathrm{bit}:\{\mathrm{true},\mathrm{false}\}\to\mathbb{N}$ by $\mathrm{bit}(\mathrm{true})=1$ and $\mathrm{bit}(\mathrm{false})=0$.
background
The module freezes world G1 of the order-sensitive gravity plan: it seats a three-cube pattern together with a single record-time bit into the Fin 16 patch. Pattern 3 is a Boolean assignment on three spatial axes. Those three bits, plus the time bit, must be packed as a natural number in ${0,\ldots,15}$.
The conversion here is the elementary bridge from Bool to $\mathbb{N}$. Downstream packing writes weighted sums $b_0+2b_1+4b_2+8t$ with each $b_i$ obtained by this map. The module deliberately avoids the heavy gravity analysis chain; only Mathlib and Patterns are imported.
proof idea
Definition by cases on Bool: true yields 1, false yields 0. Marked @[simp] so later tactics reduce it automatically. No lemmas are applied.
why it matters
Local substrate for the whole seating bijection. seatNat builds the packed index as bitNat(p 0)+2·bitNat(p 1)+4·bitNat(p 2)+8·bitNat(t). bitNat_le_one immediately gives each term at most 1, which feeds the bound used in seat_flipTime. pack4_testBit recovers the four original Booleans by Nat.testBit, confirming the packing is faithful. Together these close the THEOREM half of the module honesty note (bijectivity and the time-bit involution) while the MODEL half treats bit 3 as record time. The construction realises the eight-tick / 2^3 octave structure at the level of a single spatial cube plus one time flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.