alpha_components_derived
The lemma establishes that the inverse fine-structure constant equals a geometric seed times an exponential damping by the gap weight. Physicists deriving electromagnetic constants from Recognition Science ledger structures would cite this to confirm the exact functional form with zero free parameters. The proof is a one-line term wrapper that substitutes the seed and gap definitions then simplifies.
claimThere exist real numbers $s$ and $g$ such that $alpha^{-1} = s * exp(-g/s)$, where $s = 4 pi * 11$ and $g$ is the gap weight from the eight-tick projection.
background
The Constants.Alpha module isolates symbolic expressions for the fine-structure constant. The inverse alphaInv is defined directly as alpha_seed * exp(-(f_gap / alpha_seed)), with the doc-comment stating this is the dimensionless inverse fine-structure constant derived from the structural seed and gap with zero adjustable parameters. The seed alpha_seed equals 4 * pi * 11, representing baseline spherical closure cost over 11-edge interaction paths. The gap f_gap is taken from the GapWeight module as w8_from_eight_tick * log phi, where phi is the golden ratio.
proof idea
The proof is a term-mode construction. It refines the existential witness to the concrete pair (alpha_seed, f_gap) and applies simp to discharge the equality by unfolding the definition of alphaInv.
why it matters in Recognition Science
This declaration secures the exact functional form of the inverse fine-structure constant inside the Recognition framework. It aligns with the eight-tick octave (T7) and the phi-ladder used for constant derivations, placing alpha inverse inside the documented band (137.030, 137.039). The result supports the constants module and the forcing chain steps that fix D = 3, though it lists no downstream uses yet.
scope and limits
- Does not compute or verify any numerical value for alpha.
- Does not prove uniqueness of the seed and gap beyond the supplied definitions.
- Does not invoke J-uniqueness or the Recognition Composition Law.
- Does not address higher-order corrections from the AlphaHigherOrder module.
formal statement (Lean)
50lemma alpha_components_derived :
51 (∃ (seed gap : ℝ),
52 alphaInv = seed * Real.exp (-(gap / seed)) ∧
53 seed = alpha_seed ∧
54 gap = f_gap) := by
proof body
Term-mode proof.
55 refine ⟨alpha_seed, f_gap, ?_⟩
56 simp
57
58end
59
60end Constants
61end IndisputableMonolith