-- 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. -- -- Companion to: -- • 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⟩ end QLF