Constants Alpha Genesis Kappa Gamma Irreducibility

A scoped no-go result

The fine-structure constant α is a dimensionless number, roughly 1/137.036, that sets the strength of electromagnetic interactions between charged particles. In Recognition Science, the framework's library of formal theorems contains a module called Alpha Genesis that studies a one-parameter family of candidate values for the inverse coupling, α⁻¹. The family is defined as alphaInvK κ = κ · Constants.alphaInv, where κ is a positive real number and Constants.alphaInv is a fixed positive constant. This family is strictly increasing and injective, so each distinct κ gives a distinct candidate value, and together the family sweeps through every positive real number.

The central result is a scoped non-identifiability theorem. It defines a predicate called ForcedClosure that packages three arithmetic facts about a cube's cycle rank, edge count, and gauge redundancy, facts that hold for every κ by construction. The theorem alpha_not_pinned_by_forcedClosure proves that this predicate cannot pin down a single value of α⁻¹: for any target value t, there exist two different positive κ values, such as 1 and 2, both satisfying ForcedClosure but yielding different α⁻¹ values. The proof is a direct contradiction using injectivity. A more general theorem, kappa_blind_closure_cannot_pin, extends this: no satisfiable predicate that is independent of κ can pin the injective family alphaInvK.

In plain language, the result establishes that the three closure conditions, while true, carry no information about which normalization κ is physical. The conditions are κ-blind, so they cannot distinguish one candidate value from another. This is a theorem about the defined family, not a statement about the physical fine-structure constant. The result explicitly notes that it has no matter-charge variable, so it cannot state the field-rescaling invariant q²/κ, and the exact gauge-plus-matter classification is left to another file, CouplingNormalizationOrbit.lean.

The result also proves that the family meets a broad interval around the assembled construction value at κ = 1, with 137.030 < α⁻¹ < 137.039. This is a purely numerical fact with no evidential force, as the assembled value is empirically excluded. The status tags are precise: the κ-independence and positive-range statements are THEOREM, while the physical value of α and any global primitivity claim remain OPEN. The axiom audit for the module is clean, resting only on the standard three axioms, with no RS-specific axioms and no compiler trust.

/-- The κ_γ-scaling is strictly monotone: distinct normalizations give distinct
`α⁻¹`. -/
theorem alphaInvK_strictMono : StrictMono alphaInvK := by
  intro a b hab
  exact mul_lt_mul_of_pos_right hab alphaInv_pos

/-- … hence injective in `κ_γ`. -/
theorem alphaInvK_injective : Function.Injective alphaInvK :=
  alphaInvK_strictMono.injective

/-- The forced-closure facts hold for **every** normalization `κ_γ`. -/
theorem forcedClosure_holds (κ : ℝ) : ForcedClosure κ :=
  ⟨cube_cycle_rank_eq_5, physical_link_dof_eq_cycle_rank, seed_channel_count_ne_gauge_dof⟩

/-- No satisfiable κ-independent predicate pins the injective observable
`alphaInvK`. A predicate may still identify the physical orbit invariant
`q²/κ`; that variable is outside this module. -/
theorem kappa_blind_closure_cannot_pin
    {P : ℝ → Prop} (hconst : ∀ κ κ', P κ ↔ P κ') (hsat : ∃ κ, P κ) :
    ¬ Pins P alphaInvK := by
  rintro ⟨t, ht⟩
  obtain ⟨κ0, hκ0⟩ := hsat
  have hP1 : P 1 := (hconst κ0 1).mp hκ0
  have hP2 : P 2 := (hconst κ0 2).mp hκ0
  have e1 : alphaInvK 1 = t := ht 1 (by norm_num) hP1
  have e2 : alphaInvK 2 = t := ht 2 (by norm_num) hP2
  have : (1 : ℝ) = 2 := alphaInvK_injective (by rw [e1, e2])
  norm_num at this

/-- Three closed arithmetic facts packaged as a κ-parametrized predicate.
The parameter is ignored by definition. Graph and gauge interpretations of
the facts remain DERIVED-UNFORMALIZED or MODEL as documented in
`U1Normalization.lean`. -/
def ForcedClosure (_κ : ℝ) : Prop :=
  cube_cycle_rank = 5 ∧
  (cube_edges D - gauge_redundancy = cube_cycle_rank) ∧
  (passive_field_edges D ≠ cube_cycle_rank)

What this page does not claim

This module does not prove that the physical fine-structure constant is primitive or irreducible. The closure conditions carry no evidential weight for the physical value of α. The face-Gaussian identification with a photon cycle-space measure is a MODEL, not a theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/AlphaGenesis/KappaGammaIrreducibility.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: