Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealBoundednessModulus

show as:
view Lean formalization →

Defines a fixed rational distance threshold (the PRC boundedness delta) small enough that any two points closer than this force the squared ordinary increment of the J-cost distance below one. Supplies the positivity and conversion lemmas, the square-difference bound, and a certificate that Cauchy sequences are eventually bounded. Downstream continuity and kernel modules cite it when controlling real multiplication and product limits in the primitive recognition calculus.

claimThere is a fixed positive rational $\delta_{\mathrm{bd}}>0$ such that if the PRC $J$-cost distance between two reals is strictly less than $\delta_{\mathrm{bd}}$, then the squared ordinary increment of that distance is strictly less than $1$. The module packages this threshold, its positivity, the square bound, and a certificate that PRC Cauchy sequences are eventually bounded.

background

Primitive Recognition Calculus (PRC) rebuilds real analysis from the Recognition Composition Law and the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Distances are measured in the $J$-cost metric rather than the Euclidean metric; ordinary increments must still be controlled so that classical continuity and Cauchy arguments can be recovered.

The sibling module RealMulBoundedContinuity already treats multiplication under a boundedness hypothesis. This module isolates the numerical threshold that makes the squared increment of $J$-cost distance drop below one, which is the elementary comparison needed before one can pass from PRC Cauchy data to ordinary real boundedness.

The main named objects are the fixed rational $\delta_{\mathrm{bd}}$ (PRCBoundednessDelta), its positivity, the implication from distance $<\delta_{\mathrm{bd}}$ to squared increment $<1$, and a certificate packaging the eventual-boundedness target for Cauchy sequences.

proof idea

The module is a short foundation layer, not a single deep theorem. It fixes an explicit positive rational threshold, proves it is positive, and shows that $J$-cost distance below the threshold forces the squared ordinary increment below one by direct comparison with the algebraic form of $J$. A conversion-to-rational lemma and a packaged certificate then expose the bound to downstream continuity arguments. No long tactic script is required: the work is choosing the constant and discharging elementary real inequalities.

why it matters in Recognition Science

Eventual boundedness of PRC Cauchy sequences is a prerequisite for reconstructing real multiplication and product continuity inside the recognition calculus. Kernel and RealProductContinuity import this module precisely to obtain that control. In the broader RS forcing chain, $J$-uniqueness (T5) and the composition law fix the cost; this file turns that cost into a concrete modulus that classical analysis can use. Without the squared-increment bound below one, the passage from PRC Cauchy data to ordinary real limits would remain informal.

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