xor8_add_eight
plain-language theorem explainer
For every natural number n below 8, adding 8 and then bitwise-XOR with 8 recovers n. Analysts of the Fin-16 gravity patch seating cite it when relating packed seats that differ only in the record-time bit. The proof is a one-line exhaustive split on the eight admissible values of n.
Claim. If $n\in\mathbb{N}$ satisfies $n<8$, then $(n+8)\oplus 8=n$, where $\oplus$ is bitwise exclusive-or on natural numbers.
background
The module freezes world G1 of the order-sensitive gravity holography plan. It packs a Pattern-3 configuration (three Boolean axes) into bits 0,1,2 of a value in Fin 16, and packs a Boolean record-time flag into bit 3. The three-bit packing is therefore a natural number in ${0,\ldots,7}$.
Adding 8 sets bit 3; XOR with 8 toggles that same pure power-of-two bit. The identity records that, after the time bit has been set by addition, XOR-ing it off restores the original three-bit packing. The module treats the fourth bit as record time by model choice and proves bijectivity plus the time-bit involution as theorems, without importing the heavy gravity analysis chain.
proof idea
One-line wrapper around Mathlib's finite-range tactics. interval_cases n splits the hypothesis $n<8$ into the eight concrete goals $n=0,\ldots,7$; each residual equality is closed by decide, which evaluates the concrete XOR arithmetic.
why it matters
Feeds the sibling theorem seat_flipTime, which states that seating a Pattern 3 with the negated time bit equals applying the flipTime map to the seated pair. That identity is part of the module's THEOREM layer (bijectivity and the time-bit involution) for the canonical three-cube × record-time seating into the Fin 16 patch. It supports the frozen G1 world of the order-sensitive gravity proposition without pulling in the full gravity analysis stack. Framework-wise it is local arithmetic scaffolding for the patch model, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.