responseDiff_fwd_ne
plain-language theorem explainer
The edge-current first variation between Loom certificate configs A and B is nonzero on the generator-(0,2) seat at record-time false. Anyone proving order-sensitive gravity separation (frozen G2/G3) cites this nonvanishing. The proof rewrites the seated difference as a depth-two fingerprint difference and lifts the already-decided fingerprint separation through Nat-to-Real casting.
Claim. Let $A$ and $B$ be the two fixed Loom certificate configurations, and let $(i_0,j_0)$ be the generator-1 edge endpoints seated at record-time false. Then the history-response difference satisfies $\mathrm{responseDiff}(A,B;i_0,j_0)\neq 0$.
background
This module freezes claims G2/G3 of the order-sensitive gravity proposition: an order-sensitive Loom history is read as an antisymmetric Fin-16 edge current on the Freudenthal patch, seated on the generator-(0,2) edge at record-time false via Q3 patch seating. No metric Hamiltonian and no mu-coordinate table enter.
The history response is the depth-two commutator reading of a Loom Config (the same second-order content isolated by pairTraces / pairSum). The response difference is the pointwise subtraction of two such currents. Generator-1 seating places the evaluation at the concrete endpoints (seat(false), seat(i=1)).
Upstream, fingerprint_separates_cfgAB is a decide proof that the Nat list-fingerprints of the two depth-two readings differ. The forward evaluation lemma rewrites the seated real difference exactly as the cast fingerprint difference of A minus B.
proof idea
One short term-mode argument. Rewrite the goal by the forward evaluation lemma, so the seated real difference becomes the difference of the two cast list-fingerprints. Invoke the decide theorem that those fingerprints are unequal as Nats. Conclude the real difference is nonzero by sub_ne_zero, using injectivity of the Nat-to-Real cast to turn a hypothetical real equality back into a Nat equality that contradicts fingerprint separation.
why it matters
Nonvanishing on the seated generator edge is the algebraic hinge for metric-image exclusion. The sole downstream consumer is responseDiff_cfgAB_not_in_MetricEdgeImage, which assumes the difference lies in the strain-current image of some metric H, evaluates at the two orientations of the seat, and uses antisymmetry of the strain current together with this nonzero value to reach a contradiction.
That exclusion is one of the three THEOREM bullets in the module honesty block (separation, action firing, metric-image exclusion on cfgA/cfgB). It supports frozen G2/G3 of the order-sensitive gravity proposition: the depth-two history response is not a linearized flat-patch metric perturbation. Within Recognition gravity analysis this is local 4D patch work on the Freudenthal cover, not a global forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.