PRCBoundednessDelta_toRat
plain-language theorem explainer
The fixed PRC boundedness threshold evaluates to the ordinary rational 1/8 under the verifier display map. Anyone citing the real boundedness modulus or the J-cost distance square bound needs this numerical identification. The proof unfolds the construction 1/(4·2) in ratio-orbit rationals and transports multiplication and reciprocal through toRat, then closes by norm_num.
Claim. Let $\delta$ be the fixed PRC rational boundedness threshold built as $1\cdot(4\cdot 2)^{-1}$ in the ratio-orbit quotient. Its ordinary rational display equals $1/8$: $\mathrm{toRat}(\delta)=1/8$.
background
Primitive Recognition Calculus (PRC) builds rationals as nonzero-denominator ratio-orbit quotient classes (PRCRat), identified by cross-multiplication. The map toRat is a verifier display sending each class to an ordinary $\mathbb{Q}$ value; it is a transport wrapper whose internal characterization is cross-multiplication.
The sibling definition PRCBoundednessDelta is a fixed PRC rational distance threshold, constructed as $1\cdot((2\cdot 2)\cdot 2)^{-1}$ so that a J-cost distance below it forces the ordinary increment square below one. The module sits in the real-boundedness-modulus layer of the foundation stack, after integer/rational scaffolding and real multiplication continuity.
Upstream simp lemmas toRat_mul and toRat_recip state that the display intertwines PRC multiplication and reciprocal with ordinary $\mathbb{Q}$ operations, which is exactly what lets the threshold evaluate numerically.
proof idea
One short tactic proof. Unfold the definition of the threshold (two := 1+1, four := twotwo, then 1(four*two)^{-1}). Apply the simp lemmas toRat_mul and toRat_recip so the display becomes ordinary arithmetic on $\mathbb{Q}$. Finish with norm_num, which reduces 1/(4·2) to 1/8.
why it matters
This numerical pin is the bridge from the abstract PRC threshold to concrete $\mathbb{Q}$ comparisons. Downstream, PRCBoundednessDelta_positive rewrites positivity via positive_iff_toRat_pos and this equality, then closes by norm_num. The main consumer PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta uses the same threshold: a J-cost distance strictly below $\delta$ forces $(a.toRat-b.toRat)^2<1$.
In the Recognition foundation, that square bound is the modulus step that keeps Cauchy targets controlled when lifting from PRC rationals toward real completeness. It is local scaffolding for the real-boundedness certificate, not a forcing-chain landmark (T5–T8), but it is required before the certificate can assert that small J-cost increments stay inside the unit square.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.