Floor_Demarcation
plain-language theorem explainer
Packages the full floor demarcation: naturals, integers, and rationals are physically real (δ-forced), while the reals are not. Cited by anyone using the public dual forcing surface who wants the tower-plus-continuum-cut as one Prop. The body is a four-conjunct definition, not a proof; the classical ℝ half is tagged via uncountability elsewhere.
Claim. The floor demarcation is the proposition that $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ are physically real (equivalently, $\delta$-forced) and that $\mathbb{R}$ is not physically real.
background
PublicSpine is the public dual of UnifiedForcingChain: a δ-stratified map of what is forced versus what is purchased. Papers that mean "what is forced" are directed here rather than at UFC certificate names.
Physically real is defined, by thesis, as exactly δ-forced: for a type $X$, the predicate is DeltaForced X. The tower half of the package is the δ-only claim that $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ sit under that predicate; the continuum cut places $\neg$ physically-real on $\mathbb{R}$ and is tagged as a classical extension (panel K2: do not put $\neg\mathbb{R}$ under δ-only).
The module contract keeps H₁(S¹;ℤ) ≅ ℤ and the closed D=3 / eight-tick Alexander linking bridge as theorems, while cost form and unit calibration remain purchases rather than free theorems.
proof idea
Definitional packaging only. The Prop is the four-way conjunction that $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ satisfy the physically-real (δ-forced) predicate and that $\mathbb{R}$ does not. No tactics, no lemmas applied at this site; inhabitation is deferred to the tagged theorem that asserts the package holds under classical extension.
why it matters
Gives a single named Prop for the full demarcation (δ-only tower plus continuum cut) so the dual surface can cite one object rather than two. Downstream, floor_demarcation_holds tags it as a classical-extension strength claim and supplies the witness.
Doc guidance: prefer citing the split pair (forced tower holds, continuum is purchase) when δ-only versus purchase must stay separate; use this package when the combined floor cut is the citation target. It sits beside cost-selection, φ-from-ι, and the closed Alexander linking bridge on the same public spine, keeping UFC as certificate/floor witness rather than architecture claim.
No open scaffold here: the definition is closed; only the classical tag on the ℝ half records the uncountability route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.