of_rat
The lemma shows that the canonical embedding of any rational q into the reals lies inside the subfield generated by an arbitrary real φ. Researchers constructing algebraic bases for recognition models cite it to obtain the rational elements of that subfield. The proof is a one-line wrapper that coerces the goal to algebra-map membership and invokes the subfield's algebra-map membership property.
claimFor any real number $φ$ and rational $q$, the image of $q$ under the embedding $ℚ → ℝ$ belongs to the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x holds exactly when x lies in the subfield generated by φ, which is the smallest subfield of ℝ containing φ and closed under addition, multiplication, and inverses. The subfield itself is obtained by taking the field closure of the singleton set {φ}. This lemma belongs to the core specification module that equips the recognition parameter φ with its algebraic closure properties.
proof idea
The proof first rewrites the goal as membership of the algebra map image of q inside the generated subfield, then applies the algebra-map membership lemma of that subfield via simpa.
why it matters in Recognition Science
It supplies the rational elements required by the half lemma (which obtains closure under inversion of 2) and the of_nat lemma (which obtains closure under natural numbers). The result therefore anchors the algebraic structure used throughout the Recognition Science forcing chain by guaranteeing that the subfield generated by φ always contains ℚ.
scope and limits
- Does not prove that φ satisfies any particular minimal polynomial.
- Does not extend membership to elements outside the subfield generated by φ.
- Does not compute explicit basis elements or degrees of the extension.
Lean usage
have htwo : PhiClosed φ ((2 : ℚ) : ℝ) := of_rat φ 2formal statement (Lean)
64lemma of_rat (φ : ℝ) (q : ℚ) : PhiClosed φ (q : ℝ) := by
proof body
Term-mode proof.
65 change ((algebraMap ℚ ℝ) q) ∈ phiSubfield φ
66 simpa using (phiSubfield φ).algebraMap_mem q
67