phiClosed_alphaDefault
plain-language theorem explainer
The default alpha seed built from a real parameter φ is φ-closed: it lies in the field operations generated from φ. Anyone assembling the explicit universal dimensionless pack or the honest-closure certificate cites this. The proof unfolds the seed to (1 − 1/φ)/2 and closes under unit, reciprocal, subtraction, and division by two.
Claim. For every real $\varphi$, the default alpha seed $\alpha_0(\varphi)=(1-1/\varphi)/2$ is $\varphi$-closed (obtainable from $\varphi$ by field operations starting from $1$).
background
In RecogSpec, dimensionless observables are required to be φ-closed: built from the golden-ratio parameter by the ring/field operations that PhiClosed tracks (constants from ℕ, reciprocal, subtraction, division). The default alpha seed is the explicit algebraic expression α₀(φ) = (1 − 1/φ)/2 used as the alpha slot of the universal dimensionless pack.
PhiClosed is the inductive predicate that witnesses this algebraic dependence. Upstream helpers supply the generators: PhiClosed.one, phiClosed_one_div (closure under reciprocal of φ), PhiClosed.sub, PhiClosed.of_nat, and PhiClosed.div. The same φ-closed discipline appears in the honest-closure certificate, which demands that every reported observable be algebraic in φ rather than an external fit.
proof idea
Term-mode after a single unfold. simp only [alphaDefault] rewrites the goal to PhiClosed φ ((1 − 1/φ)/2). Build the pieces: PhiClosed.one gives 1; phiClosed_one_div gives 1/φ; PhiClosed.sub closes the difference 1 − 1/φ; PhiClosed.of_nat supplies 2; PhiClosed.div finishes the quotient. No arithmetic identities beyond the definition are needed.
why it matters
Feeds UD_explicit, which packs alphaDefault φ into the alpha0 field of UniversalDimless φ, and HonestClosureCert, whose Part A requires every observable to be φ-closed. Without this lemma the explicit dimensionless pack cannot claim algebraic honesty for its alpha slot. In the broader RS chain this is bookkeeping for the φ-ladder and the alpha band, not a derivation of α⁻¹ ∈ (137.030, 137.039); it only certifies that the default seed is an algebraic expression in φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.