rational_product_increment_sq_lt
plain-language theorem explainer
On the rationals, if two pairs stay inside a square bound M and each coordinate moves by less than a tuned eta, the squared product difference stays below any prescribed rho. The eta is forced to be rho over 4(1+M squared). Analysts proving multiplication is continuous for the PRC J-cost distance on bounded sets cite this estimate. The proof splits the product increment, bounds each factor via a sibling square lemma, then closes with nlinarith and a field-simp scale check.
Claim. Let $a,a',b,b',M,\eta,\rho\in\mathbb{Q}$ with $M>0$, $\rho>0$, and $\eta=\rho/(4(1+M^2))$. Suppose $(a')^2<M^2$, $b^2<M^2$, $(a-a')^2<\eta$, and $(b-b')^2<\eta$. Then $(ab-a'b')^2<\rho$.
background
This module builds real-product continuity for the Primitive Recognition Calculus (PRC) from rational estimates. The ambient goal is continuity of multiplication with respect to the squared J-cost distance on bounded sets of reals constructed as regular sequences of rationals.
The local variables $\eta$ and $\rho$ here are ordinary positive rationals, not the framework constants $\rho=\varphi^{-1}$ or the unit-map embedding eta. Boundedness is expressed by squared comparisons $x^2<M^2$ rather than absolute values, matching the squared-display form of the PRC cost distance.
The sibling lemma product_factor_sq_lt supplies the elementary bound $(da\cdot b)^2<\eta M^2$ whenever $(da)^2<\eta$ and $b^2<M^2$. That factor estimate is the only nontrivial upstream arithmetic input; the rest is ring algebra and ordered-field arithmetic on $\mathbb{Q}$.
proof idea
Write the product increment as $ab-a'b'=u+v$ with $u=(a-a')b$ and $v=a'(b-b')$. Apply product_factor_sq_lt twice to get $u^2<\eta M^2$ and $v^2<\eta M^2$ (the second call uses commutativity to swap factors).
From nonnegativity of $(u-v)^2$, nlinarith yields $(u+v)^2\le 2u^2+2v^2$, hence $(u+v)^2<4\eta M^2$. Substitute the defining formula $\eta=\rho/(4(1+M^2))$ and clear the positive denominator by field_simp; another nlinarith step gives $4\eta M^2<\rho$. Transitivity finishes the claim.
why it matters
This private estimate is the quantitative heart of PRCJCostDistanceMulBoundedContinuityTarget_proved, which discharges the bounded-multiplication continuity target for the PRC J-cost distance. Without a uniform rational modulus of the form $\eta=\rho/(4(1+M^2))$, the passage from rational regular sequences to real multiplication continuity would stall.
In the Recognition Science foundation stack, real arithmetic continuity is prerequisite scaffolding for lifting the discrete forcing chain (T0–T8) and the Recognition Composition Law onto continuum observables. The certificate PRCRealProductContinuityCertificate packages the proved target for downstream modules that treat real products as continuous operations on cost space.
The result is pure ordered-field analysis; it does not itself invoke $\varphi$, eight-tick structure, or dimension forcing, but it closes a necessary analytic gap those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.