phiSubfield
plain-language theorem explainer
Definition of the subfield of the reals generated by a fixed real φ. Recognition Science proofs that track algebraic closure under addition and inversion cite this when establishing PhiClosed sets. The construction is a direct one-line application of the Subfield closure operator to the singleton containing φ.
Claim. Let $φ ∈ ℝ$. The subfield generated by $φ$ is the smallest subfield of $ℝ$ that contains $φ$ and is closed under the field operations.
background
RecogSpec.Core supplies the algebraic scaffolding for recognition specifications. The predicate PhiClosed φ x holds exactly when x belongs to this subfield. The definition relies on Mathlib's Subfield type and its closure constructor; no other module hypotheses are invoked in the body itself.
proof idea
One-line wrapper that applies Subfield.closure to the singleton set containing φ.
why it matters
The definition supplies the carrier for the PhiClosed predicate and its closure lemmas (add, mul, inv, div, neg) in the same module. Those lemmas feed Recognition Science results that require φ to remain inside an algebraically closed set, including the phi-ladder mass formula and the self-similar fixed point from the T6 step of the forcing chain. It supplies the concrete algebraic setting in which the eight-tick octave and D = 3 are later expressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.