PRCRawMul
plain-language theorem explainer
Pointwise product of two raw rational ledgers: at each index n the entries multiply in the underlying rational type. Anyone assembling the multiplicative structure on recognition reals from Cauchy ledgers cites this. The body is a one-line pointwise definition, not a proof.
Claim. Given raw completed-orbit rational ledgers $u,v:\mathbb{N}\to R$ (sequences of recognition rationals, before any Cauchy certificate), their product ledger is the pointwise product $(u\cdot v)(n)=u(n)\,v(n)$.
background
In the Primitive Recognition Calculus real-construction module, a raw rational ledger is simply a sequence $\mathbb{N}\to\mathrm{PRCRat}$: a completed-orbit ledger of rationals with no Cauchy proof attached yet. The forgetful map raw strips a Cauchy ledger down to this sequence.
The ambient goal is a complete ordered field of recognition reals, obtained by quotienting Cauchy ledgers by null distance measured with the J-cost metric (the same distance used for the Cauchy predicate). Addition and negation already have pointwise raw operations; multiplication is the remaining field operation at the raw level.
Upstream, the module sits on the finite-dimensional recognition register and the self-reference forcing apparatus, but this definition itself only needs the raw-ledger type and rational multiplication.
proof idea
Pure definition: return the function $n\mapsto u(n)\cdot v(n)$. No lemmas, no tactics, no Cauchy or null-equivalence reasoning. The algebraic work is deferred to the closure and congruence targets that consume this operation.
why it matters
This is the raw multiplicative skeleton for the recognition real field. Downstream, PRCRealMulClosureTarget asks exactly that pointwise products of Cauchy ledgers remain Cauchy under the J-cost distance, and PRCRealMulCongruenceTarget asks that null-equivalent inputs yield null-equivalent products. Both blockers note that eventual boundedness of Cauchy ledgers is the expected missing lemma.
Until those targets close, the quotient cannot carry a well-defined multiplication, so the ordered-field structure on recognition reals stays incomplete. The definition itself is not a forcing-chain step (T0–T8), but it is infrastructure for the real complete ordered field that later hosts mass ladders, constants, and continuum limits in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.