PRCRealMulClosureTarget
plain-language theorem explainer
Names the exact multiplication-closure obligation for PRC reals: the pointwise product of any two Cauchy rational ledgers must itself be Cauchy in J-cost distance. Anyone assembling the null-quotient field structure or discharging the complete-ordered-field target bundle cites this Prop. It is a pure definition of a blocker, not a proved theorem; discharge is expected via eventual boundedness plus bounded product continuity.
Claim. The multiplication-closure target asserts: for every pair of PRC Cauchy sequences $u,v$, the raw ledger $n \mapsto u_n \cdot v_n$ is Cauchy, i.e. for every positive PRC rational $\varepsilon$ there exists $N$ such that for all $m,n \ge N$ the $J$-cost distance between the $m$-th and $n$-th product terms is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus real-completion layer, reals are null-quotients of Cauchy sequences of PRC rationals. A PRC Cauchy sequence is an orbit-indexed rational ledger whose $J$-cost distance eventually falls below every positive PRC rational tolerance. The raw Cauchy predicate is the same condition stated directly on bare ledgers Nat → PRCRat.
Pointwise multiplication of raw ledgers is the termwise product $(u \cdot v)(n) = u(n) v(n)$. For the null quotient to carry a well-defined multiplication, products of Cauchy ledgers must remain Cauchy, and the operation must respect null equivalence. This module packages those obligations as named Prop targets rather than proving them inline.
The ambient $J$-cost is the Recognition Science cost (T5 uniqueness: $J(x)=(x+x^{-1})/2-1$), used here as the metric on rational ledgers that drives the Cauchy condition.
proof idea
No proof: this is a def equating a name to a universal Prop. The body is simply ∀ u v : PRCCauchySeq, PRCRawCauchy (PRCRawMul u.raw v.raw). Downstream, PRCRealMulClosureTarget_of_bounded_continuity discharges it from eventual boundedness of Cauchy sequences plus a bounded product-continuity lemma on $J$-cost distance, by fixing $u,v,\varepsilon$, extracting bounds and Cauchy tails, and controlling the product distance.
why it matters
This is the exact multiplication blocker in PRCRealCompleteOrderedFieldTargets (mul_closure) and feeds the conditional complete-ordered-field certificate, the promoted Step 10 certificate, and the mul-bounded-continuity conditional certificate. Downstream doc-comments state that once eventual boundedness is proved, "the remaining multiplication blocker is only bounded product-continuity," and that product Cauchy closure follows from those two hypotheses.
Without this target closed, the null quotient cannot host a field multiplication, so the PRC real complete ordered field surface stays conditional. It sits in the foundation stack that eventually supports RS constants and the forcing chain's analytic layer, but it does not itself touch T5–T8 or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.