forcedTower
plain-language theorem explainer
The discrete tower of natural numbers, integers, and rationals is physically real in the Recognition sense: each type is δ-forced by an explicit, choice-free certificate. Anyone citing the constructive half of the continuum cut (ℕδ → ℤδ → ℚδ built, not posited) points here. The proof is a three-conjunct term packing the three prior δ-forced lemmas.
Claim. The types $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ are each physically real, where physically real means $\delta$-forced (there exists an injective certificate into $\mathbb{N}$). The conjunction is proved without classical choice.
background
In the Primitive Recognition Calculus, a type $X$ is $\delta$-forced when it carries an explicit injective certificate into $\mathbb{N}$. The ontological gloss PhysicallyReal is definitionally identical to that predicate: physical reality, by thesis, is exactly $\delta$-forcedness.
The module isolates the positive tower from the continuum cut. Naturals are their own certificate (the identity embedding). Integers use an explicit even/odd pairing into $\mathbb{N}$. Rationals use an explicit paired certificate (the top of the companion-algebra tower $\mathbb{N}\delta \to \mathbb{Z}\delta \to \mathbb{Q}_\delta$). All three constructions are choice-free.
The local setting is the demarcation line of Recognition Science foundation work: the discrete tower is built; the continuum $\mathbb{R}$ is display-tier and is handled separately via classical uncountability.
proof idea
One-line term proof. The goal is the three-way conjunction of PhysicallyReal on $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$. Because PhysicallyReal unfolds to DeltaForced, the proof is the triple
$\langle$ deltaForced_nat, deltaForced_int, deltaForced_rat $\rangle$.
Each conjunct is already proved upstream: identity embedding for $\mathbb{N}$; even/odd certificate for $\mathbb{Z}$; paired certificate for $\mathbb{Q}$. No new algebra is done here.
why it matters
This is the exact formal residue of the claim that the $\delta$ tower is constructed rather than posited. Downstream, PublicSpine.forced_tower_holds packages it under the deltaOnly strength tag, keeping classical choice out of the positive spine.
The companion demarcation note in the module states that $\mathbb{R}$ is not $\delta$-forced; that negative half lives under a classicalExtension tag. Together the two halves draw the foundation cut between forced discrete structure and display-tier continuum.
In the broader Recognition chain this supports the constructive side of the forcing program (T0–T8 landmarks sit on discrete, certificate-bearing structure). It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only certifies that the number tower those later steps act on is physically real in the $\delta$ sense.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.