prc_real_mul_bounded_continuity_conditional_certificate
plain-language theorem explainer
Packages a conditional certificate that real multiplication on the PRC null-closed carrier reduces to two analytic targets: eventual boundedness of Cauchy sequences and bounded product continuity in J-cost distance. Foundation authors cite it when wiring the first-pass kernel or closing the real-field operations. The proof is a structure inhabitant: two fields by reflexivity, two by named conditional lemmas, and the mul operation via the null-closed product constructor.
Claim. There is a conditional certificate asserting that the PRC real multiplication targets reduce to eventual boundedness of Cauchy sequences together with bounded product continuity for the $J$-cost distance: the boundedness and product-continuity target equalities hold by definitional identity; from those two hypotheses one obtains product Cauchy closure, product congruence, and a well-defined multiplication operation on the null-closed PRC real carrier.
background
Primitive Recognition Calculus (PRC) builds a real carrier from Cauchy ledgers quotiented by null $J$-cost distance. The closed carrier PRCRealNullClosed is exactly that quotient: "Cauchy ledgers quotiented by null distance." Multiplication on the quotient is not free; it must be shown to preserve Cauchy-ness and to descend under null-distance equivalence.
The local module isolates two analytic obligations that unlock those algebraic facts: (i) every Cauchy sequence is eventually bounded, and (ii) products are continuous in a bounded way with respect to the $J$-cost distance. The structure PRCRealMulBoundedContinuityConditionalCertificate records that the full multiplication package (closure, congruence, and the induced operation) factors through those two targets.
Upstream, PRCRealMulClosureTarget_of_bounded_continuity and PRCRealMulCongruenceTarget_of_bounded_continuity already give the conditional proofs of product Cauchy closure and product congruence from the same pair of hypotheses.
proof idea
The proof inhabits the certificate structure field by field. Boundedness and product-continuity target fields are definitional equalities, discharged by rfl. Closure and congruence fields are the two upstream conditional theorems applied as function values. The multiplication-operation field is a short tactic: assume the two targets, apply each conditional theorem, and feed the resulting closure and congruence witnesses into PRCRealNullClosed.mulOf, which builds the quotient multiplication. No new analysis is done here; the certificate only wires existing lemmas.
why it matters
This certificate is the packaging step that lets the PRC real field obtain multiplication once the two analytic targets are supplied. Downstream it is consumed by kernel_first_pass_certificate (K7/A2: "the first-pass kernel certificate is inhabited"), so it sits on the path that certifies the kernel's first-pass surface. In the broader Recognition stack, a well-defined real multiplication on the null-closed carrier is prerequisite infrastructure for later forcing-chain and continuum constructions; without it the PRC reals cannot host the $J$-cost calculus or the self-similar fixed-point arguments that force $\varphi$. The declaration does not itself discharge the boundedness or continuity targets; it only records that they suffice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.