rsConstants
plain-language theorem explainer
The finite seed set of named Recognition Science constants in ℝ: the golden ratio φ, π, Euler's e, and the RS inverse fine-structure value α⁻¹. Anyone constructing the minimal RS subfield cites this as the generator set. The body is a four-element set literal; no proof content.
Claim. Define the named RS constant set $C_{\mathrm{RS}} = \{\varphi, \pi, e, \alpha^{-1}\} \subset \mathbb{R}$, where $\varphi$ is the golden ratio, $e = \exp(1)$, and $\alpha^{-1} = 44\pi\,\exp\bigl(-w_8\ln\varphi/(44\pi)\)$ is the Recognition-Science inverse fine-structure constant.
background
In the Primitive Recognition Calculus minimal-field development, RS physics is not allowed to live on the full continuum. One first names a finite list of transcendental seeds, then takes the subfield of ℝ they generate. That subfield automatically contains ℚ (the prime field) and is the working home of φ-ladder arithmetic, eight-tick integers, and the assembled couplings.
The four seeds here are: golden ratio φ (the self-similar fixed point forced at T6), π, Euler's e, and the local α⁻¹. The local α⁻¹ is the explicit real $44\pi\exp(-w_8\ln\varphi/(44\pi))$, matching the canonical exponential-resummation form used elsewhere in the constants stack (seed $4\pi\cdot 11$ style identification, infrared CODATA match left open).
Upstream, related registries expose countable values sets of certified analytic expressions; the present definition is the hard-coded finite core those constructions refine.
proof idea
Pure definition: the set is the four-element literal ${\mathrm{Real.goldenRatio},,\mathrm{Real.pi},,\mathrm{Real.exp},1,,\alpha^{-1}}$. No tactics, no lemmas. Downstream finiteness is immediate from successive singleton inserts; countability follows from finiteness.
why it matters
This seed is the input to the minimal RS field: rsField is the subfield closure of these constants. Membership lemmas then place φ, π, e, and α⁻¹ inside that field by the closure subset property.
Finiteness and countability of the seed (rsConstants_finite, rsConstants_countable) feed the key structural claim that the RS field is countable, hence a proper subset of ℝ: the continuum is not the home of RS physics. The extension theorem shows adjoining any further countable family of constants keeps the closure countable, so the construction never requires the continuum no matter how many constants RS eventually names.
Framework landmarks touched: φ from the forcing chain (T6), α⁻¹ in the RS-native band near 137, and the broader program that certified analytic values stay countable (blocking continuum smuggling).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.