prc_jcost_distance_increment_triangle_certificate
plain-language theorem explainer
An explicit rational increment formula for J-cost distance closes the full null-distance setoid package: triangle inequality, modulus control, transitivity, and a closed real carrier with rational embedding. Foundation auditors cite it as Build Order step 9c. The proof is a term that assembles six already-proved targets plus the closed-carrier witnesses.
Claim. There is a closure certificate for the J-cost distance increment triangle package: for every rational $t$, the increment display equals $t^4/(2(1+t^2))$; the increment triangle, verifier triangle, and triangle-modulus targets hold; null-distance is transitive and forms a setoid; and the null-distance quotient carrier is inhabited by a closed real with a rational embedding.
background
Primitive Recognition Calculus builds a J-cost distance on rational displays and then quotients by null distance. The J-cost is the unique cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). The increment display measures how that cost grows under a rational step $t$; the sibling formula proves it equals $t^4/(2(1+t^2))$.
Build Order step 9c packages the analytic control needed to treat null distance as a setoid and to embed rationals into a closed real carrier. Upstream, the increment-triangle, verifier-triangle, and triangle-modulus targets are already discharged; the modulus target is obtained from the verifier triangle via the explicit rational estimate. ofRat embeds a PRC rational into that closed null-distance quotient carrier.
Local setting: close the J-cost null-distance chain so later kernel certificates can treat equality-up-to-null-distance as a genuine equivalence.
proof idea
Term-mode structure inhabitant. Fill each certificate field by an already-proved sibling:
increment_formulafrom the algebraic identityPRCJCostDistanceIncrementDisplay_formula(unfold, positivity of $1+t^2$,field_simp,ring).increment_triangle,verifier_triangle,triangle_modulus,null_distance_transitive, andnull_distance_setoidfrom the corresponding*_Target_provedtheorems (modulus reduces to the verifier triangle).real_null_carrierandrat_embeddingby packagingPRCRealNullClosed.ofRat(constant protocol at a rational, specialized at $0$ for the carrier witness).
why it matters
This is the Build Order step 9c closure certificate: the explicit rational increment estimate finishes the whole J-cost null-distance setoid chain. Downstream, kernel_first_pass_certificate (K7/A2) consumes foundation certificates of this shape when inhabiting the first-pass kernel package (strength tags, trace syntax, judgment surface, trace logic).
In the Recognition forcing chain, J-uniqueness (T5) and the composition law make cost comparisons the primitive metric; without a closed null-distance setoid and triangle modulus, later equality judgments on the recognition calculus cannot be quotiented cleanly. The certificate does not itself force $\varphi$, the eight-tick octave, or $D=3$, but it supplies the metric hygiene those later steps assume when they compare costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.