edgeCurrentFirstVariation
plain-language theorem explainer
Defines the local edge-current first variation on the Freudenthal Fin-16 patch as the bilinear form ∑∑ w_ij sinh(F_ij) VF_ij. Anyone citing the order-sensitive history response (G2/G3) or the cfgA/cfgB action separation uses this functional. The body is a direct double sum; no proof content.
Claim. For real edge weights $w$, an edge field $F$, and a variation field $VF$ on $\mathrm{Fin}\,16\times\mathrm{Fin}\,16$, the local edge-current first variation is $\sum_{i}\sum_{j} w_{ij}\,\sinh(F_{ij})\,VF_{ij}$.
background
The module freezes claims G2/G3 of the Order-Sensitive Gravity proposition: an order-sensitive Loom history is read as an edge-current response on the Freudenthal cover patch. The reading is a depth-two commutator fingerprint (the same second-order content isolated by pair-traces / pair-sum holonomy expansion), seated as an antisymmetric Fin-16 edge current on the generator-(0,2) edge at record-time false via Q3 patch seating. No metric $H$ and no $\mu$-coordinate table enter.
The three arguments are edge-indexed real matrices: a weight $w$, a seated field $F$ (the history response), and a probe variation $VF$. The hyperbolic factor $\sinh(F_{ij})$ is the natural linear response of a cosh-type edge action (cf. the sourced-minimizer remainder $F(s,h)=\cosh(s+h)-\cosh s-\sinh s\cdot h-h^2/2$). The doc-comment ties the formula to FreudenthalCoverEdgeCurrentAction4D.
proof idea
Pure definition: unfold to the double sum $\sum_i\sum_j w_{ij}\sinh(F_{ij}),VF_{ij}$ over the Fin-16 universe. No lemmas, no tactics. Downstream, the Dirac specialization collapses the sum to the single term $w_{ab}\sinh(F_{ab})$ by killing all off-support indices.
why it matters
This is the scalar observable that turns a seated antisymmetric history response into a numerical first variation. It is the quantity compared in edgeAction_separates_cfgAB, which proves the variation on unit weight against a Dirac probe at seatGen1 distinguishes cfgA from cfgB. The companion lemma edgeCurrentFirstVariation_dirac is the computational reduction used there.
In the Recognition gravity stack this sits under the order-sensitive history → edge-current response program on the Freudenthal patch: THEOREM-grade separation and metric-image exclusion for cfgA/cfgB, while the physical-current reading of the depth-two fingerprint remains MODEL-grade. It does not invoke the T0–T8 forcing chain directly; it is local analysis infrastructure for the holography/gravity interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.