bitNat_le_one
plain-language theorem explainer
Any Boolean bit, encoded as 0 or 1 in the naturals, is at most 1. Gravity seating arguments cite this bound when packing three Pattern-3 axes plus a record-time bit into a Fin 16 index. The proof is a two-case split on the Boolean with simplification of the encoding.
Claim. For every Boolean $b$, the natural number that sends $\mathrm{true}\mapsto 1$ and $\mathrm{false}\mapsto 0$ is at most $1$.
background
The module freezes world G1 of the order-sensitive gravity plan: it seats a three-axis Pattern into patch bits 0,1,2 and a record-time Boolean into bit 3, yielding an element of $\mathrm{Fin},16$. It proves bijectivity and the time-bit involution without importing the heavy gravity analysis chain.
The local encoding bitNat is the standard map $\mathrm{Bool}\to\mathbb{N}$ with $\mathrm{true}\mapsto 1$ and $\mathrm{false}\mapsto 0$. Downstream seating sums weighted copies of these values (coefficients $1,2,4,8$), so a uniform upper bound of 1 on each term is the elementary inequality needed before any Fin-bound or flip identity.
proof idea
One-line wrapper: case-split on the Boolean, then simplify each branch against the definition of the encoding. The true branch gives $1\le 1$; the false branch gives $0\le 1$. No external lemmas are required.
why it matters
The bound is the arithmetic fuel for the seating layer. seatNat_lt applies it four times (three pattern axes and the time bit) to prove the packed natural is strictly less than 16, so the seat lands in $\mathrm{Fin},16$. seat_flipTime reuses the same three axis bounds to show that flipping the time bit commutes with seating, i.e. the fourth bit is a pure involution on the patch.
Those two facts are the THEOREM half of the module honesty note (bijectivity and the time-bit involution). They sit under the Recognition gravity program that packs the eight-tick / three-cube structure into a 16-cell holographic patch, without yet touching the full forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.