Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle

show as:
view Lean formalization →

Module that closes the rational increment modulus for the J-cost distance triangle inequality in Primitive Recognition Calculus. It packages the proved increment-triangle target, related comparison lemmas between squared increments and display values, and the export certificate. Downstream Kernel and real-field layers import it as the last rational-side triangle step. The argument is certificate assembly over already-proved verifier and increment targets.

claimOn the rational side of Primitive Recognition Calculus, the J-cost distance increment modulus satisfies the triangle inequality: the display increment of a composite step is controlled by the sum of the display increments of the factors, with comparison lemmas relating squared increments to the display scale $\delta$. The module records the proved target and the corresponding certificate for this rational closure.

background

Primitive Recognition Calculus builds metric structure from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique cost forced by the Recognition Composition Law. Distance is read from J-cost increments; a triangle inequality on those increments is required before null-distance can be quotiented to a genuine metric and before the construction lifts from rationals to a complete ordered field.

The immediate upstream module is the verifier-triangle layer, which already discharges the checker form of the triangle statement. This module is the final rational increment-modulus closure: it ties the display formula for increments, the two-way comparisons between squared increments and display thresholds, and the named proved targets (increment triangle, verifier triangle, null-distance setoid and transitivity, triangle modulus) into one exportable package.

Sibling material includes the increment display formula, the inequalities increment display $<$ when square $<$ and the converse square bound from a display gap, null-closed reals, and ofRat embeddings used when the rational certificate is consumed higher up.

proof idea

Not a single theorem proof: a closure module. It re-exports and certifies targets already marked proved (increment triangle, verifier triangle, null-distance setoid/transitivity, triangle modulus), together with elementary comparison lemmas between squared increments and display values. The certificate prc_jcost_distance_increment_triangle_certificate packages those proved flags so Kernel and the real complete ordered field layer can import one object rather than reopen the rational case analysis.

why it matters in Recognition Science

Without a closed rational increment triangle for J-cost distance, the PRC kernel cannot treat null-distance as a setoid or pass a triangle modulus upward, and the real complete ordered field construction has no rational base step to complete. Downstream importers are exactly PrimitiveRecognitionCalculus.Kernel and RealCompleteOrderedField. In the broader Recognition chain this is foundation plumbing under T5 J-uniqueness and the RCL: it does not force $\phi$ or dimension, but it makes the J-cost metric usable on $\mathbb{Q}$ before continuum lift. Doc-comment frames it as the final closure for the rational increment modulus.

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 (12)