IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceVerifierTriangle
Module packaging the verifier-triangle view of rational J-cost distance in the primitive recognition calculus. It ties one-increment displays of that distance to triangle targets, a null-distance setoid target, and a conditional certificate. Kernel and the increment-triangle module import it as the bridge from the plain triangle development. Content is mostly target and certificate scaffolding rather than a single closed theorem.
claimObjects for the verifier form of the rational $J$-cost distance triangle: one-increment displays of that distance, a verifier-triangle target obtained from the increment triangle, the induced null-distance setoid target, and a conditional certificate asserting the verifier triangle once the increment hypotheses hold.
background
In Recognition Science the cost functional is forced as $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Distances built from $J$ on positive rationals are the primitive recognition calculus objects that later feed uniqueness and forcing arguments.
The parent module PRCJCostDistanceTriangle develops the plain triangle inequality for that rational $J$-cost distance. This module sits one layer above: it re-expresses the same geometry in verifier and one-increment form, so downstream code can treat triangle, null-setoid, and certificate data uniformly.
Sibling names indicate displays of the rational distance as an increment, targets for the increment and verifier triangles, a null-distance setoid target derived from the increment triangle, and a conditional certificate packaging those obligations.
proof idea
Definition and interface module, not a single end-to-end proof. It introduces display abbreviations for the one-increment rational $J$-cost distance, then target propositions for the increment triangle and the verifier triangle (the latter obtained from the former). From the increment-triangle target it derives a null-distance setoid target. A conditional certificate bundles the verifier-triangle claim under the named increment hypotheses; the corresponding value is the reusable certificate object downstream modules import.
why it matters in Recognition Science
Closes the gap between the plain $J$-cost distance triangle and the verifier-shaped interfaces the primitive recognition calculus kernel expects. Downstream, PrimitiveRecognitionCalculus.Kernel imports this module as part of the core stack, and PRCJCostDistanceIncrementTriangle builds the increment-triangle development on the targets and certificate defined here.
In the broader forcing picture this is scaffolding around T5-style $J$-uniqueness geometry: triangle and null-setoid structure for the cost distance must be available before higher recognition composition and dimension-forcing steps can treat distance as a settled primitive. The conditional certificate marks what remains hypothesis-bound versus already discharged in the plain triangle module.
scope and limits
- Does not prove the unrestricted verifier triangle; only a conditional certificate under increment hypotheses.
- Does not redefine $J$ or re-derive $J$-uniqueness (T5); it consumes the cost distance from upstream.
- Does not establish the eight-tick, $\varphi$, or $D=3$ forcing steps.
- Does not by itself discharge Kernel obligations beyond exporting targets and the certificate.
- Does not claim a numerical or physical mass/ladder result; scope is foundation distance geometry only.
used by (2)
depends on (1)
declarations in this module (7)
-
def
PRCJCostDistanceIncrementDisplay -
theorem
PRCJCostDistanceRatDisplay_as_increment -
def
PRCJCostDistanceIncrementTriangleTarget -
theorem
PRCJCostDistanceVerifierTriangleTarget_of_increment -
theorem
PRCNullDistanceSetoidTarget_of_increment_triangle -
structure
PRCJCostDistanceVerifierTriangleConditionalCertificate -
theorem
prc_jcost_distance_verifier_triangle_conditional_certificate