PRCRealBoundednessModulusCertificate
plain-language theorem explainer
Certificate for Step 10b of the Primitive Recognition Calculus real construction: a fixed positive rational distance threshold forces ordinary squared increments below one, Cauchy sequences are eventually bounded, and multiplication closure and congruence reduce to bounded product-continuity alone. The first-pass kernel certificate and the companion inhabitant theorem cite it. As a Prop-structure it only packages obligations; proofs live in the field fillers.
Claim. A Prop-valued certificate with five clauses: (i) the fixed boundedness threshold $\delta=1/8$ in PRC rationals is positive; (ii) if the $J$-cost distance between PRC rationals $a,b$ is strictly less than $\delta$, then the ordinary squared difference satisfies $(a^{\mathrm{disp}}-b^{\mathrm{disp}})^2<1$ in verifier rationals; (iii) every PRC Cauchy sequence is eventually bounded; (iv) bounded product-continuity of $J$-cost distance implies real multiplication closure; (v) the same continuity hypothesis implies real multiplication congruence.
background
Primitive Recognition Calculus (PRC) rebuilds arithmetic from recognition primitives before classical reals appear. PRC rationals are quotient classes of ratio orbits (nonzero-denominator pairs of signed orbits), ordered by nonnegative unbalanced difference, with positivity meaning a nonnegative unbalanced numerator. The map toRat is only a verifier display into ordinary $\mathbb{Q}$; internal identities use cross-multiplication.
The boundedness threshold $\delta$ is the fixed PRC rational $1/(4\cdot 2)=1/8$, chosen small enough that a $J$-cost ball of radius $\delta$ forces the ordinary squared increment below one. $J$-cost distance is the recognition metric built from the unique cost $J$ of the forcing chain (T5), not the Euclidean metric.
This module sits after real Cauchy data and bounded-multiplication continuity scaffolding. The local goal is to isolate what remains before PRC reals support a well-defined multiplication: eventual boundedness of Cauchy sequences, plus reduction of mul-closure and mul-congruence to a single continuity hypothesis.
proof idea
No proof body: the declaration is a structure extending Prop, i.e. a named bundle of five propositions. Field (i) is positivity of the constant $\delta=1/8$. Field (ii) is the universal implication from $J$-cost proximity below $\delta$ to ordinary squared difference $<1$. Field (iii) is the eventual-boundedness target for PRC Cauchy sequences. Fields (iv)–(v) are pure implications from the bounded product-continuity target to real mul-closure and mul-congruence targets.
The companion theorem prc_real_boundedness_modulus_certificate inhabits the structure by plugging in PRCBoundednessDelta_positive, the squared-difference lemma PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta, and the already-proved eventual-boundedness and continuity-reduction lemmas.
why it matters
Step 10b closure in the PRC real stack: once eventual boundedness is on record, the only remaining multiplication blocker is bounded product-continuity of $J$-cost distance. Downstream, prc_real_boundedness_modulus_certificate supplies a concrete inhabitant, and KernelFirstPassCertificate (K7/A2) bundles this stage into the first-pass kernel certificate: "the analytic specification has concrete Lean objects for each stage in the first theorem chain" (still a bundling certificate, not final inevitability).
In the broader Recognition framework this is foundation plumbing under the forcing chain, not a physics endpoint. It prepares well-defined real multiplication so later layers can host the Recognition Composition Law, $J$-uniqueness (T5), and the phi ladder without metric pathologies. Open remainder after this certificate: discharge the product-continuity hypothesis itself so mul-closure and mul-congruence become unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.