pith. machine review for the scientific record. sign in
lemma proved wrapper high

pow

show as:
view Lean formalization →

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 φ.

claimIf $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 in Recognition Science

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).

scope and limits

formal statement (Lean)

  96lemma pow (hx : PhiClosed φ x) (n : ℕ) : PhiClosed φ (x ^ n) := by

proof body

One-line wrapper that applies simpa.

  97  simpa using (phiSubfield φ).pow_mem hx n
  98

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.