responseDiff_cfgAB_not_in_MetricEdgeImage
plain-language theorem explainer
The history-response difference between the two distinguished Loom configurations lies outside every finite linearized metric strain current on the Freudenthal patch. Gravity analysts cite it as the finite-stage G3 exclusion: an order-sensitive residual cannot be absorbed by any metric matrix H. The proof evaluates a putative strain current on the seated generator edge, pits strain symmetry against response antisymmetry, and contradicts the nonzero forward amplitude.
Claim. The edge-current difference of history responses between the two distinguished Loom configurations is not in the finite linearized metric edge image: there is no $4\times 4$ matrix $H$ such that that difference equals the strain current of $H$ on the Freudenthal patch edges.
background
This module freezes claims G2/G3 of the Order-Sensitive Gravity proposition. It reads a Loom configuration through a depth-two commutator fingerprint and seats that reading as an antisymmetric Fin-16 edge current on the generator-(0,2) edge (record-time false) via the Q3 patch seating. No metric matrix and no mu-coordinate table enter the construction.
The metric edge image is the set of Fin-16 bilinears of the form $\mathrm{strainCurrent}(H)$ for some $4\times 4$ matrix $H$, where strain current is edge strain of the patch displacement. Strain current is symmetric in its two edge endpoints. The response difference is the pointwise difference of history responses of two configurations; on the seated generator edge it is antisymmetric and the forward value is nonzero.
The cost reparametrization $H(x)=J(x)+1$ appears only as ambient algebra; the argument itself is pure linear algebra on the patch edge currents.
proof idea
Assume for contradiction that the response difference equals $\mathrm{strainCurrent}(H)$ for some matrix $H$. Specialize both endpoint orders of the seated generator edge. Strain-current symmetry equates the two specializations, so the response difference is symmetric on that edge. Antisymmetry of the response difference then forces the forward value to vanish. That contradicts the already-proved nonzero forward amplitude on the same edge. The whole argument is a short calc plus linarith.
why it matters
This is the finite-stage G3 exclusion named in the module honesty block: the order-sensitive residual sits outside every linearized flat-patch metric perturbation. Downstream, orderSensitive_finite_gate_cfgAB packages it with depth-one source blindness and history-response separation into the three-conjunct finite gate. The continuum residual module re-exports it verbatim as finite_outside_metric_image ("Finite stage already outside the metric image (imported G3)").
In the broader Recognition gravity program this is the discrete witness that history-order content on the eight-tick / Freudenthal seating is not a metric strain. It does not yet promote the fingerprint amplitude to a continuum field equation; that remains a modeling step flagged in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.