zero
plain-language theorem explainer
The lemma establishes that zero belongs to the subfield generated by any real number φ. Developers formalizing algebraic invariants over φ in the Recognition Science specification layer would cite it as a base case. The proof is a direct one-line term that invokes the zero membership property of the generated subfield.
Claim. For every real number $φ$, the number $0$ lies in the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x asserts that the real x belongs to the subfield generated by φ, defined explicitly as membership in phiSubfield φ. The phiSubfield construction takes the smallest subfield of ℝ containing the singleton set {φ}, using the standard Subfield.closure operation from Mathlib.
proof idea
The proof is a one-line term that applies the zero_mem property of the Subfield instance for phiSubfield φ.
why it matters
The result supplies the zero base case for algebraic closure properties in the RecogSpec.Core module. It supports constructions that rely on the subfield remaining closed under field operations when building dimensionless packs and observable payloads. No downstream uses are recorded, and it touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.