inv_self
plain-language theorem explainer
The lemma shows that the inverse of any real φ lies inside the subfield generated by φ. Algebraic work on the phi-ladder and Recognition mass formulas cites this closure fact. The proof is a direct one-line wrapper that feeds the self-membership of φ into the general inverse-closure lemma.
Claim. For any real number $φ$, the multiplicative inverse $φ^{-1}$ belongs to the subfield generated by $φ$ via field operations.
background
PhiClosed φ x is the predicate that x lies in phiSubfield φ, the subfield generated by φ. The sibling self lemma records that φ itself satisfies this membership by direct subset closure. The sibling inv lemma states that the same subfield is closed under taking inverses, using the standard inverse_mem property of subfields.
proof idea
One-line wrapper that applies the inv lemma to the result of the self lemma for the given φ.
why it matters
Closure under inversion is required to keep the phi-subfield stable when mass formulas or Recognition Composition Law expressions involve reciprocals. It sits early in the RecogSpec.Core layer that supplies algebraic facts for the forcing chain and phi-ladder constructions. No downstream uses are recorded yet, indicating it functions as a basic building block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.