flipTime
plain-language theorem explainer
On the 16-element patch, flipTime toggles the record-time bit and leaves the three spatial Pattern-3 bits fixed. Gravity analysts cite it when relating opposite time slices of a seated three-cube. The body is XOR with 8, with the Fin bound discharged by exhaustive case analysis.
Claim. Define the map $\mathrm{flipTime}:\{0,\ldots,15\}\to\{0,\ldots,15\}$ by $v\mapsto v\oplus 8$. Equivalently, if $v$ is written in four bits with bits $0,1,2$ packing a Pattern-3 configuration and bit $3$ packing record time, flip only the time bit.
background
The module freezes world G1 of the order-sensitive gravity plan: a canonical seating of a three-cube times a Boolean record-time into a $\mathrm{Fin},16$ patch. Pattern 3 is a Boolean labeling of the three spatial axes; those three bits occupy patch positions $0,1,2$, and record time occupies bit $3$.
The seating map packages $(p,t)$ into a single index in ${0,\ldots,15}$. Once seated, the natural time-slice symmetry is bit-flip on the time coordinate alone. XOR with $8=2^3$ is exactly that coordinate flip in the packed representation. The module deliberately avoids the heavy gravity analysis chain; it only supplies the combinatorial seating and its elementary symmetries.
proof idea
Definitional construction, not a tactic proof of a proposition. The value is $\langle v.\mathrm{val}\oplus 8,_\rangle$. The proof obligation is only that the XOR stays strictly below $16$. That bound is obtained by interval_cases on $v.\mathrm{val}$ followed by decide on each of the sixteen concrete residues.
why it matters
flipTime is the concrete generator of the time-slice symmetry on the packed patch. Downstream, flipTime_involutive shows it is an involution, seat_flipTime shows it intertwines with seating via Boolean negation of the time argument, and timeSlice_is_patch_symmetry packages both facts as the official patch-level time symmetry.
In the Recognition framework this sits inside the gravity/holography layer that uses the eight-tick octave (forcing step T7) and three spatial dimensions (T8) as the combinatorial skeleton of a local patch. The honesty note in the module marks bijectivity and the time-bit involution as theorems, while treating the fourth bit as record time remains a modeling choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.