antisymEdge
plain-language theorem explainer
Builds the elementary antisymmetric edge current on the Fin-16 Freudenthal patch: amplitude amp on ordered pair (a,b), minus amp on (b,a), zero elsewhere. Gravity analysts cite it when seating a depth-two Loom fingerprint as a physical edge current without a metric. The body is a pure piecewise definition, no proof obligations.
Claim. For endpoints $a,b\in\mathrm{Fin}\,16$ and amplitude $\mathrm{amp}\in\mathbb{R}$, define the map $K:\mathrm{Fin}\,16\times\mathrm{Fin}\,16\to\mathbb{R}$ by $K(i,j)=\mathrm{amp}$ if $(i,j)=(a,b)$, $K(i,j)=-\mathrm{amp}$ if $(i,j)=(b,a)$, and $K(i,j)=0$ otherwise.
background
The module freezes claims G2/G3 of the Order-Sensitive Gravity proposition: an order-sensitive history response is read as an edge current on the Freudenthal patch (Fin 16), not as a linearized metric perturbation. The reading comes from the depth-two commutator content of a Loom Config (the same second-order data isolated by pairTraces / pairSum), seated on the generator-(0,2) edge at record-time false via Q3PatchSeating.
An antisymmetric edge current is the minimal object that can carry a directed amplitude between two vertices while remaining skew under swap. Here the support is a single unordered pair ${a,b}$, with opposite signs on the two orientations. Upstream, Generator is any positive real other than 1 (existence from the Law of Logic); time on a ledger state is the constant 0 in this foundation layer, so the seating is at the false/record-time-zero slice rather than a dynamical clock.
proof idea
Definitional, not a theorem. The body is a single lambda with two nested if-then-else branches: match the forward ordered pair to amp, the reverse ordered pair to -amp, and default to 0. Downstream lemmas antisymEdge_fwd and antisymEdge_rev simply unfold this definition and simplify under a ≠ b.
why it matters
This is the atomic seating map for the history response. historyResponse applies it at seatGen1 (the generator-1 endpoints (0,2) at record-time false) with amplitude equal to the real cast of the depth-two list fingerprint of a Config. The forward/reverse evaluation lemmas then certify that the seated current really carries +amp and -amp on those two orientations.
In the Recognition gravity stack this is the MODEL step that treats the depth-two fingerprint amplitude as a physical current: no metric H, no muCoord table, and explicitly outside the image of a linearized flat-patch metric perturbation. It feeds the order-sensitive edge-current story on the Freudenthal patch without claiming a full Einstein-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.