zero_in_MetricEdgeImage
plain-language theorem explainer
The zero edge-current on the sixteen-site Freudenthal patch lies in the linearized metric edge image: it is the strain current of the zero 4×4 perturbation. Anyone treating that image as a cone, subspace, or admissible set of edge postings would cite this base case. The proof is a direct existential witness with the zero matrix, followed by unfolding the bilinear strain formula and simplifying.
Claim. The identically zero map $F\colon\{0,\ldots,15\}^2\to\mathbb{R}$ lies in the finite linearized metric edge image: there exists a real $4\times 4$ matrix $H$ such that $F(i,j)$ equals the edge strain of $H$ along the integer displacement between patch sites $i$ and $j$ for every pair of sites.
background
This module freezes the linearized flat-patch metric analysis from the Order-Sensitive Gravity plan. Sites are the sixteen vertices of a Freudenthal cover patch (Fin 16). A metric perturbation is a real $4\times 4$ matrix $H$ (Mat4). The edge strain of $H$ along an integer displacement $D\in\mathbb{Z}^4$ is the quadratic form $\sum_{i,j} H_{ij} D_i D_j$, matching the formula used in the Regge exact flat Hessian / Bloch-symbol development.
The strain current of $H$ posts, on each ordered pair of patch sites, the edge strain of $H$ along the binary patch displacement between those sites. The metric edge image is the set of all such strain currents: $F$ is in the image precisely when $F=\mathrm{strainCurrent}(H)$ for some $H$. The module states its honesty scope as linearized flat-patch metric perturbations via that current, with theorems aimed at nontriviality, symmetry, and properness against antisymmetric posting.
proof idea
Existential introduction with the zero matrix as witness. After funext on the two site indices, unfold the definitions of strain current and edge strain. Both are multilinear in $H$, so every summand contains a factor of $H_{ij}=0$; simp closes the identity with the zero edge map.
why it matters
Establishes that the linearized metric edge image is nonempty and contains the null posting. In the module's honesty list this is the trivial base of the image before nontriviality, symmetry, and properness results (siblings such as axis TT-cross membership and strain-current symmetry). Downstream consumers of the image as an admissible set of edge currents can discharge the zero case without reconstructing the strain formula.
The construction is the frozen metric-null fragment of the Order-Sensitive Gravity proposition on the Freudenthal cover. It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law; it supplies the discrete geometric substrate on which those gravity claims are later evaluated. No used_by edges are recorded yet, so the lemma is presently a local completeness fact inside the analysis module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.