no_injective_real_to_nat
plain-language theorem explainer
There is no injective map from the reals into the naturals: the continuum cannot embed into a countable discrete index set. Anyone building a countable state space for recognition orbits (or arguing that continuous configurations cannot inject into ledger ticks) cites this. The proof is a short cardinality reduction: an injection would make ℝ countable, contradicting uncountability of the continuum.
Claim. For every function $f : \mathbb{R} \to \mathbb{N}$, $f$ is not injective. Equivalently, there is no injection from the continuum into the natural numbers.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). T2 in that chain is discreteness: continuous structure cannot stabilize under the cost constraints that force a ledger.
This lemma is pure set-theoretic support for that discreteness story. It records that $\mathbb{R}$ is not injectable into $\mathbb{N}$. In Mathlib terms, existence of an injection $\mathbb{R}\to\mathbb{N}$ is equivalent to countability of $\mathbb{R}$, and the continuum is not countable.
Downstream, the canonical minimal orbit framework takes its closed observable state space to be $\mathbb{N}$. The present fact underwrites why a continuous real parameter cannot serve as a faithful discrete orbit index: any attempted embedding into naturals fails injectivity.
proof idea
Assume an injection $f:\mathbb{R}\to\mathbb{N}$. By the Mathlib equivalence countable_iff_exists_injective, that witness makes $\mathbb{R}$ countable. Instantiating the countable instance and applying Cardinal.not_countable_real to the universe set yields the contradiction. The argument is a direct cardinality reduction with no Recognition-specific algebra.
why it matters
In the forcing chain, T2 asserts that continuous configurations cannot stabilize under cost; the ledger and subsequent orbit structure live on discrete carriers. This theorem supplies the elementary obstruction: the continuum does not inject into $\mathbb{N}$.
It is consumed by canonicalMinimalOrbitFramework, which builds a closed observable framework whose state space is exactly $\mathbb{N}$ and carries the minimal hierarchy orbit. Choosing $\mathbb{N}$ as the canonical countable carrier is only coherent if continuous labels cannot be smuggled in injectively.
Relative to the primer landmarks, this sits under T2 (discreteness) and supports the later discrete ladder steps (T6 $\varphi$, T7 eight-tick, T8 $D=3$) by keeping the state space countable. It does not itself force $\varphi$ or the octave; it only blocks continuum-sized injective indexing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.