rsConstants_finite
plain-language theorem explainer
The named Recognition Science constants form a finite subset of the reals: golden ratio, π, Euler's e, and α⁻¹. Anyone constructing the minimal RS constant field or proving its countability cites this. The proof unfolds the four-element set definition and chains Mathlib finite-singleton and insert lemmas.
Claim. The set $\{\varphi, \pi, e, \alpha^{-1}\} \subset \mathbb{R}$ is finite, where $\varphi$ is the golden ratio, $e = \exp(1)$, and $\alpha^{-1}$ is the reciprocal fine-structure constant used in the RS native units.
background
In the Primitive Recognition Calculus minimal-field module, the named RS constants are packaged as a single set of reals: golden ratio $\varphi$, $\pi$, Euler's $e$, and $\alpha^{-1}$. The module's goal is the minimal subfield of $\mathbb{R}$ generated by those values (automatically containing $\mathbb{Q}$ as prime field), written as the subfield closure of that set.
Finiteness of the generator set is the elementary first step before countability of the generators and of the generated subfield. Mathlib supplies Set.Finite for finite subsets of any type, with finite_singleton and insert preserving finiteness under adjoining one element at a time.
proof idea
Term-mode proof: unfold the definition of the constant set to the explicit four-element set literal, then apply Set.finite_singleton to the first point and chain three .insert applications. Each insert of a finite set remains finite, so the whole set is finite. No arithmetic or RS-specific lemmas are needed.
why it matters
This is the finiteness seed for the RS constant field. Downstream, rsConstants_countable is the one-line rsConstants_finite.countable, and rsField_countable applies subfield_closure_countable_of_finite to the same fact, proving the minimal field carrying RS physics is a countable subset of $\mathbb{R}$.
In the framework, the generators include $\varphi$ (forced at T6 as the self-similar fixed point) and $\alpha^{-1}$ (constrained to the RS band near 137). Countability of the constant field keeps the algebraic skeleton of RS physics separable and free of uncountable parameter junk, which matters when adjoining ladder values and comparing to measured constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.