alpha_coupling_derived
plain-language theorem explainer
The theorem establishes positivity of the fine-structure constant α derived from the D=3 geometric seed 4π·11 with exponential gap correction. Researchers deriving gauge couplings from Recognition Science ledger structure would cite it as the base positivity anchor for electromagnetic interactions. The proof is a one-line term that unfolds alpha, alphaInv, and alpha_seed then applies the positivity tactic.
Claim. The fine-structure constant satisfies $α > 0$, where $α := 1/α_{inv}$ and $α_{inv} := 4π·11 · exp(-f_{gap}/(4π·11))$ with geometric seed $4π·11$ from cube-edge ledger structure.
background
The GaugeCouplingsComplete module derives the three Standard Model gauge couplings from Recognition Science ledger geometry. Electromagnetic α originates in D=3 cube edges via seed 4π·11 (baseline spherical closure over 11-edge paths) corrected by gap factor f_gap. Upstream definitions set alpha_seed := 4 * Real.pi * 11, alphaInv := alpha_seed * Real.exp(-(f_gap / alpha_seed)), and alpha := 1 / alphaInv. The PrimitiveDistinction.from theorem supplies the seven-axiom structural conditions underlying these ledger quantities.
proof idea
The term proof unfolds alpha, alphaInv, and alpha_seed to expose the explicit form 1 / (4 * π * 11 * exp(-f_gap / (4 * π * 11))), then invokes the positivity tactic. The tactic succeeds directly because the seed 4π·11 is positive and the exponential term is always positive.
why it matters
This anchors the electromagnetic coupling inside the C-014 derivation chain for gauge unification. It supports the module claim that α, α_s, and α_w all arise from RS ledger geometry, with α^{-1} ≈ 137.036 matching observation and all three couplings converging near the GUT scale. In the framework it confirms positivity from T8 D=3 spatial dimensions and the geometric seed, feeding the unification hint without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.