Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceVerifierTriangle

show as:
view Lean formalization →

Module packaging the verifier form of the triangle inequality for rational J-cost distance in the primitive recognition calculus. It exposes one-increment displays, triangle targets, and a conditional certificate that the distance induced by J satisfies the triangle law under named hypotheses. Downstream Kernel and increment-triangle modules import it as the bridge from display data to certified metric structure. The argument is mostly target packaging and certificate wiring over the upstream triangle module.

claimFor the rational $J$-cost distance $d_J$ on the primitive recognition calculus, the module records one-increment displays of $d_J$, the associated triangle targets, and a conditional certificate that $d_J(x,z)\le d_J(x,y)+d_J(y,z)$ holds when the increment-triangle hypotheses are met. Null-distance setoid targets are derived from the same increment data.

background

Primitive recognition calculus works with the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law and T5 uniqueness. Distances built from $J$ on positive rationals (or phi-ladder rungs) are the natural candidates for a metric on recognition states.

The upstream module PRCJCostDistanceTriangle already states the triangle inequality for that distance. This module specializes to a verifier presentation: one-increment displays of the rational $J$-cost distance, triangle targets built from those displays, and the passage from increment data to a null-distance setoid target.

Sibling names make the layering explicit: increment display, rational display as increment, increment-triangle target, verifier-triangle target of an increment, and the conditional certificate that packages the claim for later discharge.

proof idea

Definition and certificate module rather than a long tactic proof. It imports the plain triangle development, defines one-increment display objects for rational $J$-cost distance, rephrases those displays as increments, and builds verifier-triangle targets from the increment-triangle targets. A conditional certificate records the triangle claim under the named hypotheses; a companion lemma exposes that certificate for import. Null-distance setoid targets are obtained by the same increment-triangle route. No independent analytic argument is introduced here.

why it matters in Recognition Science

Kernel of the primitive recognition calculus imports this module, so the verifier-triangle certificate sits on the path from raw $J$-cost geometry to the core PRC interface. The increment-triangle module also depends on it, tightening the one-step display story into a reusable triangle package.

In the broader Recognition chain this is foundation plumbing under T5 $J$-uniqueness and the RCL identity: once $J$ is forced, distances built from it must obey triangle if they are to underwrite later metric or setoid constructions on recognition states. The conditional certificate keeps the claim honest until the increment hypotheses are fully discharged upstream.

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)