antisymEdge_rev
plain-language theorem explainer
Evaluating the antisymmetric Fin-16 edge current seeded on the ordered pair (a,b) at the reverse pair (b,a) returns the negated amplitude. Gravity analysts working the order-sensitive history response on the Freudenthal patch cite this when flipping generator edges. The proof is a one-line unfold-and-simp of the piecewise definition under a ≠ b.
Claim. For indices $a,b\in\{0,\ldots,15\}$ with $a\neq b$ and amplitude $\mathrm{amp}\in\mathbb{R}$, the antisymmetric edge map that places $\mathrm{amp}$ on $(a,b)$ and $-\mathrm{amp}$ on $(b,a)$ evaluates to $-\mathrm{amp}$ at the ordered pair $(b,a)$.
background
The module builds an order-sensitive history response as an antisymmetric edge current on the Freudenthal Fin-16 patch (frozen claims G2/G3). The response is read from the depth-two commutator content of a Loom configuration and seated on the generator-(0,2) edge at record-time false via Q3 patch seating; no metric $H$ and no $\mu$-coordinate table enter.
The supporting map places a real amplitude on a directed pair and its negative on the reverse pair, and zero elsewhere: $$\mathrm{edge}(i,j)=\begin{cases}\mathrm{amp}&i=a,,j=b\-\mathrm{amp}&i=b,,j=a\0&\text{otherwise.}\end{cases}$$ The present lemma is the reverse-pair evaluation of that map. A sibling forward lemma records the matching $(a,b)\mapsto\mathrm{amp}$ fact.
proof idea
One-line wrapper: unfold the piecewise edge definition, then simp with the hypothesis $a\neq b$ and its symmetric form Ne.symm. The second branch of the definition fires and returns $-\mathrm{amp}$; the first branch is blocked by the inequality.
why it matters
Feeds the reverse history-response theorem in the same module, which states that the history response on the swapped generator-1 endpoints equals the negated depth-two fingerprint amplitude of the configuration. That parent unfolds the history-response seating and applies this reverse-edge identity together with the generator-pair inequality.
In the broader Recognition gravity stack this is bookkeeping for the antisymmetric Fin-16 edge current that carries the order-sensitive (depth-two commutator) reading. It supports the G2/G3 frozen claims of the order-sensitive gravity proposition: separation and action firing on the patch, without claiming a linearized flat-patch metric perturbation. The modeling step that treats the fingerprint amplitude as a physical current remains explicit and outside the proved core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.