PRCJCostDistanceMulBoundedContinuityTarget
plain-language theorem explainer
Exact product-continuity of multiplication in the J-cost metric, uniformly on bounded rational windows. Builders of Cauchy multiplication and product congruence for PRC reals cite this target as the local analytic input. It is a pure Prop packaging an epsilon-delta modulus; the discharging proof is supplied downstream.
Claim. For every positive rational $\varepsilon$ and every positive rational bound $B$, there exists a positive rational $\delta$ such that whenever rationals $a,a',b,b'$ all lie inside the bound window of radius $B$ and the $J$-cost distances satisfy $d_J(a,a')<\delta$ and $d_J(b,b')<\delta$, one has $d_J(ab,a'b')<\varepsilon$.
background
Primitive Recognition Calculus (PRC) rebuilds the ordered field of reals from an internal rational type equipped with the Recognition Science J-cost. The J-cost distance $d_J$ is the metric pulled back from $J(x)=(x+x^{-1})/2-1$ (the unique cost forced at T5 of the forcing chain). Bound windows InBound B restrict attention to rationals whose size is controlled by a positive rational $B$, so that multiplication stays inside a compact regime where a uniform modulus can exist.
This module sits after the complete ordered-field scaffolding and before full real multiplication. The local theoretical job is to isolate the exact analytic hypothesis needed for product Cauchy sequences and for multiplication congruence on null-closed reals: uniform continuity of $(a,b)\mapsto ab$ with respect to $d_J$, but only on each fixed bounded window.
Upstream order and positivity infrastructure on the internal rationals (strict order as nonnegative unbalanced difference, positive cone) supplies the quantifiers; no deeper arithmetic identity is assumed at the target level.
proof idea
Definitional packaging only: the declaration is a def equal to a single universally quantified Prop. There is no tactic proof and no lemma application here. The body writes the classical $\varepsilon$-$B$-$\delta$ modulus for four-point product continuity under $d_J$ on the bound window, using internal positivity and strict order on PRC rationals. Discharge happens later by the proved instance in RealProductContinuity.
why it matters
This target is the remaining analytic blocker once eventual boundedness of Cauchy sequences is in hand. Downstream, the conditional theorems for product Cauchy closure and product congruence both take it as a hypothesis and reduce the corresponding real-multiplication goals to eventual boundedness plus this modulus. The boundedness-modulus certificate explicitly records that after Step 10b, "the remaining multiplication blocker is only bounded product-continuity."
The product-continuity certificate then bundles the discharged target with mul-closure, mul-congruence, and a nonempty multiplication operation on null-closed reals, closing the real-multiplication package. In the broader RS foundation this is bookkeeping toward a recognition-native real field on which the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$) can act without importing classical $\mathbb{R}$ by fiat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.