PRCJCostDistanceMulBoundedContinuityTarget_proved
plain-language theorem explainer
Given positive PRC-rationals ε and bound B, an explicit positive δ is produced so that J-cost-close, B-bounded factors have products within ε in J-cost distance. Downstream product-continuity and complete-ordered-field certificates cite it. The proof builds the modulus over PRC rationals, pushes inequalities through toRat, and closes with field_simp/nlinarith/positivity.
Claim. For every positive PRC-rational $\varepsilon$ and every positive PRC-rational bound $B$, there exists a positive PRC-rational $\delta=\delta(\varepsilon,B)$ such that if two pairs of PRC-rationals are each within $\delta$ in $J$-cost distance and the factors obey the $B$-bound, then the products lie within $\varepsilon$ in $J$-cost distance.
background
Primitive Recognition Calculus (PRC) builds a real-like carrier from rational data before promoting it to a complete ordered field. Distances are measured by the Recognition $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), not by absolute value; the local target is bounded continuity of multiplication in that metric.
The module sits under Foundation.PrimitiveRecognitionCalculus and imports the real boundedness modulus. Working objects are PRCRat values with a faithful toRat embedding into $\mathbb{Q}$, so positivity and arithmetic identities can be discharged on ordinary rationals and pulled back. Sibling lemmas relate $J$-cost increments to squared display quantities and control rational product increments under square bounds.
The local goal is the bounded multiplicative continuity hypothesis needed to close Cauchy multiplication and then promote the PRC reals.
proof idea
Tactic proof: introduce $\varepsilon,B>0$, then define the explicit modulus cascade over PRCRat:
$\rho=\varepsilon/(1+\varepsilon)$, $K=1+B^2$, $\eta=\rho/(4K)$, $\delta=\eta^2/(4(1+\eta))$.
Each auxiliary is identified under toRat (add/mul/recip lemmas, one_toRat) so $2\mapsto 2$, $4\mapsto 4$, and the displayed formulas match. Positivity of $\rho,\eta,\delta$ and $\rho<1$, $\eta<1$, plus $\rho^2/2<\varepsilon$, are proved by positivity, field_simp, and nlinarith.
The remainder (elided on the page) feeds $\delta$ into the sibling square/display comparison lemmas (product_factor_sq_lt, rational_product_increment_sq_lt, PRCJCostDistance_sq_lt_of_display_lt_delta, PRCJCostDistanceIncrementDisplay_lt_of_sq_lt) to conclude the product $J$-cost is $<\varepsilon$ whenever the factor distances are $<\delta$ under the $B$-bound.
why it matters
Multiplication must be continuous on bounded sets in the $J$-cost metric before PRC Cauchy sequences can be multiplied and the carrier promoted to a complete ordered field. This theorem discharges that continuity target with a fully explicit rational modulus.
It is wired directly into prc_real_product_continuity_certificate as the product_continuity field; that certificate also packages mul-closure from bounded continuity plus eventual boundedness of Cauchy sequences. The product certificate is then consumed by prc_real_complete_ordered_field_promoted_certificate, which assembles carrier, rational embedding, and additive/multiplicative closure into the promoted field package.
In the broader Recognition stack this is infrastructure, not a T0–T8 forcing step: it makes the PRC real model honest enough to host later continuum-level claims (measures, constants, continuum limits) without smuggling classical $\mathbb{R}$ continuity of multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.