elementaryPosting_not_in_MetricEdgeImage
plain-language theorem explainer
An elementary double-entry posting between patch sites 0 and 4 cannot arise as the strain current of any 4×4 metric perturbation. Gravity analysts cite this as the properness check that metric edge currents are symmetric while recognition postings are antisymmetric. The proof assumes membership, equates the (0,4) and (4,0) entries via strain symmetry, then contradicts antisymmetry plus the unit value at (0,4).
Claim. The elementary posting from site $0$ to site $4$ on the sixteen-site Freudenthal patch does not lie in the metric edge image: there is no $4\times 4$ real matrix $H$ such that the strain current of $H$ equals that posting.
background
This module studies the finite linearized metric edge image on the sixteen-site Freudenthal patch. A matrix-valued edge field $F:\mathrm{Fin},16\to\mathrm{Fin},16\to\mathbb{R}$ lies in the metric edge image when $F$ equals the strain current of some $4\times 4$ perturbation $H$ (a linearized flat-patch metric deformation). The strain formula and binary patch coordinates match the heavier Freudenthal cover analysis, reproduced here in isolation.
An elementary posting from account $a$ to $b$ is the double-entry current with $+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere. It is built from postings, not from a potential. Strain currents are symmetric in the two edge endpoints; elementary postings are antisymmetric. The module's honesty clause flags nontriviality, symmetry, and properness against antisymmetric posting as the theorems of record.
proof idea
Assume for contradiction that some $H$ has strain current equal to the elementary posting from $0$ to $4$. Symmetry of the strain current equates the $(0,4)$ and $(4,0)$ entries. Evaluating the assumed equality at those two ordered pairs therefore forces the posting values at $(0,4)$ and $(4,0)$ to agree. Antisymmetry of elementary postings identifies the $(4,0)$ value with the negative of the $(0,4)$ value, and the dedicated nonzero lemma gives the $(0,4)$ entry as $1$. The resulting identity $1=-1$ is discharged by linarith.
why it matters
In the frozen world-metric-null plan for order-sensitive gravity, metric edge currents must be proper against pure recognition postings: a linearized metric perturbation cannot manufacture a single double-entry event. This theorem is that properness statement for the concrete edge $(0,4)$ on the sixteen-site patch. It sits beside the sibling facts that strain currents are symmetric and that certain axis TT-cross patterns do lie in the image, separating potential-derived strain from ledger postings. No downstream consumer is wired yet; the result closes the local honesty bullet on antisymmetric posting and keeps the finite 4D edge-image analysis self-contained without importing the full holography chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.