IndisputableMonolith.Gravity.Analysis.Q3PatchSeating
Four binary coordinates on a Q3 (Freudenthal) patch are packed into a single natural number and recovered bit-wise. Gravity analysts cite the seating maps when an order-sensitive Loom history must be written as an edge-current response on the patch. The module is mostly definitional: seat/unseat are mutual inverses, with injectivity and surjectivity proved by bit arithmetic.
claimFour bits $b_0,b_1,b_2,b_3\in\{0,1\}$ pack into a natural $n=\sum_{i=0}^{3}b_i\,2^i$ with $n<16$. The seating map $\mathrm{seat}$ and its inverse $\mathrm{unseat}$ are mutual inverses; $\mathrm{seat}$ is bijective onto its image. Bit extraction recovers each coordinate: $\mathrm{testBit}(n,i)=b_i$.
background
Recognition Science gravity analysis on the Freudenthal (Q3) patch needs a discrete address for four binary degrees of freedom: three spatial edge choices plus a time-orientation flip. The module introduces bitNat (a bit as a natural in ${0,1}$), seatNat (the packed address, strictly less than $16$), and the pair seat / unseat that convert between a 4-tuple of bits and that address.
A companion flipTime toggles the temporal bit inside the packed word. The local setting is pure combinatorial packing: no metric or curvature is assumed here. Upstream material is only the Patterns import (shared bit and pattern utilities). Downstream, the same seating is how an order-sensitive Loom Config is written onto patch edges for the G2/G3 frozen claims.
proof idea
Definitional core: seat packs four bits by weighted powers of two; unseat reads them back with testBit. Round-trip lemmas seat_unseat and unseat_seat are bit-arithmetic identities. Injectivity of seat follows from the round-trip; surjectivity onto the image ${0,\ldots,15}$ is by exhaustive recovery of bits. Bounds bitNat_le_one and seatNat_lt are immediate from the constructors. pack4_testBit records that each extracted bit matches the original coordinate. No deep tactics: mostly rfl, omega, and testBit simp lemmas.
why it matters in Recognition Science
This module is the discrete addressing layer for order-sensitive gravity on the Q3 patch. It is imported by OrderSensitiveHistoryResponse4D, which freezes claims G2/G3 of the Order-Sensitive Gravity proposition: the depth-two commutator reading of a Loom configuration is seated as an edge-current response on the Freudenthal patch. The audit module Q3PatchSeatingAudit re-exports the same API for axiom hygiene.
In the broader RS chain the eight-tick octave (T7) and $D=3$ (T8) already fix a $2^3$ spatial tick structure; packing one extra time-orientation bit yields the 4-bit word used here. Without bijective seating, the history-to-current map could not be stated as a function on naturals.
scope and limits
- Does not define metric, curvature, or continuum gravity on the patch.
- Does not prove dynamical response equations; only the bit packing bijection.
- Does not seat histories longer than four bits or addresses outside $0..15$.
- Does not discharge G2/G3; those live in OrderSensitiveHistoryResponse4D.
- Does not depend on J-cost, phi-ladder, or mass formulae.
used by (2)
depends on (1)
declarations in this module (18)
-
def
bitNat -
theorem
bitNat_le_one -
def
seatNat -
theorem
seatNat_lt -
def
seat -
def
unseat -
def
flipTime -
theorem
seat_unseat -
theorem
pack4_testBit -
theorem
unseat_seat -
theorem
seat_injective -
theorem
seat_surjective -
theorem
seat_bijective -
theorem
xor8_lt_eight -
theorem
xor8_add_eight -
theorem
seat_flipTime -
theorem
flipTime_involutive -
theorem
timeSlice_is_patch_symmetry