of_nat
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.