of_rat
The lemma establishes that the canonical embedding of any rational into the reals lies inside the subfield generated by an arbitrary real φ. Algebraic constructions in Recognition Science core would invoke this to ensure rationals remain inside phi-closed sets. The proof is a direct term-mode wrapper that rewrites the goal to algebraMap membership and applies the subfield's algebraMap_mem property.
claimFor every real number $φ$ and every rational $q$, the embedded value $q$ belongs to the subfield of $ℝ$ generated by $φ$.
background
PhiClosed φ x holds exactly when x lies in phiSubfield φ, the smallest subfield of the reals containing φ and obtained by taking the closure of the singleton set {φ}. The lemma appears in the RecogSpec.Core module, which develops basic algebraic closure properties for elements over the phi-generated subfield in support of observable payloads. It rests directly on the upstream definitions of PhiClosed (membership in the generated subfield) and phiSubfield (Subfield.closure of {φ}).
proof idea
The proof runs in term mode as a one-line wrapper. It first changes the goal to show that the image of q under the algebra map from ℚ to ℝ belongs to phiSubfield φ, then applies simpa to the algebraMap_mem fact supplied by the subfield structure.
why it matters in Recognition Science
This supplies the base case that all rationals are PhiClosed and is called by the of_nat and half lemmas to build further closed elements such as naturals and halves. It fills the algebraic foundation required for the Recognition Composition Law and phi-ladder constructions by keeping rational multiples inside the generated subfield. No open questions are closed here.
scope and limits
- Does not assert that irrational reals belong to the phi-subfield.
- Does not impose any equation or special property on φ beyond being real.
- Does not supply explicit basis elements or computational generators for the subfield.
- Does not extend the result to other base fields or number systems.
Lean usage
example (φ : ℝ) (q : ℚ) : PhiClosed φ (q : ℝ) := of_rat φ qformal 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