pow_self
plain-language theorem explainer
The lemma shows that any natural power of φ remains inside the subfield generated by φ. Workers on the Recognition Science phi-ladder cite it when they need to keep iterated powers algebraically closed under the base. The proof is a one-line wrapper that feeds the self lemma directly into the general pow closure result.
Claim. Let $φ ∈ ℝ$ and $n ∈ ℕ$. Then $φ^n$ belongs to the subfield generated by $φ$.
background
PhiClosed φ x is the predicate that x lies in the subfield phiSubfield φ generated by φ. The self lemma records that φ itself satisfies this predicate. The pow lemma records that if x is closed then every natural power x^n is also closed.
proof idea
The proof is a one-line wrapper that applies the pow lemma to the result of the self lemma.
why it matters
It supplies the forward power step that the downstream inv_pow_self lemma consumes. In the Recognition framework this algebraic closure supports the phi-ladder used for mass formulas and the T5 J-uniqueness construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.