PRCBoundednessDelta_positive
plain-language theorem explainer
The fixed PRC rational threshold used as a boundedness modulus is strictly positive. Anyone citing the real-boundedness certificate or the eventual-interval containment of a J-cost Cauchy ledger needs this fact. The proof reduces positivity to the ordinary rational image via the native-to-ℚ bridge and finishes by numerical evaluation (the threshold is 1/8).
Claim. The fixed PRC-rational distance threshold $\delta := 1/(4\cdot 2) = 1/8$ is positive in the PRC-native sense: its signed numerator is nonnegative and unbalanced against zero (equivalently, its ordinary rational image satisfies $0 < \delta$).
background
Primitive Recognition Calculus (PRC) builds rationals as ratio-orbit quotient classes (PRCRat), with a native positivity predicate: a ratio orbit is positive when its signed numerator is nonnegative and not balanced against zero. That predicate is equivalent to ordinary positivity of the image in $\mathbb{Q}$ via positive_iff_toRat_pos.
In this module the fixed threshold PRCBoundednessDelta is the PRC rational $1/(4\cdot 2)=1/8$. Its doc-comment states the design goal: a distance small enough that a J-cost increment below the threshold forces the ordinary squared increment below one. The surrounding development equips J-cost Cauchy ledgers with a real-style boundedness modulus so that Cauchy sequences are eventually trapped in a symmetric rational interval.
Upstream, the RationalField layer supplies the positivity API and the bridge to $\mathbb{Q}$; the sibling PRCBoundednessDelta_toRat records the concrete rational value of the threshold.
proof idea
Term-mode, two rewrites then arithmetic. Rewrite native positivity along positive_iff_toRat_pos to the claim $0 < \mathrm{toRat}(\delta)$. Substitute PRCBoundednessDelta_toRat to replace the image by the explicit rational $1/8$. Close with norm_num. No case splits and no appeal to the J-cost comparison lemmas.
why it matters
This positivity fact is the gate that lets the Cauchy property fire at the fixed modulus. Downstream, PRCCauchySeqEventuallyBoundedTarget_proved invokes the Cauchy hypothesis at PRCBoundednessDelta with this positivity witness, then anchors a symmetric rational interval at the $N$-th term; its doc-comment: "A J-cost Cauchy ledger is eventually contained in a PRC symmetric rational interval." The same fact is packaged into prc_real_boundedness_modulus_certificate as the field boundedness_delta_positive, pairing with the square-increment bound below one.
In the Recognition foundation this is scaffolding for the real completion of the J-cost ledger (Primitive Recognition Calculus), not a forcing-chain landmark (T5–T8). It closes the elementary arithmetic obligation so later steps can treat the modulus as a genuine positive distance without carrying a side proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.