PRCNullDistanceSetoidTarget_proved
plain-language theorem explainer
The null-distance relation on primitive recognition calculus (PRC) Cauchy data is an equivalence relation, so it yields a real setoid. Anyone building the J-cost metric quotient or the PRC real carrier cites this closure. The proof is a one-line term application of the increment-triangle reduction to the already-proved rational increment estimate.
Claim. The intended PRC null-distance relation is an equivalence relation: it is reflexive, symmetric, and transitive. Equivalently, the null-distance setoid target holds, so the relation may be used as the real setoid carrier for the J-cost distance construction.
background
In the primitive recognition calculus, Cauchy-style sequences are compared by a J-cost distance built from the Recognition Composition Law cost $J(x)=(x+x^{-1})/2-1$. Sequences at null distance are meant to be identified before forming the real carrier. The target proposition is exactly that this null-distance relation is an equivalence (reflexivity and symmetry already settled; transitivity was the remaining obligation).
Upstream, an explicit rational increment-triangle estimate for the J-cost display is already proved. A verifier-triangle bridge then shows that any such increment-only bound closes the full null-distance setoid chain. The local module packages those increment estimates and the resulting setoid and modulus closures.
The modular-logic modulus carrier size appears only as ambient infrastructure; the mathematical content here is the equivalence of null distance, not a change of modulus.
proof idea
One-line term proof. Apply the bridge lemma that any proof of the J-cost increment-triangle target yields the null-distance setoid target, feeding in the already-established increment-triangle theorem. That bridge itself routes through the verifier-triangle intermediate, so the increment estimate is the sole remaining analytic input; no new $\varepsilon$-$ $ work is done at this declaration.
why it matters
This declaration discharges the live setoid obligation on PRC null distance: once equivalence holds, the intended quotient carrier is legitimate. Downstream it is assembled into the J-cost distance increment-triangle certificate, whose doc-comment states that the explicit rational increment estimate closes the whole J-cost null-distance setoid chain (increment formula, increment triangle, verifier triangle, and triangle modulus).
In the Recognition foundation stack this is infrastructure for the real completion used by later forcing and cost geometry, not a direct T5–T8 step. It removes the last setoid blocker between the rational increment display and a usable null-distance quotient, so metric and Cauchy arguments can proceed on equivalence classes rather than raw sequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.