edgeCurrentFirstVariation_dirac
plain-language theorem explainer
On the Fin 16 Freudenthal edge lattice, the first variation of the edge-current action against a Dirac probe at a single oriented edge (a,b) collapses to the single term weight(a,b)·sinh(F(a,b)). Anyone comparing order-sensitive history responses of two Loom configs cites this to evaluate the action on a seated generator edge. The proof is a double Finset.sum_eq_single reduction that kills every off-support summand.
Claim. For any real edge weights $w$ and any real edge field $F$ on $\mathrm{Fin}\,16\times\mathrm{Fin}\,16$, and for any oriented edge $(a,b)$, the first variation $\sum_{i,j} w_{ij}\,\sinh(F_{ij})\,V_{ij}$ evaluated at the Dirac probe $V=\delta_{(a,b)}$ equals $w_{ab}\,\sinh(F_{ab})$.
background
The module freezes claims G2/G3 of the Order-Sensitive Gravity proposition: an order-sensitive history response is read from the depth-two commutator content of a Loom config and seated as an antisymmetric Fin 16 edge current on the generator-(0,2) edge (via Q3PatchSeating), with no metric $H$ and no muCoord table.
The local edge-current first variation is the bilinear form $\sum_i\sum_j w_{ij},\sinh(F_{ij}),V_{ij}$, matching the Freudenthal-cover edge-current action. The Dirac probe at $(a,b)$ is the indicator field that is $1$ only on that oriented edge and $0$ elsewhere. The weight $w$ is the standing label-density / class-mass factor used throughout the SevenGaps gravity stack; $F$ is the seated edge field (later specialized to a history response).
Evaluating the variation on a Dirac probe is the standard way to extract the single-edge contribution that will separate two configs.
proof idea
Unfold the first-variation double sum and the Dirac probe. For the outer sum, every row $i\neq a$ has vanishing summands because the indicator forces $i=a$; apply Finset.sum_eq_single at $i=a$. For the remaining inner sum over $j$, every $j\neq b$ likewise vanishes; apply Finset.sum_eq_single at $j=b. The surviving summand is $w_{ab}\,\sinh(F_{ab})\cdot 1$, finished by simp. Off-support zeros use the ordinary real mul_zeroafterif_neg`.
why it matters
This is the evaluation lemma that lets the module fire the edge action on a single seated generator edge. Downstream, edgeAction_separates_cfgAB rewrites both sides with this identity and concludes that the unit-weight first variation of historyResponse cfgA differs from that of historyResponse cfgB on the Dirac probe at seatGen1. That separation is one of the frozen THEOREM claims of the order-sensitive gravity package (G2/G3): action firing that distinguishes the two Loom configs without invoking a linearized flat-patch metric perturbation.
In the broader Recognition gravity stack it sits on the Freudenthal 4D edge image and the Q3 patch seating, converting the depth-two history fingerprint into a concrete real number that can be compared. It does not itself close any of the SevenGaps; it is the local algebraic step those separation theorems need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.