prc_completion_strictly_extends_carrier
plain-language theorem explainer
The real completion contains a square root of 2, while the δ-native rational carrier (ratio orbits) has none: no verifier image in ℚ squares to 2. Anyone citing the carrier/completion gap without cost machinery uses this. The proof pairs existence of √2 in ℝ with irrationality of √2 against the rational display of any ratio orbit.
Claim. There exists a real $x$ with $x^2 = 2$, and there is no ratio orbit $q$ (integer numerator over nonzero orbit denominator) such that the real embedding of its rational display satisfies $(\mathrm{toRat}(q))^2 = 2$.
background
In the Primitive Recognition Calculus, the δ-native carrier is built from distinction and orbit data. A ratio orbit packages a signed-orbit numerator with a nonzero distinction-nat denominator; its verifier display toRat lands in ordinary ℚ. That display is only a transport wrapper: the internal equality is cross-multiplication.
The module separates strength layers for native cost uniqueness. One layer is the δ-only floor (kernel first pass); another is the continuous completion tagged traceClosure. The present claim is cost-independent: it compares the carrier to ℝ by asking whether √2 is expressible at all.
Upstream, ratio orbits and their rational displays supply the carrier side. Classical real analysis supplies √2 and its irrationality. No J-cost or d'Alembert hypothesis enters.
proof idea
Split the conjunction. Left conjunct: take $x = \sqrt{2}$ and apply Real.sq_sqrt with a numeric nonnegativity check. Right conjunct: assume some ratio orbit $q$ with $(\mathrm{toRat},q)^2 = 2$ in ℝ. Irrationality of $\sqrt{2}$ (irrational_sqrt_two) plus Real.sqrt_sq_eq_abs rewrites $\sqrt{2}$ as the absolute value of that rational cast. Feeding the absolute value back into the irrationality witness yields a rational equal to $\sqrt{2}$, a contradiction (via Rat.cast_abs).
why it matters
This is the algebraic root of the program's slogan that J is forced only on the continuous completion: the carrier cannot even name the limits the completion supplies, before any cost is discussed. Downstream, prc_full_stratification installs it as carrier_strictly_below_completion, discharging the stratification field-by-field with no project-local axioms.
It sits beside the cost-mediated gap prc_jcost_strength_separation: that result sees the same separation through J-forcing failure on the carrier and success on the completion. Here the gap is primitive and cost-free, and it underwrites the strength tag inequality StrengthTag.deltaOnly_lt_traceClosure. In the broader forcing chain this is foundation plumbing for why continuous completion (and later T5 J-uniqueness on that completion) is a genuine extension rather than a cosmetic rephrasing of δ-native data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.