of_rat
plain-language theorem explainer
The lemma shows that the canonical embedding of any rational q into the reals lies inside the subfield generated by an arbitrary real φ. Researchers building algebraic closure properties for the phi-subfield cite this when constructing rational multiples and inverses inside Recognition Science calculations. The proof is a one-line term reduction that rewrites the goal to algebraMap membership and applies the subfield's algebraMap_mem property via simpa.
Claim. For any real number $φ$ and rational $q$, the image of $q$ under the embedding $ℚ → ℝ$ belongs to the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x is the proposition that x lies in the subfield generated by φ, defined explicitly as membership in phiSubfield φ. The phiSubfield φ is the smallest subfield of the reals containing φ, constructed as the closure of the singleton set {φ} under addition, multiplication, and inverses. This lemma appears in the RecogSpec.Core module, which assembles the basic membership facts needed to treat rational expressions in φ as closed under the Recognition framework's algebraic operations.
proof idea
The proof proceeds in term mode by a change tactic that rewrites the target as membership of (algebraMap ℚ ℝ) q in phiSubfield φ. It then finishes with a single simpa application of the algebraMap_mem lemma supplied by the Subfield instance for phiSubfield φ.
why it matters
This supplies the rational base case that downstream lemmas such as of_nat and half rely on to place natural numbers and the element 1/2 inside the phi-subfield. It thereby supports the algebraic manipulations required for the phi-ladder mass formula and the constants ħ = φ^{-5}, G = φ^5 / π in Recognition Science. The result closes a foundational gap in the subfield construction without touching the forcing chain T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.