responseDiff
plain-language theorem explainer
Pointwise difference of two depth-two history responses, valued as real Fin-16 edge currents. Gravity residual and continuum-promotion arguments cite it whenever two Loom configurations (typically cfgA and cfgB) must be compared on the Freudenthal patch. The body is a one-line subtraction of the already-seated antisymmetric responses.
Claim. For two configurations $c_1,c_2$, the response difference is the map $\mathrm{Fin}\,16\times\mathrm{Fin}\,16\to\mathbb{R}$ given by pointwise subtraction of their history responses: $(i,j)\mapsto R(c_1)(i,j)-R(c_2)(i,j)$, where each $R(c)$ is the antisymmetric edge current obtained by seating the depth-two fingerprint of $c$ on the generator-$(0,2)$ edge.
background
The module freezes claims G2/G3 of the Order-Sensitive Gravity proposition: an order-sensitive history reading becomes an edge-current response on the Freudenthal patch. No metric $H$ and no $\mu$-coordinate table enter.
A Loom configuration is a finite list of closed walks at a shared basepoint. Its depth-two reading yields a fingerprint amplitude; historyResponse seats that amplitude as an antisymmetric real current on $\mathrm{Fin},16\times\mathrm{Fin},16$ along the fixed generator-$(0,2)$ edge (via the Q3 patch seating). The present definition simply compares two such seated currents.
Upstream, the single-edge complex and the multi-distinction geometry supply the combinatorial skeleton; the history response already packages the depth-two commutator content that Core pair-traces isolate.
proof idea
Definitional one-liner: the function $(i,j)\mapsto$ history-response of $c_1$ at $(i,j)$ minus history-response of $c_2$ at $(i,j)$. No lemmas, no tactics; pure pointwise subtraction of two already-constructed $\mathrm{Fin},16$ edge currents.
why it matters
This difference is the finite-stage residual that continuum residual analysis consumes. Downstream, RefinementFamily stores a sequence of such differences; normalizedSeparation, MetricCollapse, and LatticeWashout are defined in terms of their edge norms and metric projections. The concrete pair cfgA/cfgB is shown outside the metric edge image (responseDiff_cfgAB_not_in_MetricEdgeImage, re-exported as finite_outside_metric_image), and the methodological wall finite_exclusion_does_not_earn_promotion records that this finite outside-image fact does not flip continuum promotion.
In the Recognition gravity stack it is the discrete carrier of order-sensitive residual content before any continuum limit: the object on which G3 (metric-image exclusion) is stated, and against which washout versus surviving-sector terminals are later judged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.