physicallyReal_iff_deltaForced
plain-language theorem explainer
Physically real types are exactly the δ-forced ones: those that inject into the naturals. Anyone citing the RS demarcation between physical and non-physical carriers uses this bridge. The proof is pure definitional reflexivity, since the two predicates are the same Prop by construction.
Claim. For every type $X$, $X$ is physically real if and only if $X$ is $\delta$-forced, i.e., there exists an injection $X \hookrightarrow \mathbb{N}$.
background
In the primitive recognition calculus, a type is δ-forced when it carries an explicit countable certificate: a nonempty type of injections into $\mathbb{N}$. That is the formal content of being finitely generated, hence enumerable, from the act of distinction.
Physically real is the ontological reading of the same predicate. By thesis it coincides with δ-forced; the mathematical content lives entirely in the injection certificate, while the name records that this demarcation is the physical one.
The surrounding module builds a constructive, choice-free tower of such certificates (naturals, integers, rationals via ratio orbits), deliberately avoiding Mathlib encodings that depend on classical choice.
proof idea
One-line term proof: Iff.rfl. The left-hand side is defined to be identical to the right-hand side, so the biconditional holds by definitional equality. Marked @[simp] so rewrites collapse the ontological name to the injection predicate automatically.
why it matters
This is the naming bridge for the RS claim that physical reality lines up exactly with δ-forced carriers: only structures with an explicit countable certificate from distinction count as physically real. It sits at the head of the constructive δ tower (ℕδ → ℤδ → ℚδ) developed in the same module, which supplies choice-free injections for the integer and rational stages.
No downstream theorems currently depend on it (used_by is empty), so its role is conceptual and simp-facing: keep the ontological vocabulary interchangeable with the formal injection predicate wherever the foundation layer talks about physical carriers. It does not itself invoke the forcing chain T0–T8, the J-cost, or the eight-tick octave; it only fixes the demarcation language those later layers inherit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.