PRCRealMulBoundedContinuityConditionalCertificate
plain-language theorem explainer
Conditional certificate packaging that PRC real multiplication (Cauchy closure of products, null-congruence, and a binary operation on the null-closed carrier) follows from eventual boundedness of Cauchy ledgers plus a local product-continuity modulus for the J-cost distance on bounded rational windows. Field-construction and first-pass kernel work cite it as the reduction interface. The structure is a Prop bundle of those reduction arrows; a companion theorem fills the fields by reflexivity and the two of-bounded-continuity lemmas.
Claim. A conditional certificate asserting that the multiplication targets for PRC reals reduce to two analytic hypotheses: (i) every Cauchy ledger is eventually bounded, and (ii) the $J$-cost distance admits a product-continuity modulus on bounded rational windows $[-B,B]$. From these one obtains: Cauchy-closure of pointwise products of ledgers; well-definedness of multiplication under null equivalence; and a nonempty binary multiplication map on the null-closed real carrier (Cauchy ledgers quotiented by null distance).
background
Primitive Recognition Calculus (PRC) builds a real carrier from Cauchy ledgers of PRC rationals, then quotients by null $J$-cost distance. The closed carrier is the type of null-closed reals: Cauchy ledgers modulo the proved null-distance transitive relation. Multiplication is not free: one must show that the pointwise product of two Cauchy ledgers is again Cauchy, and that null-equivalent inputs yield null-equivalent products, so the operation descends to the quotient.
Two exact blockers sit upstream. The mul-closure target asks that the raw pointwise product of any two Cauchy ledgers is Cauchy. The mul-congruence target asks that null equivalence is respected by that product. Both are expected to need eventual boundedness of Cauchy ledgers (every Cauchy sequence is eventually trapped in a symmetric rational window $[-B,B]$) together with a local continuity modulus for products in the $J$-cost distance on such windows.
This module isolates those two analytic inputs as named targets and records the reduction of the multiplication blockers to them.
proof idea
No proof body: this is a structure definition whose carrier is Prop. Five fields package the certificate. The first two are tautological equalities pinning the boundedness target and the product-continuity target as the named interfaces. The remaining three are implication fields: from eventual boundedness plus product continuity one gets mul-closure, mul-congruence, and a nonempty binary operation on the null-closed carrier. The companion theorem instantiates the structure by rfl on the two target pins and by the lemmas that derive closure and congruence from the bounded-continuity pair.
why it matters
Multiplication is the remaining algebraic gap once the PRC additive ordered structure is in place. This certificate is the explicit reduction interface: it states that the mul-closure and mul-congruence blockers (and hence a multiplication operation on null-closed reals) are discharged once eventual boundedness of Cauchy ledgers and the local $J$-cost product-continuity modulus are available. Downstream, the companion theorem builds a concrete instance of the certificate, and the first-pass kernel certificate bundles stage objects for the analytic specification chain. In the broader Recognition forcing picture this sits in the foundation layer that must supply a complete ordered field before constants, the $\phi$-ladder, and the T0--T8 chain can be interpreted on a finished real carrier. It does not close the analytic targets themselves; it freezes the contract those targets must meet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.