Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealBoundednessModulus

show as:
view Lean formalization →

Supplies a fixed rational distance threshold in the Primitive Recognition Calculus so that J-cost distance increments have ordinary square strictly below one. Analysts building real Cauchy and product continuity from PRC data cite it. The argument is a concrete positive rational delta plus elementary comparison lemmas that convert a distance bound into a square bound.

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

background

Primitive Recognition Calculus works with displays and a J-cost distance before ordinary real arithmetic is fully available. The cost $J$ is the unique symmetric generator from the forcing chain ($J(x)=(x+x^{-1})/2-1$), and distances built from it control how close two recognition states are. To pass from PRC Cauchy data to real limits one needs a uniform modulus that keeps ordinary increments inside a safe ball.

This module sits on RealMulBoundedContinuity and introduces a single fixed rational threshold $\delta_{\mathrm{bd}}$ small enough that any J-cost distance below it forces the squared ordinary increment below one. Sibling objects record the rational value, its positivity, the square comparison for increment displays, and the eventual-boundedness target for Cauchy sequences.

The local setting is foundation-level analysis inside Recognition Science: convert discrete recognition distances into classical real boundedness without assuming a finished real product topology.

proof idea

Definition-first module. A concrete positive rational PRCBoundednessDelta is fixed and cast to $\mathbb{Q}$. Positivity is immediate. The key comparison lemma states that if J-cost distance is less than this delta, then the squared ordinary increment display is strictly less than one. That comparison is fed into a proved eventual-boundedness statement for PRC Cauchy sequences, then wrapped as a named certificate object and a top-level certificate lemma for downstream import.

why it matters in Recognition Science

Real product continuity and the PRC Kernel both import this module. Without a uniform boundedness modulus, Cauchy sequences in J-cost distance need not stay inside a region where multiplication and limits behave classically. The certificate closes the boundedness step of the real-construction path that later supports continuity of products and the kernel interface for recognition calculus. It is infrastructure rather than a forcing-chain landmark, but it is required before real arithmetic can be treated as continuous on PRC data.

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)