PRCBoundednessDelta
plain-language theorem explainer
Fixed PRC-rational distance threshold equal to 1/8, built as the reciprocal of 4·2 in the ratio-orbit calculus. Anyone proving eventual boundedness of J-cost Cauchy ledgers, or that small J-cost distance forces ordinary increment square below one, cites this constant. Pure arithmetic construction from unit rationals; no theorem content.
Claim. Define the fixed PRC rational $\delta := 1 \cdot (4 \cdot 2)^{-1}$, i.e. $\delta = 1/8$ in the ratio-orbit quotient. This threshold is chosen small enough that a J-cost distance strictly below $\delta$ forces the ordinary rational display increment to satisfy $(a - b)^2 < 1$.
background
Primitive Recognition Calculus works with PRC rationals: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication (K4.8). Arithmetic on these classes is the native language before real completion.
This module supplies a boundedness modulus for real construction. The J-cost distance between two PRC rationals is the native metric; the ordinary rational display map sends each class to $\mathbb{Q}$. The fixed threshold $\delta$ links the two: distances below $\delta$ must force the squared ordinary increment below one, so Cauchy ledgers become eventually trapped in a symmetric rational interval.
Upstream, the constant two appears as the ratio orbit with numerator the signed orbit of two and denominator one. Here two and four are rebuilt from unit addition and multiplication inside PRCRat itself.
proof idea
Definitional construction, not a proof. Set two := 1 + 1 and four := two · two inside PRCRat, then return 1 · (four · two)⁻¹. The sibling lemma equating the display to 1/8 in ℚ is a separate unfold-and-norm_num argument; positivity is likewise deferred.
why it matters
Step 10b of the real-construction ladder needs a concrete positive modulus so that J-cost Cauchy sequences are eventually bounded. This constant is that modulus.
It is consumed by the positivity lemma, the display-equality lemma (value 1/8), the implication from J-cost distance below the threshold to ordinary square-increment below one, the proved eventual-boundedness target for Cauchy ledgers, and the Step 10b closure certificate structure. That certificate records that eventual boundedness is settled, leaving only bounded product-continuity as the remaining multiplication blocker.
In the broader Recognition stack this is scaffolding for completing the reals from the primitive calculus, not a forcing-chain (T0–T8) landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.