pack4_testBit
plain-language theorem explainer
Packing four Booleans into a natural number via powers of two recovers each bit under Nat.testBit. Gravity analysts cite it when seating a 3-cube pattern plus a record-time flag into a Fin 16 patch index. The proof is a finite case split: revert the four bits and decide.
Claim. For any four Booleans $b_0,b_1,b_2,b_3$, if $n = [b_0] + 2[b_1] + 4[b_2] + 8[b_3]$ where $[\mathrm{true}]=1$ and $[\mathrm{false}]=0$, then $n.\mathrm{testBit}\,i = b_i$ for each $i\in\{0,1,2,3\}$.
background
The module freezes world G1 of the order-sensitive gravity plan: it seats a Pattern 3 (three Boolean axes of a cube) together with a record-time bit into a single Fin 16 patch index, without pulling in the heavy gravity analysis chain.
bitNat is the standard Bool-to-Nat embedding (true maps to 1, false to 0). The packing $n = b_0 + 2b_1 + 4b_2 + 8b_3$ is the usual binary place-value encoding of four bits; Nat.testBit i reads the coefficient of $2^i$.
Downstream seating maps use this recovery identity to prove that unseating after seating returns the original pattern and time flag.
proof idea
Pure finite exhaustion. Revert the four Boolean parameters so the goal is a closed proposition over Bool^4, then decide discharges all 16 cases by computation. No algebraic lemmas beyond the definition of bitNat and the kernel's evaluation of testBit on small naturals.
why it matters
Local lemma for the Fin 16 seating bijection. It is the only nontrivial arithmetic step inside unseat_seat, which states that unseating after seating recovers (p, t) for a Pattern 3 and a time bit. That round-trip, together with the dual seat_unseat, underwrites the THEOREM half of the module honesty note: bijectivity of the three-cube × record-time packing into the 16-cell patch. The MODEL half (treating bit 3 as record time) is interpretive and sits outside this lemma. In the broader RS gravity story the patch is the discrete carrier for order-sensitive holography; this fact just guarantees the bit packing is lossless.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.