prc_jcost_distance_verifier_triangle_conditional_certificate
plain-language theorem explainer
Conditional certificate for Build Order step 9b: the three-endpoint J-cost verifier triangle on rationals reduces to a one-dimensional additive increment modulus. Kernel and PRC first-pass assemblers cite it to isolate the remaining obligation. The proof is a term-mode structure inhabitant wiring translation invariance, a trivial identity on the increment target, and two implication lemmas.
Claim. A conditional certificate for the rational J-cost verifier triangle holds: (i) the displayed distance between rationals $x,y$ equals a pure function of the increment $x-y$; (ii) the increment-only triangle target is self-identical; (iii) that increment target implies the three-endpoint verifier triangle target; (iv) that increment target implies the PRC null-distance setoid target.
background
In the Primitive Recognition Calculus, distances on rationals are displayed via a J-cost style functional of the endpoints. The displayed distance is translation-invariant: it depends only on the difference of the endpoints, not on their absolute placement. That fact is already proved by a short algebraic identity.
Build Order step 9b asks for a three-endpoint verifier triangle inequality on those displayed distances. The module reduces that ask to a sharper one-dimensional blocker: an additive two-leg modulus stated only for rational increments. Two upstream lemmas then lift any proof of the increment modulus to (a) the full verifier triangle target and (b) the PRC null-distance setoid target that closes the equivalence-relation chain.
The conditional certificate packages exactly those four pieces: translation invariance, a placeholder identity for the increment target, and the two lifting implications. The only remaining mathematical theorem is the increment-only modulus itself.
proof idea
Term-mode construction of the conditional-certificate structure. The translation-invariance field is filled by the already-proved identity that the displayed rational distance equals the increment display of $x-y$. The increment-triangle field is the trivial reflexivity rfl on that target proposition. The verifier-from-increment field is the lifting lemma that turns any proof of the increment modulus into a three-endpoint verifier triangle. The setoid-from-increment field is the further composition that routes the same increment hypothesis through the verifier lift into the null-distance setoid target.
why it matters
This is the Build Order step 9b conditional closure: it pins the entire verifier-triangle and null-distance-setoid obligations onto a single one-dimensional additive estimate. Downstream, the kernel first-pass certificate (K7/A2) consumes this packaging when it assembles the inhabited kernel surface. In the Recognition forcing chain the J-cost $J(x)=(x+x^{-1})/2-1$ is the unique cost forced at T5; controlling its triangle behaviour on rational displays is a prerequisite for treating null-cost pairs as a setoid and for later continuum and physical-constant extractions. The certificate does not discharge the increment modulus; it makes that modulus the unique open gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.