rsField_proper

In the Primitive Recognition Calculus minimal-field module, the RS constant field is the subfield of $\mathbb{R}$ obtained by closing the finite set of named constants under field operations. That set automatically contains $\mathbb{Q}$ (the prime field) and the concrete constant values that appear in the framework (including $\varphi$, $\pi$, $e$, and the inverse fine-structure constant). Upstream, the same module proves that this field, viewed as a set of reals, is countable: finite generators yield a countable subfield closure.

The surrounding Item 1 programme asks whether the continuum is required as the home of RS physics. Countability alone does not yet say the field is proper; one still needs that $\mathbb{R}$ itself is uncountable. That is the local gap this theorem fills.

Term-mode proof by contradiction. Assume the constant field equals $\mathrm{Set.univ}$ as subsets of $\mathbb{R}$. Transport the already-proved countability of the field along that equality to conclude that the universe of reals is countable. Discharge with the standard Mathlib fact that $\mathbb{R}$ is not countable. No field-theoretic computation is needed beyond the prior countability lemma.

This is the properness half of Item 1: every named RS constant lives in one countable subfield strictly below the continuum, so the uncountable real line is not required as the home of the constants. Downstream, the headline theorem packages countability together with membership of $\varphi$, $\pi$, $e$, and $\alpha^{-1}$; the sharpened scaffold theorem adds the full $\varphi$-ladder, the eight-tick integer, dimension three, and re-uses properness explicitly. In the forcing-chain picture this supports the claim that the discrete RS scaffold (T6 $\varphi$, T7 eight-tick, T8 $D=3$, and the $\alpha$ band) can sit inside a countable field without ever needing the full continuum as ambient codomain.