prc_jcost_distance_triangle_conditional_certificate
plain-language theorem explainer
Conditional certificate for Build Order step 9a: PRC J-cost distance triangle transport and the null-distance setoid both reduce to one explicit rational inequality. Kernel assemblers cite it when inhabiting the first-pass kernel certificate. The proof is a term-mode structure fill that wires the display theorem and two transport lemmas.
Claim. A conditional certificate for step 9a is inhabited: for all PRC rationals $a,b$, the J-cost distance displays as the stated rational formula; the verifier-rational triangle target implies the triangle-modulus target; and that same verifier target implies the null-distance setoid target. The sole remaining obligation is the explicit rational triangle inequality.
background
Primitive Recognition Calculus (PRC) works over a rational carrier with a J-cost distance built from the Recognition cost $J(x)=(x+x^{-1})/2-1$. Distances are compared after a conservative rational display map, so analytic claims become explicit inequalities on rationals.
The module isolates the triangle inequality for this distance and the induced null-distance setoid (pairs at distance zero). Upstream, the display theorem equates the abstract PRC J-cost distance, after .toRat, with PRCJCostDistanceRatDisplay on the underlying rationals. Two transport lemmas then say: if the verifier-rational triangle inequality holds, the triangle-modulus target follows by display transport, and the null-distance setoid target follows from that modulus target.
The conditional certificate structure packages exactly those four pieces, leaving only the rational inequality as open mathematics.
proof idea
Term-mode inhabitant of the conditional-certificate structure. The distance_display field is the already-proved display theorem equating PRC J-cost distance to its rational display. The verifier_triangle_target field is discharged by rfl (definitional self-equality of the target Prop). The two implication fields are filled by the named transport theorems: verifier target implies triangle-modulus target, and verifier target implies null-distance setoid target (the latter via the former plus the modulus-to-setoid bridge).
why it matters
Closes Build Order step 9a conditionally: triangle transport for the PRC J-cost distance is reduced to one displayed rational inequality. Downstream, the first-pass kernel certificate (kernel_first_pass_certificate, tagged K7/A2) consumes this packaging when assembling strength tags, trace syntax, and judgment surface. In the broader Recognition stack this sits under the foundation layer that eventually supports the forcing chain (J-uniqueness, $\phi$, eight-tick octave, $D=3$): a usable null-distance quotient needs the triangle inequality, and this certificate makes that dependency fully explicit and local to a rational estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.