prc_real_boundedness_modulus_certificate
plain-language theorem explainer
Packages the Step 10b boundedness-modulus certificate for the primitive recognition calculus: positivity of the fixed threshold, the square-increment bound under small J-cost distance, eventual boundedness of J-Cauchy ledgers, and the two conditional multiplication targets once bounded product-continuity is assumed. Kernel first-pass assembly cites it. Proof is a structure inhabitant wiring five already-proved lemmas.
Claim. The Step 10b boundedness-modulus certificate holds: the fixed boundedness threshold $\delta$ is positive; if the $J$-cost distance between two PRC rationals is less than $\delta$, then their ordinary rational difference has square less than $1$; every $J$-cost Cauchy ledger is eventually contained in a symmetric rational interval; and both product Cauchy-closure and product congruence follow from that eventual boundedness once bounded product-continuity is granted.
background
Primitive Recognition Calculus (PRC) builds a real-number layer from a $J$-cost ledger on a rational display. The cost $J$ is the unique nonnegative defect of the Recognition Composition Law; distances are measured in that cost, not in the ordinary absolute value. A fixed positive threshold $\delta$ (the boundedness delta) is chosen so that a small $J$-distance forces the ordinary squared increment below one.
Eventual boundedness means every $J$-Cauchy sequence of PRC rationals is eventually trapped in a symmetric rational interval. That fact is already proved in this module. Multiplication of Cauchy ledgers still needs a continuity hypothesis on products over bounded sets; the certificate records that, given that hypothesis, both product closure and product congruence follow.
The local setting is Step 10b of the PRC real construction: close the boundedness modulus so the only remaining multiplication blocker is bounded product-continuity.
proof idea
Structure inhabitant, not a deep argument. Positivity of $\delta$ is the already-proved numeric fact. The square-increment field is discharged by introducing two PRC rationals and applying the lemma that $J$-distance below $\delta$ forces ordinary squared difference below one. Eventual boundedness is plugged in as the proved Cauchy-ledger target.
The two multiplication fields are one-line conditionals: assume bounded product-continuity, then apply the upstream theorems that derive product Cauchy-closure and product congruence from eventual boundedness plus that continuity hypothesis, feeding the proved eventual-boundedness target as the first argument.
why it matters
Closes Step 10b of the PRC real layer: eventual boundedness is settled, so multiplication is reduced to a single remaining hypothesis (bounded product-continuity). Downstream, the kernel first-pass certificate (K7/A2) consumes this package when assembling the inhabited first-pass kernel surface.
In the broader Recognition stack this sits under the foundation forcing chain that later forces $J$-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). The certificate does not itself force those landmarks; it clears a real-construction bottleneck so later ledger arithmetic can proceed without an open boundedness gap.
The open residual is explicit in the structure doc: only bounded product-continuity still blocks full multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.