self
plain-language theorem explainer
The lemma asserts that for any real number φ, φ belongs to the subfield of the reals generated by φ. Algebraists constructing phi-based rings and physicists deriving constants in Recognition Science cite this membership when embedding the generator into algebraic extensions. The term-mode proof reduces the claim directly to subset closure of the generated subfield followed by simplification.
Claim. For any real number $φ$, $φ$ lies in the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x holds precisely when x belongs to the subfield generated by φ. The auxiliary definition phiSubfield φ constructs that subfield as the closure of the singleton set {φ} under the field operations of ℝ. This supplies the trivial base case for any construction that begins with the generator φ itself. The surrounding module RecogSpec.Core assembles these subfield facts as the algebraic substrate for later Recognition Science objects such as rings and constant derivations.
proof idea
The proof is a one-line term wrapper. It rewrites the goal to membership in phiSubfield φ and discharges the inclusion by applying Subfield.subset_closure together with a simplification tactic.
why it matters
This membership fact feeds directly into phiInt_sq, which verifies the relation φ² = φ + 1 inside the integer ring generated by φ, and into several climate and complexity results that rely on the same algebraic closure. It anchors the self-similar fixed-point property of φ at the T6 step of the forcing chain and supplies the starting point for the phi-ladder used in mass formulas and the alpha band bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.