deltaForced_rat
plain-language theorem explainer
The rationals carry an explicit injection into the naturals, so they are δ-forced (countably certified from distinction). Anyone citing the forced tower ℕδ → ℤδ → ℚδ or the physical-reality demarcation needs this top rung. The proof is a one-line term packing the paired certificate map and its injectivity.
Claim. The type $\mathbb{Q}$ is $\delta$-forced: there exists an injection $\mathbb{Q}\hookrightarrow\mathbb{N}$. Concretely, the map sending $q$ to the natural pairing of the $\delta$-forced code of its numerator with its denominator is injective.
background
In this module a type $X$ is $\delta$-forced when it carries a countable certificate: a nonempty injection $X\hookrightarrow\mathbb{N}$. That is the formal content of being finitely generated, hence enumerable, from the act of distinction. By thesis, physically real coincides with $\delta$-forced; the mathematical content lives entirely in the certificate.
The forced tower is built rung by rung. Naturals are trivially certified; integers are certified by an explicit bijection-style coding intToNat; rationals are certified by pairing that integer code of the numerator with the (already natural) denominator via dpair. The companion algebra paper presents this as $\mathbb{N}\delta\to\mathbb{Z}\delta\to\mathbb{Q}_\delta$, all choice-free.
Upstream, ratToNat is the explicit map $q\mapsto\mathrm{dpair}(\mathrm{intToNat},q.\mathrm{num},,q.\mathrm{den})$, and ratToNat_inj proves it injective by unpacking the pair, using injectivity of the integer coding, and reconstructing equality of rationals from equal reduced data.
proof idea
One-line term proof. DeltaForced ℚ is Nonempty (ℚ ↪ ℕ), so it suffices to exhibit an element of the function type. The term is the subtype pair ⟨ratToNat, ratToNat_inj⟩: the explicit pairing certificate together with the already-proved injectivity lemma. No tactics, no classical choice.
why it matters
This is the top of the constructive forced tower. Downstream, forcedTower packages deltaForced_nat, deltaForced_int, and this theorem into the choice-free conjunction that $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ are physically real. demarcation extends that conjunction by the classical non-certificate for $\mathbb{R}$, drawing the line: the $\delta$ tower is forced; the continuum is display-tier only.
In Recognition Science terms this formalizes which number systems arise by iterated distinction rather than by continuum completion. It does not itself invoke J-cost, $\varphi$, or the T0–T8 forcing chain, but it supplies the arithmetic substrate those later layers assume when they treat discrete certificates as ontologically prior to continuum displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.