elementaryPosting_zero_four_nonzero
plain-language theorem explainer
The elementary double-entry posting from site 0 to site 4 on the sixteen-site Freudenthal patch equals +1 at the ordered pair (0,4). Gravity analysts cite this when separating antisymmetric recognition currents from linearized metric strain. The proof unfolds the posting definition and simplifies the indicator arithmetic.
Claim. Let $P$ be the elementary recognition posting from account $0$ to account $4$ on $\mathrm{Fin}\,16$ (value $+1$ on the ordered pair $(0,4)$, $-1$ on $(4,0)$, and $0$ elsewhere). Then $P(0,4)=1$.
background
This module studies the finite linearized metric edge image on the sixteen-site Freudenthal patch. A matrix-valued field $F$ lies in the metric edge image when it equals the strain current of some $4\times 4$ metric perturbation on the patch; the strain formula and binary patch coordinates match the Freudenthal cover ledger graph, reproduced locally to avoid the heavy analysis import chain.
The elementary posting is the double-entry current of one recognition event from account $a$ to account $b$: it places $+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere. It is built from postings, not from a potential. The present lemma evaluates that kernel at a concrete ordered pair on the $16$-site patch.
proof idea
Term-mode style via two tactics: unfold the definition of the elementary posting, then simp discharges the indicator arithmetic. With $a=0$, $b=4$, and evaluation at $(i,j)=(0,4)$, the first indicator is true and the second is false, so the difference collapses to $1-0=1$.
why it matters
The lemma supplies the concrete nonzero value needed by elementaryPosting_not_in_MetricEdgeImage, which proves that this antisymmetric posting is not the strain current of any linearized metric perturbation. That parent theorem is part of the module's honesty package: nontriviality and properness of the metric edge image against antisymmetric postings. In the frozen Order-Sensitive Gravity plan, the distinction separates recognition ledger currents from metric-null strain on the Freudenthal patch, keeping the linearized flat-patch scope clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.