continuum_is_purchase
plain-language theorem explainer
The continuum ℝ is not δ-forced: it admits no injection into ℕ. The claim is packaged under the classicalExtension strength tag, separating it from the choice-free ℕ/ℤ/ℚ tower. Anyone citing the public δ-stratified spine (panel K2) uses this cut. The proof is a one-line term wrapper around the classical uncountability lemma.
Claim. Under the classical-extension strength tag, $\mathbb{R}$ is not $\delta$-forced: there is no injection $\mathbb{R} \hookrightarrow \mathbb{N}$. Equivalently, the continuum carries no countable certificate of the form required for physical reality in the $\delta$-stratification.
background
PublicSpine is the public dual of UnifiedForcingChain: an honest δ-stratified map of what is forced versus what is purchased. A type is δ-forced when it carries an explicit countable certificate, i.e. a nonempty injection into ℕ. By thesis, physically real means exactly δ-forced.
The forced tower (ℕ, ℤ, ℚ) is choice-free and tagged deltaOnly. The continuum cut is deliberately separate: classical uncountability of ℝ is a fact about the display-tier object, not about the forced side. Panel K2 forbids conjoining ¬ℝ under the deltaOnly tag.
Upstream, not_deltaForced_real proves ¬DeltaForced ℝ by reducing a putative certificate to Countable ℝ, then to $|\mathbb{R}| \le \aleph_0$, which contradicts $\aleph_0 < \mathfrak{c}$. The full demarcation package conjoins the tower with this cut; this declaration isolates the continuum half.
proof idea
One-line term proof. The structure Tagged classicalExtension (¬ DeltaForced ℝ) is inhabited by setting the holds field to the existing theorem not_deltaForced_real. No new argument is constructed here; the classical cardinality contradiction (certificate ⇒ Countable ℝ ⇒ continuum ≤ ℵ₀, absurd) lives entirely upstream.
why it matters
This is the continuum half of the public dual forcing surface. Downstream, publicSpineCert_holds assembles the full PublicSpineCert by taking continuum_purchase := continuum_is_purchase alongside the δ-only tower, cost selection, φ-from-ι, and circle H₁.
In the Recognition framework the cut marks where classical set theory enters: the forced realm stops at ℚ; ℝ is a purchase, not a free theorem. That stratification keeps papers and loops honest about what δ alone delivers versus what classical uncountability buys. It does not touch T5–T8 (J-uniqueness, φ, eight-tick, D=3); those live on the linking and cost spines. The module contract is Lean-map honesty only: cite this surface for "what is forced."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.