Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceTriangle

show as:
view Lean formalization →

Module packaging the triangle inequality for the J-cost square-gap distance in Primitive Recognition Calculus, in verifier-display (rational) form rather than as the native PRC definition. Supplies the rational formula via the to-rat display, triangle and modulus targets, and a conditional certificate. Downstream Kernel and the dedicated verifier-triangle module import it to close metric structure on the null setoid.

claimOn the real null setoid of PRC, the square-gap distance built from the J-cost $J(x)=(x+x^{-1})/2-1$ admits a rational verifier display $d_{\mathrm{rat}}$; the module records triangle targets, the induced modulus, and a conditional certificate that $d_{\mathrm{rat}}(x,z)\le d_{\mathrm{rat}}(x,y)+d_{\mathrm{rat}}(y,z)$.

background

Primitive Recognition Calculus works on a real null setoid (imported from RealNullSetoid): equivalence classes of positive reals under the recognition null relation, so that cost and distance descend to well-defined quotients. The fundamental cost is the J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain.

Distance is not taken as raw $J$ but as a square-gap construction that yields a genuine metric candidate on the quotient. This module does not redefine that PRC distance; it exposes the rational formula shown by the to-rat display, intended for verifier-side checking and certificate packaging rather than as the definitional core.

Sibling declarations name the rat display, the conversion map, verifier triangle and modulus targets, the induced null-distance setoid target, and the conditional triangle certificate.

proof idea

Definition-and-certificate module, not a single closed theorem. It introduces the rational verifier display of the J-cost square-gap distance, the map that produces that display, and Prop-level targets for the triangle inequality and its modulus. Conditional certificates package the triangle claim under named hypotheses; the null-distance setoid target is derived from the verifier triangle. Substantive inequality work is deferred to the dedicated verifier-triangle consumer and Kernel.

why it matters in Recognition Science

Metric structure on the PRC null setoid is a prerequisite for treating recognition cost as a geometry rather than a bare functional. This module supplies the verifier-facing triangle package that Kernel and PRCJCostDistanceVerifierTriangle import, so that downstream development can quote a rational display and a conditional triangle certificate without re-deriving the square-gap algebra. In the broader RS chain it sits under the J-uniqueness (T5) and RCL layer: once $J$ is fixed, square-gap distance and triangle are the natural next metric axioms. It does not itself finish the unconditional triangle proof; it organizes the interface those later modules discharge.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)