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

neg

show as:
view Lean formalization →

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.

claimLet φ 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  82lemma neg (hx : PhiClosed φ x) : PhiClosed φ (-x) :=

proof body

Term-mode proof.

  83  (phiSubfield φ).neg_mem hx
  84

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.