patchDisp_symm
plain-language theorem explainer
Antisymmetry of the four-component patch displacement on the sixteen-site Freudenthal cover: swapping the two endpoints negates every coordinate difference. Gravity analysts characterizing the linearized metric edge image cite it when proving strain-current symmetry. The proof is a one-line simp that unfolds the difference definition and rewrites subtraction via add-comm.
Claim. For all sites $i,j$ among the sixteen Freudenthal patch sites and every axis $\mu\in\{0,1,2,3\}$, the integer patch displacement satisfies $\mathrm{disp}(j,i)_\mu=-\mathrm{disp}(i,j)_\mu$.
background
This module freezes the linearized flat-patch metric picture from the Order-Sensitive Gravity plan: a four-by-four integer matrix $H$ posts a strain current on the sixteen-site Freudenthal cover, and MetricEdgeImage is the set of all such currents. Coordinates on the patch are binary four-tuples (patchSite), so each directed pair of sites has an integer four-vector of coordinate differences.
That four-vector is the patch displacement: $\mathrm{disp}(i,j)_\mu$ is the $\mu$-component of site $j$ minus site $i$. Edge strain is built from these displacements contracted against $H$, matching the Regge/Bloch Hessian symbol used elsewhere in the gravity chain. The present lemma records the elementary antisymmetry of those differences before strain is formed.
The ambient arithmetic is ordinary integer subtraction; the simp proof only needs commutativity of addition (available from several foundation layers) and the rewrite of subtraction as add-of-negate.
proof idea
One-line wrapper. Unfold patchDisp to the raw site-coordinate difference, rewrite subtraction as addition of a negation (sub_eq_add_neg), then apply add_comm so the two orderings become literal negatives of each other. No case split on sites or axes is required.
why it matters
Immediate parent is strainCurrent_symm, which lifts this sign flip through the edge-strain formula (via edgeStrain_neg) to conclude that the strain current of any Mat4 perturbation is symmetric in its two site arguments. That symmetry is one of the three honesty bullets of the module: nontriviality, symmetry, and properness of the linearized edge image against antisymmetric posting.
In the broader RS gravity stack this sits inside the finite Freudenthal-patch model of metric perturbations (flat-patch, linearized), not the full curved or nonlinear theory. It is bookkeeping that keeps the edge-image characterization well-defined and undirected, so later properness and image theorems can treat edges without orientation artifacts. No forcing-chain landmark (T5–T8, RCL, phi) is touched directly; the lemma is pure discrete geometry on the 16-site cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.