of_nat
Natural numbers embedded into the reals lie inside the subfield generated by any real φ. Workers extending algebraic closure results from rationals to integers in Recognition Science constructions cite this step. The proof is a one-line wrapper that reduces the natural case to the rational case via simpa on the of_rat lemma.
claimFor any real number $φ$ and natural number $n$, the real embedding of $n$ belongs to the subfield generated by $φ$, that is $n ∈ phiSubfield(φ)$.
background
PhiClosed φ x is the proposition that x lies in phiSubfield φ, the subfield of ℝ generated by φ under field operations. The upstream lemma of_rat shows that every rational q satisfies PhiClosed φ (q : ℝ) by verifying that the algebra map from ℚ lands inside phiSubfield φ. This lemma appears in the Core module of RecogSpec, which records basic membership facts needed for observable payloads.
proof idea
The proof is a one-line wrapper that applies of_rat φ n. The simpa tactic automatically handles the coercion from ℕ to ℚ to ℝ and discharges the resulting membership goal.
why it matters in Recognition Science
The lemma supplies the natural-number case of PhiClosed, completing the integer fragment of the subfield membership results that feed algebraic constructions in the Recognition framework. It builds directly on of_rat and aligns with the requirement that constants and ladder rungs remain inside the φ-generated subfield. No downstream uses are recorded yet.
scope and limits
- Does not prove closure of phiSubfield under operations outside the field axioms.
- Does not address membership for real numbers outside the subfield generated by φ.
- Does not depend on φ satisfying any specific equation such as the golden-ratio relation.
- Does not supply explicit generators or basis elements for phiSubfield.
formal statement (Lean)
108lemma of_nat (φ : ℝ) (n : ℕ) : PhiClosed φ (n : ℝ) := by
proof body
One-line wrapper that applies simpa.
109 simpa using of_rat φ n
110