rsField_mass_ladder
plain-language theorem explainer
Mass-ladder values formed as a yardstick times an integer power of the golden ratio stay inside the minimal RS subfield of the reals whenever the yardstick does. Anyone arguing that the RS mass spectrum lives in a countable field cites this closure. The proof is a one-line subfield multiplication step using the already-proved integer powers of φ.
Claim. If $y$ lies in the minimal RS subfield of $\mathbb{R}$ and $n\in\mathbb{Z}$, then $y\cdot\varphi^{n}$ also lies in that subfield, where $\varphi$ denotes the golden ratio.
background
The module constructs the minimal subfield of $\mathbb{R}$ that carries Recognition Science physics: the subfield closure of a named finite set of constants. That field automatically contains the prime field $\mathbb{Q}$ and every named RS constant (including $\varphi$, $\pi$, and $e$).
A prior lemma already places every integer power of $\varphi$ in the field, so the entire $\varphi$-ladder is countable-field content rather than continuum content. The RS mass law writes particle masses as yardstick times a power of $\varphi$ on that ladder; field closure under multiplication by those powers is the algebraic step that keeps every rung inside the same countable subfield.
proof idea
Term-mode one-liner. Invoke subfield multiplication-membership on the hypothesis that the yardstick lies in the field and on the lemma that every integer power of the golden ratio already lies in the field. No further arithmetic or induction is required.
why it matters
Recognition Science places masses on the $\varphi$-ladder via yardstick $\cdot\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. This theorem records that every such rung remains inside the minimal countable RS field once the yardstick does. Together with countability of the field, it underwrites the claim that the discrete mass spectrum never needs the continuum. The forcing chain already forces $\varphi$ as the self-similar fixed point (T6); the present lemma is the field-theoretic bookkeeping that keeps the mass ladder on that forced scaffold. No downstream users are wired yet; the result is infrastructure for later spectrum and countability arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.