Constants Alpha Genesis Kappa Gamma Irreducibility Forced Closure Plus Blind Con

What the closure facts cannot do

The inverse fine-structure constant, written 1/α, is a number near 137.036 that measures the strength of electromagnetic interaction. The Recognition Science framework builds a family of candidate values for this number by scaling a base construction value: the family is α⁻¹(κ) = κ · α_base, where κ is a positive real scaling parameter. The framework's library, a machine-checked collection of formal theorems, proves that this family is injective: different κ values give different candidate values, and together they sweep out every positive real number.

The framework also defines a predicate called ForcedClosure, a set of three arithmetic facts about a cube's edges and cycles that hold for every κ by construction. The central theorem, forcedClosure_plus_blind_conjunct_cannot_pin, states a precise limitation: no satisfiable condition that is independent of κ, even when added as an extra requirement on top of ForcedClosure, can force the family to take a single value. The proof compares κ = 1 and κ = 2: both satisfy any κ-independent condition, so both would have to equal the same pinned value, contradicting injectivity.

This is a scoped result about the defined family, not a statement about the physical constant. The theorem does not prove that 1/α is primitive or irreducible in nature. It does not show that the base construction value is the true physical coupling, and it cannot address the field-rescaling invariant q²/κ because the module has no matter-charge variable. The exact gauge-plus-matter classification lives in a separate file. The theorem's status is THEOREM for the κ-independence and positive-range statements; the physical value of α remains OPEN.

/-- Adding any satisfiable κ-independent conjunct preserves the scoped
non-pinning result for `alphaInvK`. -/
theorem forcedClosure_plus_blind_conjunct_cannot_pin
    {Q : ℝ → Prop} (hQconst : ∀ κ κ', Q κ ↔ Q κ') (hQsat : ∃ κ, Q κ) :
    ¬ Pins (fun κ => ForcedClosure κ ∧ Q κ) alphaInvK := by
  apply kappa_blind_closure_cannot_pin
  · intro κ κ'
    exact ⟨fun h => ⟨forcedClosure_holds κ', (hQconst κ κ').mp h.2⟩,
           fun h => ⟨forcedClosure_holds κ, (hQconst κ' κ).mp h.2⟩⟩
  · obtain ⟨κ, hκ⟩ := hQsat
    exact ⟨κ, forcedClosure_holds κ, hκ⟩

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

/-- The defined closure holds for every positive κ, while `alphaInvK` sweeps
every positive value. This is a theorem about the defined family, not global
irreducibility of the physical fine-structure constant. -/
theorem alphaInv_irreducible_under_closure :
    ∀ t : ℝ, 0 < t → ∃ κ : ℝ, 0 < κ ∧ ForcedClosure κ ∧ alphaInvK κ = t := by
  intro t ht
  have hne : Constants.alphaInv ≠ 0 := ne_of_gt alphaInv_pos
  refine ⟨t / Constants.alphaInv, div_pos ht alphaInv_pos, forcedClosure_holds _, ?_⟩
  unfold alphaInvK
  field_simp

What this page does not claim

The theorem does not prove that the physical fine-structure constant is primitive or irreducible. The theorem does not establish that the base construction value is the true physical inverse coupling. The theorem does not claim that every future physical law is independent of the scaling parameter κ.

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: