rsField_dimension
plain-language theorem explainer
The forced spatial dimension D = 3 is an element of the minimal RS subfield of the reals. Anyone citing the forcing chain (T8) or the countable-carrier claims needs this membership. The proof is a one-line cast: every subfield contains the naturals, hence contains 3.
Claim. The real number $3$ belongs to the minimal Recognition Science field $K_{\mathrm{RS}} \subseteq \mathbb{R}$, i.e. the subfield generated by the named RS constants (which already contains $\mathbb{Q}$).
background
In the Primitive Recognition Calculus, physics is required to live on a countable carrier rather than the full continuum. The object rsField is defined as the subfield of $\mathbb{R}$ generated by a finite named constant set; as a subfield it automatically contains the prime field $\mathbb{Q}$ and therefore every natural number.
The forcing chain (T0–T8) outputs three integer-scale landmarks: the golden ratio $\varphi$ (T6), the eight-tick octave $8 = 2^3$ (T7), and the spatial dimension $D = 3$ (T8). This lemma records that the last of those outputs is already inside the minimal field, with no extra generators required.
Upstream, the field is just Subfield.closure of the constant set, so ordinary field axioms (and the Mathlib fact that naturals embed into every subfield of $\mathbb{R}$) apply directly.
proof idea
One-line term proof. Apply the Mathlib fact that every natural number, cast to $\mathbb{R}$, lies in any Subfield ℝ, specialized to the generator set of the RS field and to $n = 3$. The exact_mod_cast tactic discharges the $\mathbb{N}\to\mathbb{R}$ coercion.
why it matters
T8 of the Unified Forcing Chain forces $D = 3$ spatial dimensions. This lemma places that integer inside the countable RS field, so the chain never leaves a countable carrier.
It is consumed by three parents: rs_chain_all_rungs_in_field (Item 3: every named chain output—$\varphi$, 8, and 3—lands in the field), rs_scaffold_below_continuum (Item 1: the scaffold carries the $\varphi$-ladder, eight-tick, and dimension while remaining a proper countable subset of $\mathbb{R}$), and the top-level prc_shrunk_certificate that packages the seven δ-program headlines. Without this membership, the “below continuum” and “chain on a countable carrier” claims would have a hole at the dimension rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.