inv_pow_self
plain-language theorem explainer
The lemma shows that the reciprocal of any natural power of a real number φ remains inside the subfield generated by φ. Researchers handling phi-ladder constructions or dimensionless observables in Recognition Science would cite it to confirm closure under inversion. The proof is a one-line wrapper that feeds the output of the power-closure result into the inverse-closure lemma.
Claim. Let $φ ∈ ℝ$ and $n ∈ ℕ$. Then $(φ^n)^{-1}$ belongs to the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x means that x lies in the subfield generated by φ, closed under the field operations of addition, multiplication, and inversion. The module develops elementary closure properties for this subfield to support Recognition Science observables and algebraic manipulations of phi-powers. Upstream, pow_self shows φ^n itself belongs to the subfield for every natural n, while the separate inv result establishes that the subfield is closed under reciprocals via the inverse_mem property of phiSubfield.
proof idea
This is a one-line wrapper that applies the inv lemma directly to the result of pow_self φ n.
why it matters
The result supplies a basic algebraic closure step required for the phi-ladder mass formulas and for keeping dimensionless quantities inside the phi-generated field. It supports the Recognition Composition Law and the handling of inverses in unit equivalences and absolute packs. No immediate downstream theorems are recorded, yet the lemma closes an elementary operation needed before more complex constructions in the core specification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.