patchDisp
plain-language theorem explainer
The displacement between two of the sixteen Freudenthal patch sites is the integer 4-vector of binary hypercube coordinate differences. Gravity analysts cite it when assembling the linearized strain current on patch edges. The body is a one-line componentwise difference of site coordinates, matching the displacement argument of the Regge flat-Hessian edge strain.
Claim. For sites $i,j\in\{0,\ldots,15\}$, the patch displacement is the map $\mu\mapsto s(j)_\mu-s(i)_\mu$, where $s(v)\in\mathbb{Z}^4$ is the binary coordinate of site $v$ on the unit 4-cube (bit extraction of $v$ along each axis $\mu=0,1,2,3$).
background
This module freezes the finite linearized metric edge image on the Freudenthal sixteen-site patch: a 4-cube whose vertices are labeled by Fin 16, with binary coordinates extracted bit-by-bit. The site map sends each vertex $v$ to $(v\bmod 2,\lfloor v/2\rfloor\bmod 2,\lfloor v/4\rfloor\bmod 2,\lfloor v/8\rfloor\bmod 2)\in\mathbb{Z}^4$.
Edge strain of a symmetric $4\times 4$ metric perturbation $H$ against a displacement $D:\mathrm{Fin},4\to\mathbb{Z}$ is the quadratic form $\sum_{i,j} H_{ij} D_i D_j$, copied from the Regge exact flat Hessian Bloch-symbol development so this file stays light.
The local setting is linearized flat-patch metric perturbations: an edge image is whatever arises as the strain current of some $H$ on all ordered pairs of patch sites.
proof idea
Pure definition: for each axis $\mu$, return the integer difference of the two sites' binary coordinates. No lemmas; the body is the anonymous function $\mu\mapsto s(j)\mu-s(i)\mu$.
why it matters
This displacement is the bridge from discrete patch geometry to continuum-style strain. Downstream, the strain current is defined by feeding it into edge strain: $F_H(i,j)=\mathrm{edgeStrain}(H,\mathrm{patchDisp}(i,j))$. Symmetry lemmas (patchDisp_symm, then strainCurrent_symm via the oddness of edge strain under $D\mapsto -D$) and the explicit zero-to-twelve displacement check rest on it.
In the frozen Order-Sensitive Gravity plan, MetricEdgeImage F means $F$ is exactly such a strain current. The definition therefore sits at the base of the nontriviality, symmetry, and properness theorems against antisymmetric posting on the patch, without importing the heavy analysis chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.