PRCRealMulClosureTarget_of_bounded_continuity
plain-language theorem explainer
If every PRC Cauchy sequence is eventually bounded and multiplication is continuous on bounded rational windows in J-cost distance, then the product of two Cauchy sequences is Cauchy. Real-field promotion and product-continuity certificates cite this as the mul-closure step. The proof picks a joint bound B, pulls a continuity modulus delta, then takes a common Cauchy index past the bound and modulus thresholds.
Claim. Assume every Cauchy sequence of PRC rationals is eventually bounded, and that for every $\varepsilon>0$ and bound $B>0$ there is a modulus $\delta>0$ making multiplication continuous on the window $[-B,B]$ in J-cost distance. Then for any two Cauchy sequences $u,v$ and any $\varepsilon>0$ there exists $N$ such that for all $m,n\ge N$, the J-cost distance between $u_m v_m$ and $u_n v_n$ is less than $\varepsilon$.
background
Primitive Recognition Calculus (PRC) builds arithmetic from recognition ledgers before promoting to a complete ordered field. Here the carrier pieces are PRC rationals (PRCRat), with Cauchy sequences of those rationals as the raw material for reals.
Eventual boundedness says every Cauchy ledger $u$ admits $B>0$ and an index past which all terms lie in the symmetric window $[-B,B]$ (PRCRat.InBound). Bounded product-continuity supplies, for each tolerance $\varepsilon$ and window radius $B$, a positive $\delta$ so that if $a,a',b,b'$ stay inside $[-B,B]$ and the J-cost distances $d_J(a,a')$ and $d_J(b,b')$ are both $<\delta$, then $d_J(ab,a'b')<\varepsilon$. The J-cost distance is the metric pulled from the Recognition cost $J$, the unique generator forced at T5 of the forcing chain.
The target discharged here is product Cauchy closure: the pointwise product of two Cauchy sequences must itself be Cauchy. That is the analytic gate needed before multiplication descends to equivalence classes of Cauchy sequences.
proof idea
Tactic proof, not a wrapper. Fix Cauchy sequences $u,v$ and $\varepsilon>0$. From eventual boundedness extract positive bounds $B_u,B_v$ and indices past which $u$ and $v$ stay inside those windows. Set $B:=B_u+B_v+1$ and check $B>0$ with $B_u,B_v\le B$ via the rational embedding and nlinarith.
Feed $\varepsilon$ and $B$ into the product-continuity hypothesis to obtain a modulus $\delta>0$. Cauchy-ness of $u$ and $v$ at scale $\delta$ yields indices $N_u^C,N_v^C$. Take $N$ as the max of the two bound indices and the two Cauchy indices.
For $m,n\ge N$, monotonicity of InBound places all four terms $u_m,u_n,v_m,v_n$ inside $[-B,B]$, while the Cauchy tails give $d_J(u_m,u_n)<\delta$ and $d_J(v_m,v_n)<\delta$. Apply the continuity witness directly to conclude $d_J(u_m v_m,u_n v_n)<\varepsilon$.
why it matters
Multiplication on the PRC real completion is well-defined only after Cauchy sequences are closed under products and the operation respects the Cauchy equivalence. This theorem is the conditional closure half of that pair (its sibling handles congruence).
Downstream, prc_real_mul_bounded_continuity_conditional_certificate packages it with the congruence half as the mul-closure field of the conditional certificate. prc_real_product_continuity_certificate instantiates the same arrow once eventual boundedness and the continuity target are proved, feeding the product-continuity certificate. The promoted complete-ordered-field certificate chain (prc_real_complete_ordered_field_promoted_certificate) needs mul-closure among the field operations on the null-closed real carrier.
In framework terms this is infrastructure under the real arithmetic that later carries the phi-ladder mass formula and the RS-native constants, not a forcing-chain landmark itself. It closes the analytic gap between rational J-cost continuity and Cauchy-real multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.