PRCJCostDistanceTriangleConditionalCertificate
plain-language theorem explainer
Conditional certificate for Build Order step 9a: the PRC J-cost distance triangle and null-distance setoid both reduce to one explicit rational inequality on the displayed J-cost formula. Kernel and Cauchy-surface authors cite it when packaging first-pass closure. It is a Prop structure whose fields are display equality, a trivial well-formedness clause, and two implication arrows from the verifier target.
Claim. A Prop certificate with four clauses: (1) for all PRC rationals $a,b$, the J-cost distance displays as $\frac{g+g^{-1}}{2}-1$ with $g=1+(x-y)^2$ on the verifier rationals $x=a^{\mathbb{Q}}$, $y=b^{\mathbb{Q}}$; (2) the verifier triangle target equals itself; (3) that target implies the triangle-modulus target; (4) that target implies the null-distance setoid target. The only open analytic obligation is the rational $\varepsilon$-$\delta$ inequality in the verifier target.
background
Primitive Recognition Calculus (PRC) builds reals from traces and ratio-orbit quotients. PRCRat is the nonzero-denominator ratio-orbit quotient; toRat is its verifier display into $\mathbb{Q}$. The J-cost distance on PRC rationals sends additive separation through the positive gap $1+(a-b)^2$, then applies the PRC rational J-cost (the same $J$ forced at T5: $J(x)=(x+x^{-1})/2-1$).
The sibling display PRCJCostDistanceRatDisplay is the explicit rational formula $(g+g^{-1})/2-1$ with $g=1+(x-y)^2$. The verifier triangle target asks: for every positive PRC rational $\varepsilon$ there is a positive $\delta$ such that if two consecutive displayed distances are $<\delta$, the third is $<\varepsilon$. That is the remaining analytic estimate for the null-distance quotient.
This module sits in the foundation layer that transports PRC Cauchy data onto ordinary rational inequalities so later kernel certificates can close without reopening the internal PRC definitions.
proof idea
No proof body: this is a structure definition (a Prop bundle), not a proved theorem. The four fields are named obligations. The companion theorem prc_jcost_distance_triangle_conditional_certificate fills them by (i) the display lemma PRCJCostDistance_toRat, (ii) rfl on the verifier target, (iii) the transport lemma PRCJCostDistanceTriangleModulusTarget_of_verifier, and (iv) PRCNullDistanceSetoidTarget_of_verifier_triangle. The structure only records what must hold for step 9a conditional closure.
why it matters
Step 9a of the Build Order: once the verifier triangle inequality is proved, both the triangle-modulus target and the null-distance setoid target drop out by the packaged implications, so the PRC J-cost distance becomes a genuine pseudometric on the quotient. Downstream, KernelFirstPassCertificate bundles first-pass kernel stages (strength tags, traces, judgment surface, trace logic); this certificate is one of the concrete Lean objects that certificate expects in the analytic chain. The companion inhabitant theorem is the local closure point. Framework link: the displayed cost is exactly the T5 J-cost on the square-gap ratio, so triangle control here is what lets the eight-tick and dimension forcing sit on a Cauchy-complete recognition metric rather than a raw cost functional. Open residue: prove PRCJCostDistanceVerifierTriangleTarget itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.