alpha
plain-language theorem explainer
The declaration defines the fine-structure constant α_EM as the reciprocal of its inverse value obtained from the structural seed via exponential resummation with the gap. Physicists assembling dimensionless couplings in Recognition Science derivations cite this when referencing the electromagnetic interaction strength. The definition is a direct one-line reciprocal applied to the upstream inverse computation.
Claim. The fine-structure constant is defined by $α := 1/α^{-1}$, where the inverse $α^{-1}$ is the product of the structural seed and the exponential of the negative ratio of the gap function to the seed.
background
In the Constants.Alpha module the fine-structure constant appears together with its inverse. The inverse is obtained as the structural seed multiplied by the exponential of minus the gap divided by the seed, producing a value near 137.036. Upstream the Constants structure from LawOfExistence bundles related parameters such as Knet and Cproj with a non-negativity condition, while the Provenance inductive type from EarthBrainResonance separates forced derivations from empirical predictions. This placement continues the derivation of constants from the Recognition Science forcing chain.
proof idea
The definition is a one-line wrapper that applies the reciprocal operation to the alphaInv definition in the same module.
why it matters
This definition supplies the fine-structure constant for downstream results including phi_cubed_in_theta_band in photobiomodulation devices and the zero-parameter status hypothesis in astrophysics mass-to-light ratios. It also supports lattice parameter constraints in crystal symmetry. Within the framework it realizes the inverse fine-structure constant inside the interval (137.030, 137.039) as part of the constants derived from the phi-ladder and T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.