patchDisp_zero_twelve
plain-language theorem explainer
The displacement from site 0 to site 12 on the sixteen-site Freudenthal patch is the integer 4-vector (0,0,1,1). Gravity analysts evaluating linearized strain currents on fixed edges cite this evaluation. The proof is function extensionality followed by a four-way finite case split, each reducing by definitional equality.
Claim. On the sixteen-site Freudenthal patch, the coordinate-wise displacement from site $0$ to site $12$ equals the map sending $\mu\in\{0,1,2,3\}$ to $(0,0,1,1)_\mu$ in $\mathbb{Z}$.
background
This module freezes the linearized flat-patch metric edge image used in the Order-Sensitive Gravity proposition. A Mat4 perturbation on the sixteen-site patch induces a strain current on oriented edges; MetricEdgeImage F means $F$ arises that way. The strain formula and binary patch coordinates match the Freudenthal cover ledger graph, reproduced locally to avoid the heavy analysis import chain.
Displacement between sites is the integer 4-vector $\mathrm{patchDisp}(i,j)(\mu)=\mathrm{patchSite}(j,\mu)-\mathrm{patchSite}(i,\mu)$. Edge strain is built from that displacement contracted against the perturbation, and the strain current is the resulting edge-supported integer. The present lemma evaluates one concrete displacement that appears in the axis TT-cross current.
proof idea
Term-mode proof. Apply function extensionality in the coordinate index $\mu:\mathrm{Fin},4$. Split into the four cases $\mu=0,1,2,3$ via fin_cases; each residual goal is definitional equality against the match expression and closes by rfl. No external lemmas are required beyond the definition of patch displacement.
why it matters
Feeds the immediate parent strainCurrent_axisTTCross_zero_twelve, which unfolds the strain current of the axis TT-cross perturbation on the edge $(0,12)$, rewrites by this evaluation, and obtains the integer value $2$ after a four-term sum. That parent is part of the module's nontriviality and image-membership facts for MetricEdgeImage: showing concrete nonzero strain currents of admissible perturbations. In the broader RS gravity chain this sits inside the linearized Freudenthal-patch analysis that underwrites the frozen world-metric-null of the Order-Sensitive Gravity proposition, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.