Constants Alpha Genesis Kappa Gamma Irreducibility Forced Closure Kappa Independ

A scoped non-identifiability result

The declaration forcedClosure_kappa_independent is a machine-checked theorem in the framework's library of formal theorems. It states that a specific predicate, called ForcedClosure, holds for every positive real number κ (kappa), and that its truth does not depend on κ at all. The predicate packages three closed arithmetic facts about a cube's cycle rank, edge count, and gauge redundancy; the parameter κ is ignored by definition. The theorem's content is that this particular closure condition is κ-blind: it cannot distinguish one normalization from another.

The theorem's force is negative. The framework also defines a family alphaInvK κ = κ * Constants.alphaInv, which is strictly monotone and injective in κ, so it sweeps every positive value. The theorem alpha_not_pinned_by_forcedClosure proves that no single target value t is forced for every positive κ satisfying ForcedClosure. The proof compares κ = 1 and κ = 2: both satisfy the closure, so a pinning predicate would force alphaInvK 1 = alphaInvK 2, contradicting injectivity. A stronger theorem, kappa_blind_closure_cannot_pin, generalizes this: no satisfiable κ-independent predicate can pin the injective family alphaInvK. This is a scoped normalization-coordinate result, not a statement about the physical coupling's primitivity.

In plain language, the declaration establishes that the closure facts alone do not determine the value of the inverse fine-structure constant. The framework's own documentation is explicit: the module has no matter-charge variable, so it cannot state the field-rescaling invariant q²/κ. The exact gauge-plus-matter classification lives in a separate file, CouplingNormalizationOrbit.lean. The theorem is a correct scoped result about a defined family; it does not prove that the physical coupling is primitive, nor that every future physical law is κ-independent.

What the theorem does not claim is as important as what it proves. It does not claim that the physical value of α is derived or forced. It does not claim that the closure condition is the correct physical law. It does not claim that the family alphaInvK is the physical inverse coupling. The theorem's status is THEOREM for the κ-independence and positive-range statements inside the definitions; the physical value of α and any global primitivity claim remain OPEN. The declaration is a boundary marker, not a destination.

/-- The defined closure is κ-independent because its argument does not occur in
the body. -/
theorem forcedClosure_kappa_independent (κ κ' : ℝ) :
    ForcedClosure κ ↔ ForcedClosure κ' := Iff.rfl

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

/-- The defined `ForcedClosure` does not pin `alphaInvK`. The proof compares
κ values 1 and 2. No physical coupling conclusion follows without the missing
matter-charge relation. -/
theorem alpha_not_pinned_by_forcedClosure : ¬ Pins ForcedClosure alphaInvK := by
  rintro ⟨t, ht⟩
  -- The closure holds at κ = 1 and κ = 2, so both values must equal t, forcing
  -- alphaInvK 1 = alphaInvK 2, contradicting injectivity (1 ≠ 2).
  have h1 : alphaInvK 1 = t := ht 1 (by norm_num) (forcedClosure_holds 1)
  have h2 : alphaInvK 2 = t := ht 2 (by norm_num) (forcedClosure_holds 2)
  have : alphaInvK 1 = alphaInvK 2 := by rw [h1, h2]
  have : (1 : ℝ) = 2 := alphaInvK_injective this
  norm_num at this

What this page does not claim

Not claimed: the physical value of α is derived or forced. Not claimed: the closure condition is the correct physical law. Not claimed: the family alphaInvK is the physical inverse coupling.

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: