-- QLF_FineStructureSubstrate.lean -- The fine-structure constant α derived from QLF substrate combinatorics, -- with zero free parameters. -- -- The full derivation chain (Magnetism_Spatial_Dynamics.md §6.1): -- -- 1. Naive closure rate: 1/16 -- (per substrate event, 1/16 chance of forming any of the 4 base -- half-spin closures {^v, <>, /\, +-} from the 8-twist alphabet, -- via prob 1/8 per twist-pair partner) -- -- 2. Gauge selectivity: 1/4 -- (only `+-` of the 4 base closures is the gauge fold that mediates -- Coulomb binding; spatial closures {^v, <>, /\} mediate orbital -- structure but not the gauge-twist exchange that defines α) -- -- 3. Phase coherence: 1/2 -- (binary in-phase / out-of-phase selectivity; for a closure to -- advance the bound state's orbital phase rather than randomise -- it, the closure's relative phase must align with the orbital -- cycle) -- -- 4. Spatial co-location: 1 -- (the binding-photon wavelength λ_binding = ℏc/Ry ≈ 91 nm gives -- λ/2 ≈ 45 nm >> the Bohr radius a₀ ≈ 0.053 nm; the electron is -- always within λ/2 of the proton at the binding energy) -- -- 5. Bare combinatorial α: α_bare = 1/16 × 1/4 × 1/2 × 1 = 1/128 = 2⁻⁷ -- -- 6. Emergent E-conservation: α_QLF = α_bare / (1 + N · α_bare) -- (energy conservation is emergent from substrate dynamics, not -- axiom; the leading-order correction is a self-energy / -- vacuum-polarization-like resummation) -- -- 7. N = 9 from the 3² spatial directional-coupling tensor: -- - Substrate is 3-dimensional in the spatial sector (6 spatial -- twists organised into 3 axis-pairs: Y = ^v, X = <>, Z = /\; -- the 3D itself derived in Magic_numbers.md from the 8-twist -- alphabet's 6+2 split and the (k+1)(k+2) 3D-SHO inequality k > 2) -- - Bound-state binding interaction has directional structure -- (per substrate event, gauge-twist exchange has an input -- direction × output direction) -- - Directional-coupling tensor T_{ij} has 3 × 3 = 9 independent -- components (substrate isotropy: no symmetry reduces the count) -- - Each tensor component contributes one self-energy term α_bare -- → N = 9 -- -- 8. Final value: α_QLF = 1/128 / (1 + 9/128) = 1/137 (exact rational) -- vs CODATA α = 1/137.036 (0.026% relative error) -- -- The residual 0.026% sits at the Schwinger anomalous-moment scale -- α/(2π) ≈ 1.16 × 10⁻³ and is consistent with higher-order substrate -- corrections (multi-twist closures beyond length-2, two-loop substrate -- diagrams). -- -- This module packages the structural-counting facts. The arithmetic -- is finite rational arithmetic; the structural content lives in the -- named-quantity decomposition with each factor tied to a substrate -- first-principles claim. No real-valued integrals, no non-constructive -- reasoning. -- -- SCALE AND COSMOLOGICAL INVARIANCE (see Alpha.md): -- • The derived value is the q²→0 (Thomson / IR) coupling of *fully- -- rendered 3-D space* — the (1 + 9·α_bare) factor is the self-energy / -- screening resummation, taking the bare 2⁻⁷ = 1/128 to the screened -- (low-energy) 1/137. N = 9 = 3² exists only once space renders to its -- minimal faithful dimension 3 (SpaceTime.md §3a: α = N = 3² is a -- *consequence* of 3-D rendering). -- • The whole chain collapses to the closed form α(d) = 1/(128 + d²) -- (alpha_at_dim_closed_form): α is a function of the rendering dimension -- `d` ALONE — there is no time parameter. So α(0) = α(d=3) = 1/137 has -- no cosmological-time dependence: it can change only if `d` changes, -- and d = 3 is fixed by the minimal-faithful-rendering necessity, not by -- epoch. This is the "no cosmological drift of α(0)" statement -- (no_cosmological_drift_of_alpha) — falsifiable, and *sharper* than the -- Standard Model, which treats α(0) as a free input that varying-α models -- can promote to a slowly-drifting field; QLF forbids that. -- • The SM *running* of the *effective* α(μ) (larger in the UV / early -- universe) is a separate thing — energy not time — read in QLF as the -- effective-dimension flow 3→2 toward the UV (α: 1/137→1/132, via -- alpha_QLF_2d_counterfactual), with the magnitude the open β-coefficient -- sector (QLF_RunningCouplings, running_couplings_structural). -- -- Companion to: -- • Alpha.md — the canonical α doc -- • Magnetism_Spatial_Dynamics.md §6.1, §6.1.1, §6.1.2, §6.1.3, §6.1.4 -- • magnetism_spatial_dynamics_demo.py — runnable demo -- • Hydrogen.md §§2-4 — QLF Bohr derivation -- • Magic_numbers.md — 3-dimensionality from 6+2 split -- • Experimental_Consistency.md §6.3 + §10 Class-B falsifier -- • Proton_Resonance_R_e.md — parallel Tier-3 pathway -- • fine_structure_demo.py — observable-input pathway import Mathlib.Analysis.SpecialFunctions.Pow.Real namespace QLF /-- **Naive closure rate per substrate event.** Per pair of substrate events, the probability of forming any of the four base half-spin closures `{^v, <>, /\, +-}` is `1/8` — the second twist must partner the first (1 of 8 choices). Per individual substrate event: `1/16`. This is the unconstrained substrate combinatorial baseline from the 8-twist alphabet structure; no observable input, no fit parameter. -/ noncomputable def naive_closure_rate : ℝ := 1 / 16 /-- **Gauge selectivity.** Of the 4 base half-spin closures `{^v, <>, /\, +-}`, only `+-` is the *gauge* closure (the U(1) phase fold that mediates Coulomb binding per `Hydrogen.md` §2 Coulomb-via-gauge-twist-exchange). The other three (`^v`, `<>`, `/\`) are *spatial* axis closures (Pauli σ_y, σ_x, σ_z respectively). For a Coulomb-mediated bound state, only gauge closures advance the binding interaction. Selectivity: 1 of 4 base closures → `1/4`. -/ noncomputable def gauge_selectivity : ℝ := 1 / 4 /-- **Phase coherence selectivity.** For a substrate-level closure to advance the bound state's orbital phase rather than randomise it, the closure's relative phase must align with the orbital cycle. This is a binary in-phase / out-of-phase selectivity: `1/2`. -/ noncomputable def phase_coherence : ℝ := 1 / 2 /-- **Spatial co-location at the binding scale.** For the bound state, spatial co-location is guaranteed at the relevant scale: the binding-photon wavelength `λ_binding = ℏc / Ry ≈ 91 nm` gives `λ_binding / 2 ≈ 45 nm`, vastly larger than the Bohr radius `a₀ ≈ 0.053 nm`. The electron is always within `λ_binding / 2` of the proton at the binding energy. No selectivity penalty. Selectivity factor: `1`. -/ noncomputable def spatial_colocation : ℝ := 1 /-- **Bare combinatorial α** — the product of the four substrate selectivities, evaluating to `1/128 = 2⁻⁷`. No observable input. Each factor traces to a specific QLF substrate principle: | Factor | Value | Source | |---|---|---| | Naive closure rate | 1/16 | 8-twist alphabet, 4 base closures | | Gauge selectivity | 1/4 | `+-` is 1 of 4 base atoms (the gauge axis) | | Phase coherence | 1/2 | binary in / out of phase | | Spatial co-location | 1 | λ_binding/2 ≈ 45 nm >> a₀ ≈ 0.053 nm | The substrate combinatorial value `1/α_bare = 128 = 2⁷` is a clean substrate-arithmetic number. -/ noncomputable def alpha_bare : ℝ := naive_closure_rate * gauge_selectivity * phase_coherence * spatial_colocation /-- **Spatial substrate dimension** — the number of spatial axes in the substrate. The 8-twist alphabet partitions as 6 spatial + 2 gauge twists. The 6 spatial twists organise into 3 axis-pairs: Y axis: `^` (σ_y), `v` (−σ_y) X axis: `<` (−σ_x), `>` (+σ_x) Z axis: `/` (+σ_z), `\` (−σ_z) Hence the substrate has exactly 3 spatial dimensions. This is derived in `Magic_numbers.md` from the `(k+1)(k+2)` 3D-SHO inequality `k > 2`, where `3` comes from the `d = 3` of `(k+1)(k+2)`, exactly the 3 spatial dimensions encoded by the alphabet's 6 spatial twists. Substrate first-principles fact, not an empirical input. -/ def substrate_spatial_dimension : ℕ := 3 /-- **Number of independent directional-coupling tensor components**: `N = (substrate_spatial_dimension)² = 9`. The bound-state binding interaction per substrate event has directional structure: an *input direction* (where the gauge twist comes from) × an *output direction* (where it goes to). The set of all (input, output) pairs forms a `d × d` directional-coupling tensor `T_{ij}` where `d = substrate_spatial_dimension`. For an isotropic substrate (no preferred direction in the vacuum, which holds at the 6+2 alphabet level where all 3 spatial axes are treated equivalently), every component is independent — no symmetry reduces the count. Therefore `N = d² = 3² = 9`. This is the *structural derivation* of N = 9, replacing what would otherwise be a fit parameter. The counterfactual: a 2D substrate would give N = 4 (off CODATA α by ≈ 4%); a 4D substrate would give N = 16 (off by ≈ 5%). Only 3D (N = 9) lands at 0.026%. -/ def N_directional_modes : ℕ := substrate_spatial_dimension ^ 2 /-- **Emergent energy-conservation correction**: `α_QLF = α_bare / (1 + N·α_bare)`. Energy conservation is not a QLF axiom — it is emergent from substrate dynamics. At the substrate event level, individual closures need not conserve energy; statistical averaging over many events produces effective conservation at the bound-state scale. The standard leading-order form for such an emergent-conservation correction is a self-energy / vacuum-polarization-like resummation: $$ \alpha_{\text{QLF}} \;=\; \frac{\alpha_{\text{bare}}}{1 + N \alpha_{\text{bare}}} $$ where `N` counts the substrate "vertex modes" through which the bound state's energy can leak into the substrate (and which the emergent conservation suppresses). Each independent leak channel contributes one factor `α_bare` per substrate event; the geometric series resums to the closed-form above. For QLF, `N = N_directional_modes = 9` from the structural derivation above. Plugging α_bare = 1/128: `α_QLF = (1/128) / (1 + 9/128) = (1/128) × (128/137) = 1/137`. -/ noncomputable def alpha_QLF : ℝ := alpha_bare / (1 + (N_directional_modes : ℝ) * alpha_bare) /-- **Bare combinatorial product evaluates to `1/128`.** Direct arithmetic on the four substrate selectivities. -/ theorem alpha_bare_eq : alpha_bare = 1 / 128 := by unfold alpha_bare naive_closure_rate gauge_selectivity phase_coherence spatial_colocation norm_num /-- **N = 9** as the 3² spatial directional-coupling tensor count. -/ theorem N_directional_modes_eq_nine : N_directional_modes = 9 := by unfold N_directional_modes substrate_spatial_dimension norm_num /-- **Substrate-derived α equals `1/137` exactly** — main theorem. The combinatorial product `1/128` corrected by the emergent energy-conservation factor `(1 + 9 · 1/128)⁻¹` gives exactly `1/137`, matching CODATA α = `1/137.036` at 0.026% relative error. Zero free parameters: every factor in the chain is derived from a QLF substrate first-principles claim. Proof: rewriting `alpha_bare` and `N_directional_modes` to their numeric values reduces the goal to finite rational arithmetic, discharged by `norm_num`. -/ theorem alpha_QLF_eq : alpha_QLF = 1 / 137 := by unfold alpha_QLF rw [alpha_bare_eq, N_directional_modes_eq_nine] push_cast norm_num /-- **Counterfactual: 2D substrate would give `α = 1/132`** (= 3.82% off CODATA). If the substrate had 2 spatial dimensions instead of 3, the directional tensor would have 2² = 4 components, giving N = 4 and α_corrected = (1/128) / (1 + 4/128) = 1/132. -/ theorem alpha_QLF_2d_counterfactual : alpha_bare / (1 + (4 : ℝ) * alpha_bare) = 1 / 132 := by rw [alpha_bare_eq] norm_num /-- **Counterfactual: 4D substrate would give `α = 1/144`** (= 4.84% off CODATA). If the substrate had 4 spatial dimensions, the directional tensor would have 4² = 16 components, giving N = 16 and α_corrected = (1/128) / (1 + 16/128) = 1/144. -/ theorem alpha_QLF_4d_counterfactual : alpha_bare / (1 + (16 : ℝ) * alpha_bare) = 1 / 144 := by rw [alpha_bare_eq] norm_num /-- **Counterfactual summary**: only the 3D substrate (N = 9) gives `α = 1/137`. The fine-structure constant's empirical value reflects the empirical 3-dimensionality of space — both emerging from the 8-twist alphabet's 6+2 split. -/ theorem only_3d_substrate_gives_137 : alpha_QLF = 1 / 137 ∧ alpha_bare / (1 + (4 : ℝ) * alpha_bare) = 1 / 132 ∧ alpha_bare / (1 + (16 : ℝ) * alpha_bare) = 1 / 144 := by exact ⟨alpha_QLF_eq, alpha_QLF_2d_counterfactual, alpha_QLF_4d_counterfactual⟩ /-- **α as a function of the rendering dimension alone.** `α(d) = α_bare / (1 + d²·α_bare)` — the bare `2⁻⁷` screened by the `d²` directional-coupling tensor. The only variable is the rendering dimension `d`; there is **no time parameter**. This is what makes the no-cosmological-drift statement precise (see below). -/ noncomputable def alpha_at_dim (d : ℕ) : ℝ := alpha_bare / (1 + (d : ℝ) ^ 2 * alpha_bare) /-- **Closed form**: `α(d) = 1/(128 + d²)`. The entire combinatorial chain reduces to this single rational function of the rendering dimension. -/ theorem alpha_at_dim_closed_form (d : ℕ) : alpha_at_dim d = 1 / (128 + (d : ℝ) ^ 2) := by unfold alpha_at_dim rw [alpha_bare_eq] have h1 : (1 : ℝ) + (d : ℝ) ^ 2 * (1 / 128) ≠ 0 := by positivity have h2 : (128 : ℝ) + (d : ℝ) ^ 2 ≠ 0 := by positivity field_simp /-- At the physical rendering dimension `d = 3`, `α(3) = 1/137`. -/ theorem alpha_at_dim_three : alpha_at_dim 3 = 1 / 137 := by rw [alpha_at_dim_closed_form]; norm_num /-- At `d = 5`, `α(5) = 1/153` (= `1/(128+25)`). Completes the `d = 2,3,4,5` counterfactual series. But the higher-`d` values do not describe viable physics: by QLF's own derived force law `F ∝ 1/r^(d−1)` (Gravity_From_Delay), the Coulomb potential is `V ∝ 1/r^(d−2)`, so at `d ≥ 4` the bound state is critically unstable (`d=4`) or collapses (`d≥5`) — **no stable atoms** (Ehrenfest 1917 / Tangherlini). Only `d = 3` (`α = 1/137`) supports atoms, the nuclear `ℓ = 3` magic-number threshold, and the 3-axis gauge unification. See Alpha.md §4a. -/ theorem alpha_at_dim_five : alpha_at_dim 5 = 1 / 153 := by rw [alpha_at_dim_closed_form]; norm_num /-- `α(d)` at the substrate's spatial dimension **is** `alpha_QLF`. -/ theorem alpha_at_dim_eq_alpha_QLF : alpha_at_dim substrate_spatial_dimension = alpha_QLF := by rw [alpha_QLF_eq, show substrate_spatial_dimension = 3 from rfl, alpha_at_dim_three] /-- **No cosmological-time drift of α(0).** `alpha_at_dim` is a function of the rendering dimension `d` only — it has no time argument (`alpha_at_dim_closed_form`: `α = 1/(128 + d²)`). Hence `α(0) = alpha_at_dim 3 = 1/137` (`alpha_at_dim_three`, `alpha_at_dim_eq_alpha_QLF`) is an **atemporal structural fact**: there is no dynamical variable for it to drift along. α(0) can change only if the macroscopic rendering dimension `d` changes — and `d = 3` is fixed by the minimal-faithful-rendering *necessity* (SpaceTime.md §3a, QLF_ReachableEvent), not by epoch. So "no drift" is a **conditional theorem** (given the atemporal 8-twist alphabet and epoch-independent 3-D rendering, both QLF structural necessities), and a **falsifiable prediction sharper than the SM**: where the Standard Model treats α(0) as a free input that varying-α models can promote to a drifting field, QLF *forbids* it — a confirmed cosmological drift of α(0) would falsify the substrate. The honest boundary (the `True` marker, the QLF idiom for a named non-arithmetic claim): that the two premises hold of the *physical* universe is empirical content provable within QLF's frame, not ZFC-absolutely. See Alpha.md §5. -/ theorem no_cosmological_drift_of_alpha : True := trivial end QLF