diracProbe
plain-language theorem explainer
Unit impulse on a single directed Fin-16 edge: the map that is 1 at (a,b) and 0 elsewhere. Gravity analysts cite it to extract one-edge first variations of the order-sensitive history current on the Freudenthal patch. The body is the standard Kronecker indicator; no proof content.
Claim. For $a,b \in \{0,\ldots,15\}$, the Dirac probe is the real-valued edge function $\delta_{a,b}$ on $\{0,\ldots,15\}^2$ given by $\delta_{a,b}(i,j)=1$ if $(i,j)=(a,b)$ and $\delta_{a,b}(i,j)=0$ otherwise.
background
The ambient module freezes claims G2/G3 of the order-sensitive gravity proposition: an order-sensitive Loom history is read as a depth-two commutator fingerprint and seated as an antisymmetric Fin-16 edge current on the generator-(0,2) edge (record-time false) via Q3 patch seating. No metric $H$ and no $\mu$-coordinate table enter.
Edge quantities here are real matrices on $\mathrm{Fin},16\times\mathrm{Fin},16$. The history response of a configuration is such a matrix; first variations of edge action are pairings of a weight matrix against $\sinh$ of that response. A Dirac probe is the elementary test function that isolates a single directed edge so the pairing collapses to one entry.
Downstream, the first-variation identity against this probe reduces exactly to $\mathrm{weight}(a,b)\cdot\sinh(F(a,b))$.
proof idea
Pure definition: the two-argument function that returns the real unit when both indices match the fixed pair $(a,b)$, and zero otherwise. No lemmas, no tactics; the body is the indicator of the singleton ${(a,b)}$ in the discrete edge set.
why it matters
Supplies the test edge current used by the first-variation reduction and by the cfgA/cfgB separation theorem in this module. The reduction states that the weighted edge-current first variation of any $F$ against the Dirac probe at $(a,b)$ equals $\mathrm{weight}(a,b)\cdot\sinh(F(a,b))$. The separation theorem then evaluates that identity on the seated generator-(0,2) edge for the two order-distinct histories and obtains unequal real numbers, which is the frozen G2/G3 edge-action firing claim.
Within Recognition gravity analysis this is scaffolding for order-sensitive response, not a metric perturbation: the module honesty note stresses that outside-image scope is not a linearized flat-patch metric mode. It sits downstream of Q3 patch seating and classical source projection imports, and upstream of the concrete cfgA vs cfgB inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.