PRCJCostDistanceIncrementTriangleCertificate
plain-language theorem explainer
Bundling certificate that the rational J-cost increment display, its triangle inequality, the verifier triangle, triangle modulus, null-distance transitivity and setoid, and a nonempty closed real null-distance carrier with rational embedding all hold at once. Cited by anyone assembling the PRC real carrier from Cauchy ledgers under null J-cost distance. Pure packaging of already-proved targets; the companion theorem fills every field.
Claim. A proposition asserting eight simultaneous claims: (i) for every rational $t$, the J-cost distance increment display equals $\frac{t^{4}}{2(1+t^{2})}$; (ii) that increment meets the triangle target; (iii) the verifier triangle target holds; (iv) the triangle modulus target holds; (v) null distance is transitive; (vi) null distance forms a setoid; (vii) the closed null-distance real carrier is nonempty; (viii) there exists an embedding of PRC rationals into that carrier.
background
Primitive Recognition Calculus (PRC) constructs a real carrier from Cauchy ledgers quotiented by null J-cost distance. The J-cost is the unique nonnegative cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (T5). Observer and multiplicative-recognizer costs are instances of this same $J$.
PRC rationals are nonzero-denominator ratio-orbit quotient classes under cross-multiplication. Null distance is the equivalence relation that identifies ledgers whose J-cost separation vanishes; the closed carrier is the corresponding quotient of Cauchy ledgers once transitivity is secured.
This module is Build Order step 9c: an explicit rational increment estimate for the J-cost distance display, strong enough to close triangle inequality, modulus control, and the full null-distance setoid chain.
proof idea
Definitional structure, not a proved theorem. It is a Prop-valued record whose eight fields name the required targets (increment formula, increment triangle, verifier triangle, triangle modulus, null-distance transitivity, null-distance setoid, nonempty closed carrier, nonempty rational embedding).
The companion theorem prc_jcost_distance_increment_triangle_certificate is a one-shot constructor that fills every field from the corresponding *_proved lemmas and the explicit display identity PRCJCostDistanceIncrementDisplay_formula. No new algebra lives in the structure itself.
why it matters
Closes the J-cost null-distance setoid chain that produces the final PRC real carrier (Cauchy ledgers modulo null distance). Downstream, the companion theorem instantiates this certificate, and KernelFirstPassCertificate consumes the surrounding first-pass kernel surface (K7/A2 bundling of concrete Lean objects for each stage of the analytic specification).
In the Recognition forcing chain this is foundation plumbing under T5 J-uniqueness: without a closed null-distance setoid and rational embedding, later mass-ladder and continuum constructions have no carrier. It is a bundling certificate, not the final inevitability theorem; it records that step 9c is discharged so the kernel first pass can cite a single object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.