patchSite
plain-language theorem explainer
Binary coordinates of a vertex on the unit 4-cube. Given site index v in {0,...,15} and axis μ in {0,1,2,3}, returns the μ-th bit of v as an integer 0 or 1. Displacement and strain formulas on the Freudenthal patch cite this as the discrete site embedding. Pure bit extraction by successive division and mod 2.
Claim. For each vertex $v \in \{0,\ldots,15\}$ and coordinate direction $\mu \in \{0,1,2,3\}$, the site coordinate is the $\mu$-th binary digit of $v$, valued in $\{0,1\} \subset \mathbb{Z}$: namely $\lfloor v / 2^\mu \rfloor \bmod 2$.
background
The module studies the finite linearized metric edge image on the Freudenthal patch: sixteen sites of the unit hypercube in 4D, indexed by Fin 16, with spacetime axes indexed by Fin 4. A Mat4 is a real 4×4 matrix (linearized metric perturbation). The module freezes the world metric-null of the order-sensitive gravity proposition and reproduces the strain formula and binary patch coordinates from the Freudenthal cover edge-current action, without importing the heavy analysis chain.
MetricEdgeImage F means F is the strain current of some Mat4 perturbation on this sixteen-site patch. Site labels must be unpacked into hypercube coordinates before displacements and edge strains can be formed. This definition is that unpacking: each vertex index is read as a 4-bit string in {0,1}^4.
proof idea
Definition by cases on the axis μ. Case μ = k returns the k-th bit of v.val: integer-divide by 2^k, reduce mod 2, cast ℕ → ℤ. No lemmas, no tactics; pure pattern match on Fin 4.
why it matters
Feeds patchDisp, which is the integer displacement between two sites as the difference of binary coordinates along each axis. That displacement enters edgeStrain and strainCurrent, which define MetricEdgeImage: the set of strain currents arising from Mat4 perturbations on the patch. Symmetry and nontriviality theorems in the same module (edgeStrain_neg, patchDisp_symm, strainCurrent_symm, axisTTCross_in_MetricEdgeImage) rest on this coordinate convention matching the Freudenthal cover ledger graph.
In the broader RS gravity stack this is the discrete geometry of the 4D unit hypercube (16 = 2^4 sites), the local patch on which linearized metric edge currents are classified. It is combinatorial scaffolding for the strain-current image, not a dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.