responseDiff_fwd
plain-language theorem explainer
The edge-current response difference between certificate configs A and B at the generator-(0,2) seat equals the difference of their depth-two fingerprint amplitudes (as reals). Gravity analysts working the order-sensitive history response on the Freudenthal patch cite this identity. Proof is a one-line simp unfolding the difference and applying the forward history-response evaluation at that seat.
Claim. For the two Loom certificate configurations $A$ and $B$, the response difference at the seated generator-$(0,2)$ edge endpoints equals $\mathrm{fp}(R_2(A))-\mathrm{fp}(R_2(B))$ in $\mathbb{R}$, where $R_2$ is the depth-two commutator (pair-trace) reading of a config and $\mathrm{fp}$ is the base-17 polynomial fingerprint of a natural-number list.
background
This module freezes claims G2/G3 of the order-sensitive gravity proposition: an order-sensitive history is turned into an edge-current response on the Freudenthal patch. The response is built from the depth-two commutator reading of a Loom config (the same second-order content isolated by pair-traces / pair-sums), seated as an antisymmetric Fin-16 edge current on the generator-(0,2) edge at record-time false. No metric $H$ and no $\mu$-coordinate table enter.
The depth-two reading extracts the recognition residual (not a classical source) as a list of naturals. Its polynomial fingerprint folds the list with multiplier 17. History response at a seated edge is that fingerprint cast to $\mathbb{R}$ when the edge is the forward generator-1 seat; the response difference of two configs is the pointwise difference of those history responses. The forward evaluation theorem already states that history response of any config at that seat equals the real fingerprint of its depth-two reading.
proof idea
One-line wrapper. Unfold the response-difference definition (difference of history responses) and simplify with the forward history-response theorem at the generator-1 seat. That theorem reduces each history response to the real-cast list fingerprint of the corresponding depth-two reading, so the difference collapses to the claimed scalar difference.
why it matters
Gives the explicit scalar form of the A-vs-B edge-current first variation at the seated generator-(0,2) edge, which is the concrete amplitude the module treats as a physical current under the G2/G3 model. The sole downstream consumer is the non-vanishing theorem: after rewriting by this identity, separation of the two fingerprints (already proved for cfgA/cfgB) yields a nonzero real difference via injectivity of the natural-to-real cast. That non-vanishing is the quantitative separation step in the order-sensitive history response campaign on the Freudenthal patch. It stays inside the honesty boundary of the module: theorem-level separation and seating, model-level reading of the fingerprint as current, and explicitly not a linearized flat-patch metric perturbation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.