neg
plain-language theorem explainer
If x lies in the subfield of the reals generated by the golden ratio φ, then -x also lies in that subfield. Algebraists constructing the phi-ring or recognition categories cite this to verify additive inverses exist inside the closed set. The proof is a one-line wrapper that applies the subfield's built-in negation membership rule.
Claim. Let φ be the golden ratio. If x ∈ ℝ lies in the subfield generated by φ, then -x also lies in that subfield.
background
PhiClosed φ x means x belongs to the subfield of ℝ obtained by closing the singleton {φ} under field operations. The module RecogSpec.Core introduces this predicate together with phiSubfield to capture algebraic elements over φ for the recognition specification. Upstream negation results appear in integers and rationals constructed from logic as well as in interval arithmetic, but the direct dependency here is the subfield structure itself.
proof idea
One-line wrapper that applies the neg_mem property of the subfield generated by φ.
why it matters
This lemma supplies the additive inverse closure needed to turn the phi-subfield into a ring, feeding directly into PhiInt, J_at_phi, canonicalPhiRingObj, and PhiRingHom. It supports the algebraic backbone of the Recognition framework, including the cost algebra where J(φ) = (√5 - 2)/2 and the phi-ladder constructions. The result closes a basic step toward equipping recognition objects with group structure under addition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.