PRCRawCauchyRealizationTarget_proved
plain-language theorem explainer
Every raw rational Cauchy ledger packages as a Cauchy-sequence object whose underlying raw ledger is exactly that sequence. Completeness and null-distance quotient arguments in the Primitive Recognition Calculus cite this packaging step. The proof is a one-line structure introduction: store the Cauchy witness as a field; the raw projection is definitional.
Claim. For every raw rational ledger $s$, if $s$ is Cauchy then there exists a Cauchy sequence $u$ such that the raw projection of $u$ equals $s$.
background
In the Primitive Recognition Calculus, candidate reals are built from rational ledgers that satisfy a Cauchy condition. A raw rational ledger is the bare sequence of rationals; a Cauchy-sequence object pairs that ledger with a proof it is Cauchy. The forgetful raw map simply reads the term field of such an object.
The target proposition says every Cauchy raw ledger can be re-packaged into a full Cauchy-sequence object. That is the first step before forming the null-distance quotient that realizes the PRC real line.
The local setting is the RealCompleteness module in Foundation.PrimitiveRecognitionCalculus, which assembles the sharpened completeness certificate for that scalar field.
proof idea
Introduce the raw ledger $s$ and its Cauchy hypothesis. Build the Cauchy-sequence structure with term field equal to $s$ and cauchy field equal to the given hypothesis. The residual goal (raw projection equals $s$) is definitional reflexivity, because the raw map is exactly the term field.
why it matters
Feeds the quotient-point realization theorem: every raw rational Cauchy ledger determines a point of the final null-distance quotient (via packaging then Quot.mk under the null-distance setoid). Also fills the raw_cauchy_realization field of the sharpened real-completeness certificate, which bundles packaging, quotient points, and diagonal selection into one completeness witness for the PRC real line.
That certificate is the analytic substrate under Recognition Science foundation work: once the scalar field is complete, the forcing chain (T0–T8), the Recognition Composition Law, and the derived constants sit on a finished ordered field rather than on incomplete rational ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.