PhiClosed
plain-language theorem explainer
PhiClosed φ x asserts that the real number x belongs to the subfield of ℝ generated by φ. Researchers modeling algebraic dependence on the golden ratio in Recognition Science cite this predicate when verifying closure under arithmetic operations. The definition is a direct membership condition in the phiSubfield construction with no further steps required.
Claim. Let $φ ∈ ℝ$. A real number $x$ is $φ$-closed if $x$ lies in the subfield of $ℝ$ generated by $φ$.
background
The RecogSpec.Core module defines predicates for recognition specifications that remain invariant under field operations. Upstream, phiSubfield φ constructs the smallest subfield of ℝ containing φ via Subfield.closure of the singleton set {φ}. PhiClosed then marks membership in this subfield, supplying the algebraic domain for subsequent closure results.
proof idea
This declaration is a direct definition that sets PhiClosed φ x to x ∈ phiSubfield φ. No lemmas or tactics are applied; it functions as the base predicate from which all downstream closure lemmas are derived.
why it matters
PhiClosed underpins the closure lemmas add, div, inv, and half that preserve the predicate under field operations. These results maintain algebraic consistency around the self-similar fixed point φ in the Recognition Science framework and support manipulations on the phi-ladder. The definition fills a basic interface needed for expressions involving the eight-tick octave and derived constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.