rsField_mem_phi
plain-language theorem explainer
The golden ratio φ sits in the minimal RS field: the subfield of ℝ generated by the named constants {φ, π, e, α⁻¹}. Anyone citing the countable carrier for RS constants, the φ-ladder mass scaffold, or the continuum-avoidance headline uses this membership. The proof is a one-line wrapper: φ is literally a generator, so it lies in the subfield closure.
Claim. The golden ratio $\varphi$ belongs to the minimal Recognition-Science field $K_{\mathrm{RS}}\subseteq\mathbb{R}$, i.e. the subfield generated by the named constant set $\{\varphi,\pi,e,\alpha^{-1}\}$.
background
In this module the named RS constants are packaged as a finite set of reals: $\varphi$ (golden ratio), $\pi$, Euler's $e$, and the reciprocal fine-structure value $\alpha^{-1}$. The minimal field carrying RS physics is the subfield closure of that set inside $\mathbb{R}$. Because every subfield contains the prime field, the construction automatically includes $\mathbb{Q}$ and is exactly the adjunction of those constant values to the rationals.
The local claim is pure membership: the T6 fixed point $\varphi$ is one of the generators, so it is an element of that closure. Downstream work treats this field as the countable carrier for all named RS constant values and for the integer powers of $\varphi$ that scaffold the mass law.
proof idea
One-line wrapper. Apply Mathlib's Subfield.subset_closure: every element of a generating set lies in the subfield it generates. Unfold the definition of the constant set and discharge the membership goal by simp (φ is definitionally one of the four generators).
why it matters
This is the elementary generator fact that makes φ a countable-field citizen rather than a continuum-only real. It is re-exported as phi_in_minimal_field in the PRC chain bridge, where the doc-comment states that the T6 output φ lives in the minimal RS field and never requires the uncountable continuum (the weld between the forcing chain and the countable carrier).
It feeds four parents: soundness of FRS evaluation (eval_mem uses it on the phi constructor so every carrier term stays inside the field); the full φ-ladder theorem (rsField_phi_zpow), which places every integer power of φ in the field and thereby keeps the mass-law scaffold countable; and the Item 1 headline rs_physics_below_continuum, which packages countability of the field together with membership of φ, π, e, and α⁻¹. Framework landmark: T6 forces φ as the self-similar fixed point; this lemma places that forced constant inside the countable RS field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.