PRCRealMulCongruenceTarget_of_bounded_continuity
plain-language theorem explainer
Product congruence for PRC reals follows from eventual boundedness of Cauchy ledgers plus a local product-continuity modulus on bounded rational windows. Anyone assembling real multiplication from recognition calculus cites this reduction. The proof builds a common rational bound B from the four sequences, pulls a continuity delta, then takes a max index so all factors sit in-window and are delta-close in J-cost distance.
Claim. Assume every PRC Cauchy sequence is eventually bounded in a symmetric rational window, and that multiplication is continuous on bounded rational windows with respect to J-cost distance. Then multiplication is congruent on Cauchy sequences: whenever $u \equiv u'$ and $v \equiv v'$ as Cauchy ledgers, the products $uv$ and $u'v'$ are eventually arbitrarily close in J-cost distance for every positive rational $\varepsilon$.
background
Primitive Recognition Calculus builds reals from Cauchy ledgers over PRC rationals (quotient classes of ratio orbits, displayed into $\mathbb{Q}$ by toRat). Distance is measured by the J-cost metric on positive ratios, the same cost forced unique at T5 of the forcing chain.
Eventual boundedness says each Cauchy ledger $u$ admits a positive rational $B$ and an index past which every term lies in the symmetric window $(-B,B)$. Bounded product continuity supplies, for every positive $\varepsilon$ and window bound $B$, a positive $\delta$ such that if four rationals sit in that window and the two factor pairs are each $\delta$-close in J-cost, then the products are $\varepsilon$-close.
The local setting is the real-multiplication layer of PRC: congruence of products is the missing algebraic target once addition is already closed and congruent. The two named hypotheses are pure Prop targets; this theorem is the conditional bridge from those targets to product congruence.
proof idea
Tactic proof, not a wrapper. Fix four Cauchy sequences $u,u',v,v'$ with $u\equiv u'$, $v\equiv v'$, and a positive $\varepsilon$. From eventual boundedness extract positive bounds $B_u,B_{u'},B_v,B_{v'}$ and indices past which each sequence is in-window. Form the common bound $B:=B_u+B_{u'}+B_v+B_{v'}+1$; positivity and the four inequalities $B_\bullet\le B$ are discharged by transport to $\mathbb{Q}$ and nlinarith.
Invoke bounded product continuity at $(\varepsilon,B)$ to obtain $\delta>0$. Use Cauchy closeness of the two pairs at scale $\delta$ to get indices $N_{uC},N_{vC}$. Take $N$ as the max of all six indices (four bound indices, two closeness indices). For $n\ge N$, monotonicity of InBound under enlarging the bound places all four terms in the $B$-window, the factor pairs are $\delta$-close, and the continuity modulus yields the $\varepsilon$-closeness of the products.
why it matters
This is the congruence half of real multiplication in PRC. Downstream it is installed directly into the conditional certificate prc_real_mul_bounded_continuity_conditional_certificate (field mul_congruence_from_targets), and it is the congruence input used by prc_real_product_continuity_certificate once eventual boundedness and the continuity modulus are discharged. The promoted complete-ordered-field certificate also sits on this stack: without product congruence the real carrier cannot carry a well-defined multiplication on null-closed classes.
In the broader Recognition framework the result is infrastructure rather than a forcing-chain landmark: it lets the J-cost geometry on rationals lift to a field structure on the Cauchy completion, which is prerequisite for stating continuum-level claims (mass ladder, constants in RS-native units) over PRC reals rather than ad hoc analytic models. The companion closure theorem in the same module handles existence of the product ledger; together they reduce multiplication to two analytic targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.