PhysicallyReal
plain-language theorem explainer
A type is physically real exactly when it is δ-forced: it carries an explicit injection into the naturals. The name is pure ontology; the math is the countable-certificate predicate. Anyone citing the forced tower (ℕ, ℤ, ℚ) or the continuum cut uses this label. The body is definitional equality, not a proof.
Claim. For any type $X$, $X$ is physically real if and only if there exists an injection $X \hookrightarrow \mathbb{N}$ (i.e., $X$ is $\delta$-forced).
background
In the primitive recognition calculus, a type is δ-forced when it carries an explicit countable certificate: a nonempty type of injections into ℕ. That is the formal content of "finitely generated, hence enumerable, from the act of distinction."
This module sits under Foundation and imports the omniscience layer. The local thesis is that physical reality coincides with what the δ-act can force into an enumerable carrier. Continuum objects sit outside that cut unless a separate purchase is made.
Upstream, the entire mathematical content is the δ-forced predicate itself. The present name only records the ontological reading that the demarcation line drawn by countability is the physical one.
proof idea
One-line definitional abbreviation: the predicate is identical to δ-forced. No tactics, no lemmas. The companion simp lemma is definitional iff (Iff.rfl).
why it matters
This name is the public face of the δ-cut. Downstream, the choice-free forced tower asserts that ℕ, ℤ, and ℚ are physically real via explicit certificates; demarcation adds the classical conjunct that ℝ is not. PublicSpine packages both as ForcedTower and Floor_Demarcation for panel citation (K2: keep ¬ℝ off the δ-only side).
In the Recognition framework this is the floor under the forcing chain: only δ-enumerable carriers count as physically real before continuum purchase. It does not itself force φ, the eight-tick octave, or D = 3; those sit higher in T6–T8. It fixes the ontological vocabulary those later steps inherit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.