prc_real_product_continuity_certificate
plain-language theorem explainer
Packages a full product-continuity certificate for PRC reals: J-cost bounded continuity of multiplication, Cauchy closure under products, congruence under null distance, and a well-defined multiplication on the null-closed carrier. Downstream complete-ordered-field and kernel certificates cite it. The proof fills the four structure fields from already-proved bounded-continuity and eventual-boundedness targets.
Claim. There is a product-continuity certificate for the PRC real carrier: (i) multiplication is continuous in the $J$-cost distance on eventually bounded Cauchy ledgers; (ii) the termwise product of two $J$-cost Cauchy ledgers is again Cauchy; (iii) products respect null-distance equivalence; (iv) multiplication descends to a well-defined binary operation on the null-distance quotient of Cauchy ledgers.
background
Primitive Recognition Calculus builds a real carrier from Cauchy ledgers of PRC rationals, quotiented by null $J$-cost distance. The closed carrier is that quotient: Cauchy sequences identified when their $J$-cost separation vanishes. The $J$-cost is the Recognition cost $J(x)=(x+x^{-1})/2-1$, and the associated distance governs Cauchy and null relations.
Eventual boundedness of $J$-cost Cauchy ledgers is already proved: every such ledger is eventually trapped in a symmetric rational interval. Separately, bounded product-continuity of the $J$-cost distance is proved in this module: on a fixed bound $B$, small $J$-cost increments of the factors force a small $J$-cost increment of the product.
From those two facts, upstream lemmas give conditional product Cauchy-closure and product congruence. The certificate structure here simply records that the whole package is inhabited: continuity, closure, congruence, and a nonempty multiplication map on the null-closed carrier.
proof idea
Structure construction, not a fresh analytic argument. The product-continuity field is the already-proved bounded $J$-cost product-continuity target. Closure and congruence are obtained by applying the two conditional lemmas that take eventual boundedness plus bounded product-continuity and return mul-closure and mul-congruence. The multiplication operation field is a one-line existence proof: feed those same closure and congruence witnesses into the null-closed carrier's multiplication constructor, then wrap the result in a nonempty witness.
why it matters
Multiplication is the missing algebraic piece once addition and the ordered carrier are in place. This certificate is consumed by the promoted complete ordered field certificate, which lists add-closure, add-congruence, and the corresponding multiplicative data as fields of the promoted structure. It also appears in the first-pass kernel certificate path that records the inhabited kernel surface for the foundation layer.
In the Recognition forcing chain, a complete ordered real carrier is prerequisite infrastructure before continuum-level statements (dimension forcing, continuum limits of the eight-tick calculus) can be stated inside the formal development. Closing product continuity on the null quotient is the step that makes the PRC reals a field candidate rather than a mere additive ordered group of Cauchy classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.