-- 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
