phiClosed_one_div
plain-language theorem explainer
For any real φ, the reciprocal 1/φ lies in the subfield generated by φ. Spec and certification authors cite this when building φ-closed expressions for dimensionless RS defaults (α, g−2, mass ratios). The proof is a three-line field-closure argument: 1 and φ are φ-closed, and PhiClosed is closed under division.
Claim. For every real number $\varphi$, the reciprocal $1/\varphi$ belongs to the subfield of $\mathbb{R}$ generated by $\varphi$ (i.e., $1/\varphi$ is obtainable from $\varphi$ by field operations).
background
In RecogSpec, a real $x$ is called $\varphi$-closed when $x\in\mathrm{phiSubfield}(\varphi)$, the subfield of $\mathbb{R}$ generated by a fixed real $\varphi$. That predicate packages the algebraic content of RS dimensionless quantities: they must be built from $\varphi$ by $+$, $-$, $\cdot$, and $/$ only.
Upstream, PhiClosed.self records that $\varphi$ itself is in the generated subfield, and the companion one-witness gives $1$. Closure under division is the subfield lemma PhiClosed.div: if $x$ and $y$ are $\varphi$-closed then so is $x/y$. Those three facts are the only inputs here.
The local module assembles the explicit universal dimensionless pack (fine-structure default, mass ratios, mixing angles, muon $g-2$ toy value) and the honest-closure certificate that every listed observable is $\varphi$-closed.
proof idea
Term-mode proof with two intermediate witnesses. First apply the unit witness to get $\mathrm{PhiClosed},\varphi,1$. Second apply the generator witness to get $\mathrm{PhiClosed},\varphi,\varphi$. Feed both into the division-closure lemma to conclude $\mathrm{PhiClosed},\varphi,(1/\varphi)$. No arithmetic identities beyond field structure are used.
why it matters
This is the first nontrivial reciprocal witness in the $\varphi$-closure chain. Downstream, phiClosed_alphaDefault builds the default fine-structure expression $(1-1/\varphi)/2$ by subtracting this reciprocal from 1 and dividing by 2; without $1/\varphi$ that step fails. The same reciprocal appears inside the explicit universal dimensionless pack UD_explicit (via alphaDefault and related defaults) and is consumed by HonestClosureCert, whose Part A requires every listed observable to be algebraic in $\varphi$.
In the broader RS picture, $\varphi$ is the self-similar fixed point forced at T6, and dimensionless constants live on the $\varphi$-ladder. Certifying that $1/\varphi$ is $\varphi$-closed is the elementary gate that lets later band and Born-rule witnesses stay inside the generated subfield rather than adjoining new transcendentals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.