alphaDefault
plain-language theorem explainer
Canonical dimensionless fine-structure default at scale φ, given by (1 − 1/φ)/2. Spec-level seed for the universal dimensionless pack, the explicit UD witness, and φ-closure certificates. Pure algebraic definition with @[simp]; no proof content.
Claim. For a real scale $\varphi$, the canonical (spec-level) dimensionless $\alpha$ default is $\alpha(\varphi)=(1-1/\varphi)/2$.
background
RecogSpec packages dimensionless observables (fine structure, mass ratios, mixing angles, muon $g-2$) as $\varphi$-parameterized data for the Recognition verification layer. The scale $\varphi$ is the free real that, in the forcing chain, is fixed as the golden-ratio self-similar point (T6).
This definition supplies the canonical $\alpha$ entry used by the explicit dimensionless pack and the universal dimless witness. The companion lemma phiClosed_alphaDefault shows the expression is algebraic in $\varphi$ (PhiClosed), which is exactly the kind of closure HonestClosureCert Part A demands.
The formula is elementary half of one minus the reciprocal. It is not the inverted lock value near 137; it is the raw dimensionless seed the pack carries.
proof idea
Definitional, not a theorem. The body is the closed form $(1-1/\varphi)/2$, tagged @[simp] so downstream tactics unfold it automatically. No lemmas are applied; the only work is the arithmetic expression itself.
why it matters
Feeds dimlessPack_explicit and UD_explicit as the alpha / alpha0 field of the dimensionless pack. The lemma phiClosed_alphaDefault certifies $\varphi$-closure of this seed, which HonestClosureCert uses when stating that observables are algebraic in $\varphi$.
Also appears in the exclusivity framework structure DerivesObservables, on the electromagnetic fine-structure prediction path (the deprecated band check near $137.035$–$137.037$). In the broader RS picture this is the pack-level handle on $\alpha$, sitting upstream of the observational $\alpha^{-1}$ band $(137.030,137.039)$ from the primer; the def itself does not close that band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.