add
The add lemma asserts closure under addition for the subfield of reals generated by φ. Researchers constructing composite algebraic expressions over φ in Recognition Science calculations would cite it to combine phi-closed quantities. The proof is a direct one-line application of the subfield's add_mem property.
claimLet φ ∈ ℝ. If x and y belong to the subfield of ℝ generated by φ, then x + y also belongs to that subfield.
background
In RecogSpec.Core the definition phiSubfield φ constructs the smallest subfield of ℝ containing φ via Subfield.closure of the singleton {φ}. PhiClosed φ x is the membership predicate x ∈ phiSubfield φ, which encodes that x is obtained from φ by field operations. This supplies the algebraic setting for handling quantities closed under the golden-ratio subfield in the Recognition framework.
proof idea
The proof is a one-line wrapper that applies the add_mem operation of the subfield instance (phiSubfield φ) to the hypotheses hx and hy.
why it matters in Recognition Science
The lemma supplies the additive closure property required to build larger expressions inside the phi-subfield, forming a basic algebraic tool for Recognition Science constructions. It aligns with the self-similar fixed-point structure around φ and supports downstream handling of dimensionless packs and observable payloads. No immediate parent theorems are listed in the used-by graph, indicating its role as a foundational closure fact.
scope and limits
- Does not prove closure under multiplication or inversion.
- Does not specify any concrete numerical value for φ.
- Does not address continuity or topological closure of the subfield.
- Does not connect the algebraic property to physical mass or dimension formulas.
formal statement (Lean)
74lemma add (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
75 PhiClosed φ (x + y) :=
proof body
Term-mode proof.
76 (phiSubfield φ).add_mem hx hy
77