MetricEdgeImage
plain-language theorem explainer
A 16×16 real edge field lies in the finite linearized metric edge image exactly when it equals the strain current of some 4×4 metric perturbation on the Freudenthal patch. Gravity analysts cite it to separate genuine linearized metric responses from order-sensitive ledger residuals. The body is a pure existential: membership means F is strainCurrent of some Mat4.
Claim. A map $F:\{0,\ldots,15\}^2\to\mathbb{R}$ lies in the finite linearized metric edge image if and only if there exists a $4\times 4$ real matrix $H$ such that $F$ equals the strain current of $H$ on the sixteen-site Freudenthal patch.
background
The module freezes the world metric-null of the Order-Sensitive Gravity proposition on a sixteen-site Freudenthal patch. Coordinates and the strain formula are reproduced locally so the analysis does not pull the heavy cover-ledger chain.
A Mat4 is a $4\times 4$ real matrix standing for a linearized flat-patch metric perturbation. Edge strain of such an $H$ along a patch displacement yields a scalar; the strain current packages those scalars into a full $16\times 16$ edge field via the binary patch coordinates.
The shifted cost $H(x)=J(x)+1$ from the Recognition Composition Law appears only as ambient cost algebra; the edge image itself is pure linear strain geometry on the patch.
proof idea
Definition, not a proved theorem. The body is the single existential proposition: there exists a Mat4 whose strain current equals the given edge field F. No tactics or lemmas fire at the definition site; downstream theorems discharge or refute the existential by exhibiting a witness Mat4 or by symmetry contradictions.
why it matters
This predicate is the finite-stage gate for the order-sensitive gravity program. Downstream, zero and the axis TT-cross strain current sit inside the image, while elementary antisymmetric postings and the cfgA/cfgB response difference sit outside. ContinuumOrderSensitiveResidual4D imports the outside-image fact as the finite stage of G3 and records that exclusion alone does not flip continuumPromotionEarned. The module honesty block lists nontriviality, symmetry, and properness against antisymmetric posting as the theorems this definition supports. It is the linearized flat-patch metric null against which ledger residuals are measured, not a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.