pow
plain-language theorem explainer
The lemma shows that if a real number x lies in the subfield generated by φ, then any natural power x^n also lies in that subfield. Analysts working with algebraic closures in Recognition Science models cite this result when propagating phi-closure through polynomial expressions. The proof reduces immediately to the built-in pow_mem property of the Subfield instance for phiSubfield φ.
Claim. If $x$ belongs to the subfield of $ℝ$ generated by $φ$, then for every natural number $n$, $x^n$ also belongs to that subfield.
background
In the RecogSpec.Core module, phiSubfield φ is defined as the smallest subfield of the reals containing φ, obtained by closing the singleton set {φ} under field operations. PhiClosed φ x is the proposition that x lies in this subfield. This setup supports algebraic manipulations involving the golden ratio φ in the Recognition Science framework, where φ appears as the self-similar fixed point (T6).
proof idea
The proof is a one-line wrapper that invokes the pow_mem lemma from the Subfield structure on (phiSubfield φ), applied to the hypothesis hx and the exponent n, with simpa handling the simplification.
why it matters
This closure property under natural powers feeds into downstream results such as energy_conservation in Action.Hamiltonian and various ODE uniqueness theorems in Cost.AczelProof, Cost.AczelTheorem, and Foundation.DAlembert.AnalyticBridge. It ensures that powers of phi-closed quantities remain within the algebraic structure generated by φ, supporting the phi-ladder and mass formulas in the Recognition Science chain (T5-T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.