PRCJCostDistanceVerifierTriangleConditionalCertificate
plain-language theorem explainer
Conditional certificate packaging Build Order step 9b: the three-endpoint J-cost verifier triangle and the null-distance setoid both reduce to a single one-dimensional additive increment modulus on rationals. Anyone closing the PRC distance quotient cites this bundle. The structure records translation invariance of the display, a tautological self-equality of the increment target, and the two implication arrows from that target.
Claim. A proposition bundling four facts: (i) the rational J-cost display $d(x,y)=(g+g^{-1})/2-1$ with $g=1+(x-y)^2$ equals the one-increment display of $x-y$; (ii) the additive two-leg increment-modulus target is identical to itself; (iii) that increment modulus implies the three-endpoint verifier triangle modulus; (iv) that same increment modulus implies the null-distance relation is an equivalence (the setoid target).
background
Primitive Recognition Calculus builds a real carrier by quotienting traces under a null J-cost distance. The verifier display of that distance on rationals is $d(x,y)=(g+g^{-1})/2-1$ with $g=1+(x-y)^2$, the same algebraic shape as the RS J-cost $J(x)=(x+x^{-1})/2-1$. The one-increment display is simply $d(0,t)$, and translation invariance says the two-point display depends only on the difference of endpoints.
The three-endpoint verifier triangle target asks for a modulus of continuity: for every positive PRC-rational $\varepsilon$ there is $\delta$ so that small $d(x,y)$ and $d(y,z)$ force small $d(x,z)$. The sharper increment triangle target restates the same estimate on pure increments $p,q\in\mathbb{Q}$: small $d(0,p)$ and $d(0,q)$ force small $d(0,p+q)$. Upstream, the null-distance setoid target is exactly the claim that the intended null relation is an equivalence; reflexivity and symmetry are already proved, and transitivity is the live obligation.
proof idea
This declaration is a bare Prop structure, not a proved theorem. It names the four fields that a later inhabitant must supply: the translation-invariance identity, a reflexive equality placeholder for the increment target, and the two implication arrows (increment target implies verifier triangle; increment target implies setoid target). The sibling theorem that fills the structure applies the translation lemma, rfl on the self-equality, and the two reduction lemmas that derive the verifier and setoid targets from the increment modulus.
why it matters
Step 9b of the PRC build order collapses the remaining analytic work for the J-cost distance quotient to one statement: an additive two-leg modulus on rational increments. Downstream, the concrete certificate theorem inhabits this structure, and the first-pass kernel certificate bundles the surrounding PRC stage objects. Closing the increment modulus discharges both the verifier triangle needed for the rational display and the transitivity half of the null-distance setoid, which is the gate to the first internal quotient carrier. In RS terms this is foundation plumbing under the J-cost uniqueness (T5), not yet a forcing-chain step, but it is the exact blocker between the displayed J-distance and a usable real setoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.