antisymEdge_fwd
plain-language theorem explainer
On the Fin-16 Freudenthal edge lattice, the antisymmetric edge current seeded by amplitude amp at ordered pair (a,b) evaluates to amp when read at that same forward pair (provided a eq b). Gravity analysts working the order-sensitive history response (G2/G3) cite this to pin the forward seating of a depth-two fingerprint. The proof is a one-line unfold-and-simp of the piecewise definition.
Claim. Let $a,b\in\mathrm{Fin}\,16$ with $a\neq b$, and let $\mathrm{amp}\in\mathbb{R}$. Define the antisymmetric edge map $E_{a,b}^{\mathrm{amp}}:\mathrm{Fin}\,16\times\mathrm{Fin}\,16\to\mathbb{R}$ by $E(i,j)=\mathrm{amp}$ if $(i,j)=(a,b)$, $-\mathrm{amp}$ if $(i,j)=(b,a)$, and $0$ otherwise. Then $E_{a,b}^{\mathrm{amp}}(a,b)=\mathrm{amp}$.
background
The module builds an order-sensitive history response as an edge current on the Freudenthal patch (Fin 16 vertices). Frozen claims G2/G3 of the Order-Sensitive Gravity proposition seat a depth-two commutator reading of a Loom Config as an antisymmetric current on the generator-(0,2) edge, with no metric $H$ and no muCoord table.
The local primitive is the piecewise map that places amplitude amp on the ordered pair $(a,b)$, minus amp on the reverse pair $(b,a)$, and zero elsewhere. That construction is the only upstream dependency. The $a\neq b$ hypothesis keeps the two branches disjoint so the forward evaluation is unambiguous.
proof idea
One-line wrapper: unfold the piecewise definition of the antisymmetric edge map, then simp with the hypothesis $a\neq b$. The first branch fires and returns amp; the reverse branch is excluded by inequality.
why it matters
Feeds the forward evaluation of the history response: historyResponse_fwd unfolds the response and applies this lemma at the seated generator pair (with the generator inequality) to recover the depth-two fingerprint amplitude as a real. That pins the MODEL step of treating the fingerprint as a physical edge current on the Freudenthal patch, which is the concrete content of frozen claims G2/G3. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is local gravity-analysis scaffolding for the order-sensitive reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.