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

inv

show as:
view Lean formalization →

The lemma shows that if a real number x lies in the subfield generated by φ then its multiplicative inverse also lies in that subfield. Algebraic closure properties like this are invoked when constructing reciprocal quantities in Recognition Science calculations involving the golden ratio fixed point. The proof reduces immediately to the inverse membership axiom of the generated subfield.

claimIf $x$ belongs to the subfield of $ℝ$ generated by $φ$, then $x^{-1}$ also belongs to that subfield.

background

PhiClosed φ x asserts that x lies in phiSubfield φ, the smallest subfield of the reals containing φ, obtained via Subfield.closure on the singleton {φ}. This definition supplies the algebraic closure under field operations needed for elements built from the golden ratio. The lemma sits in RecogSpec.Core alongside sibling properties such as PhiClosed and phiSubfield, forming the basic toolkit for handling φ-generated quantities.

proof idea

The proof is a one-line term that applies the inv_mem property of the Subfield instance on (phiSubfield φ) directly to the hypothesis hx.

why it matters in Recognition Science

This closure under inversion feeds downstream results including toComplex_inv in ComplexFromLogic, zetaReciprocal differentiability and meromorphicity in EulerInstantiation, and automorphism compositions in RecogGeom.Symmetry. It supports algebraic manipulations required for the phi-ladder and self-similar fixed point in the Recognition framework (T5 J-uniqueness and T6).

scope and limits

formal statement (Lean)

  89lemma inv (hx : PhiClosed φ x) : PhiClosed φ x⁻¹ :=

proof body

Term-mode proof.

  90  (phiSubfield φ).inv_mem hx
  91

used by (18)

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

depends on (3)

Lean names referenced from this declaration's body.