PRCRealProductContinuityCertificate
plain-language theorem explainer
Certificate packaging the four ingredients for multiplication on the PRC real carrier (Cauchy ledgers modulo null distance): a bounded J-cost product-continuity modulus, Cauchy closure of pointwise products, null-distance congruence of products, and existence of the induced multiplication map. Downstream ordered-field and kernel first-pass certificates cite it. Pure Prop structure with no proof body; inhabited by a sibling theorem that discharges each field.
Claim. A product-continuity certificate is the conjunction of four claims: (i) multiplication is continuous on bounded rational windows in the $J$-cost distance (for every $\varepsilon,B>0$ there is $\delta>0$ controlling products inside the window $B$); (ii) the pointwise product of two Cauchy ledgers is Cauchy; (iii) null-equivalent Cauchy ledgers have null-equivalent products; (iv) there exists a binary multiplication map on the null-closed real carrier.
background
Primitive Recognition Calculus builds an internal real carrier from Cauchy ledgers of PRC rationals, then quotients by null distance. The closed carrier is the type of those equivalence classes. Multiplication is not free: one must show pointwise products stay Cauchy, descend to the quotient, and are continuous in the native cost geometry.
The cost geometry is the $J$-cost distance on rationals (from the Recognition Composition Law and T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). The local analytic input is a bounded product-continuity modulus: on any positive bound $B$, small $J$-cost increments of the factors force a small increment of the product. Upstream targets isolate exactly the blockers: Cauchy closure of raw products, and congruence of raw products under null equivalence, both expected to need eventual boundedness of Cauchy ledgers.
This module sits in the foundation layer that promotes the null quotient toward a complete ordered field, before Mathlib typeclass packaging.
proof idea
No proof body: the declaration is a structure extending Prop whose four fields are named targets. Inhabitation is deferred to the sibling theorem, which fills product_continuity by the proved bounded-continuity modulus, obtains mul_closure and mul_congruence from that modulus plus eventual boundedness of Cauchy sequences, and supplies mul_operation as a nonempty witness for the induced map on the null-closed carrier.
why it matters
Multiplication is the hard half of the field structure on the PRC real carrier; addition has a parallel certificate path. This bundle is the exact product-side input to the promoted Step 10 complete ordered-field certificate, which requires closed operations and theorem surfaces on the null quotient (full Mathlib instances later). It also feeds the first-pass PRC kernel certificate that records concrete Lean objects for each stage of the early theorem chain.
In the Recognition forcing chain, a well-defined continuous product on the cost-geometric reals is prerequisite infrastructure for later analytic work (constants, mass ladder, continuum limits), even though this certificate itself does not yet force $\phi$, the eight-tick octave, or $D=3$. It closes the product-continuity scaffolding slot rather than an open physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.