rs_physics_below_continuum
plain-language theorem explainer
Every named Recognition Science constant (φ, π, e, and α⁻¹) lives in one countable proper subfield of ℝ, so the framework's constant codomain never needs the full continuum. Anyone citing the PRC “below continuum” headline or the δ-program certificate would point here. The proof is a six-conjunct term packing prior countability, membership, and properness lemmas.
Claim. Let $K \subset \mathbb{R}$ be the Recognition Science constants field (the subfield generated by the named RS constants). Then $K$ is countable, $\varphi \in K$, $\pi \in K$, $e \in K$, $\alpha^{-1} \in K$, and $K \neq \mathbb{R}$.
background
In the Primitive Recognition Calculus minimal-field module, the RS constants are collected into a single subfield $K \subset \mathbb{R}$ (written rsField in the development). That field is generated from a finite seed set of named constants and is closed under the field operations, so every further algebraic combination of those seeds remains inside $K$.
The seeds include the golden ratio $\varphi$ (the self-similar fixed point forced at T6), $\pi$, $e$, and the dimensionless inverse fine-structure value $\alpha^{-1}$ built from the canonical exponential resummation $\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (nothing fit to CODATA). Upstream countability facts for certified analytic registries already show that values of finite expression trees over countable labels form a countable set; the same idea blocks continuum smuggling into the constant layer.
The local claim is the Item 1 headline of the PRC package: every named RS constant value lives in one countable subfield strictly below the continuum, so the uncountable real line is not required as the home of the constants.
proof idea
Pure term-mode packing of six already-proved conjuncts. The proof is the tuple
⟨rsField_countable, rsField_mem_phi, rsField_mem_pi, rsField_mem_e, rsField_mem_alphaInv, rsField_proper⟩.
Countability of $K$ comes from the sibling lemma that the subfield closure of a countable (in fact finite) seed set remains countable. The four membership lemmas place $\varphi$, $\pi$, $e$, and $\alpha^{-1}$ in $K$ by construction of the seed set and field closure. Properness ($K \neq \mathbb{R}$) is the remaining sibling, so $K$ is a strict subfield and cannot be the whole continuum.
why it matters
This is the formal Item 1 headline of the PRC minimal-field package: RS physics runs on a countable field, not on continuum content. Downstream it is wired directly into prc_shrunk_certificate as the below_continuum field of the δ-program certificate (“Seven proved headlines, no axioms, no sorry”).
In the broader Recognition framework it underwrites the claim that the φ-power ladder (the scaffold of the RS mass law) and the integer outputs of the forcing chain T0–T8 live inside countable-field content. Constants such as $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and the α band sit in the same countable home; the continuum is not smuggled in as a required codomain for named values.
The module comment after the proof stresses the stronger reading: not only isolated constants, but the entire working machinery (φ-ladder and forcing-chain integers) remains inside the countable field no matter how many further constants the framework names.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.