ForcedTower
plain-language theorem explainer
The δ-only tower is the conjunction that ℕ, ℤ, and ℚ are physically real (δ-forced, choice-free). It is the discrete arithmetic floor of the public dual spine, cited by anyone packaging the δ-stratified forcing surface. The declaration is a bare Prop definition: three conjuncts, no proof work.
Claim. The naturals, integers, and rationals are each physically real: each type is $\delta$-forced. (The continuum cut $\neg\delta$-forced $\mathbb{R}$ is deliberately excluded from this package.)
background
PublicSpine is the public dual of UnifiedForcingChain: a δ-stratified map of what is forced, kept separate from the Boolean certificate spine for loop compatibility. Papers that mean "what is forced" are directed here rather than at UFC names as architecture claims.
Physically real is defined as exactly δ-forced: the ontological demarcation line is carried by DeltaForced, and the name records that this line is the physical one. The tower therefore asserts that the three discrete arithmetic types sit on the forced side of that line.
Panel K2 of the dual-surface contract forbids folding the classical continuum cut into the same δ-only package. Uncountability of ℝ lives under a classicalExtension tag, not under deltaOnly.
proof idea
Definition only: the body is the three-way conjunction that ℕ, ℤ, and ℚ each satisfy the physically-real (δ-forced) predicate. No tactics, no lemmas applied at this site. Inhabitation is discharged downstream by the tagged theorem that wraps this Prop.
why it matters
This is the first panel of the public dual spine. The tagged theorem forced_tower_holds inhabits it under StrengthTag.deltaOnly, and the dual-surface certificate structure PublicSpineCert requires that tagged inhabitant as its forced_tower field alongside continuum purchase, cost selection, φ-from-ι, and circle H₁.
In the Recognition forcing picture this is the discrete floor beneath the continuum cut and the later cost / φ / linking panels. It does not replace T0–T8 in UnifiedForcingChain; it retypes the arithmetic base as a δ-only claim so that classical ¬ℝ is not smuggled under the same strength tag. The D=3 / eight-tick bridge is handled elsewhere on this surface (Alexander linking closure), not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.