add
plain-language theorem explainer
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.
Claim. Let φ ∈ ℝ. 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.