Constants Alpha Genesis U1 Normalization

The U(1) normalization verdict

The fine-structure constant α is a number that measures the strength of the electromagnetic force. In the Recognition Science framework, a candidate seed for its inverse, 1/α = 4π¹¹, has been under scrutiny. The question was whether this seed could be promoted from a numerical identification to a theorem about how a U(1) gauge symmetry, the kind that describes electromagnetism, gets its coupling strength from the geometry of a three-dimensional cube. A gauge symmetry is a redundancy in description that leaves physics unchanged.

The test module, called U1Normalization, performs this check with machine-checked arithmetic. It first computes a candidate count of gauge degrees of freedom from the cube: 12 edges minus 8 vertices plus 1 equals 5. This count, the cycle rank of the cube graph, is what a finite link model would use for independent loop coordinates. The module also verifies an alternative route to the same number: 12 edges minus 7 redundancies equals 5. Both routes agree in the formal proof.

The central result is a proved mismatch. The seed's channel count, 11, comes from a ledger count of passive edges in the framework's recognition model. This is not the same as the candidate gauge count of 5. The machine-checked theorem seed_channel_count_ne_gauge_dof proves 11 ≠ 5. Neither number is thereby shown to be a photon kinetic coefficient. The module also defines a candidate stiffness of 20π by substituting the graph count into the seed formula, but proves only that this candidate is less than the assembled alphaInv value. It does not derive a Maxwell action or compare with experiment.

The honest formal object is a conditional reading, SeedNormalizationReading, which holds only under three explicit assumptions: the Heaviside-Lorentz convention α = e²/(4π), a bare charge quantum e² = 1, and the load-bearing identification that photon stiffness equals the ledger count 11, not the gauge count 5. This reading is inhabited, meaning it is a valid identification, but it is not a derivation. The framework models a finite parity quotient of the cube's automorphism group, not the continuous group U(1), and no gauge theory or Maxwell action is derived from the cube.

What this establishes in plain language is a sharp negative result. The number 11 is a ledger count, the number 5 is a candidate graph count, and neither determines the physical ratio e²/κ. The attempt to promote the α seed to a coupling-normalization theorem fails cleanly, and the framework records that failure as a proved arithmetic mismatch rather than a speculative gap.

/-- **Arithmetic verdict.** The seed channel count `11` is not the candidate
cycle-rank count `5`. This theorem does not identify either number with a
kinetic coefficient. -/
theorem seed_channel_count_ne_gauge_dof :
    passive_field_edges D ≠ cube_cycle_rank := by
  rw [seed_channel_count, cube_cycle_rank_eq_5]; norm_num

theorem cube_cycle_rank_eq_5 : cube_cycle_rank = 5 := by
  unfold cube_cycle_rank cube_edges cube_vertices D; decide

/-- The defined candidate `20π` is less than the corpus's assembled
`Constants.alphaInv`. This is not a direct measurement verdict, and it does
not establish a genuine gauge normalization. -/
theorem gauge_invariant_seed_excluded :
    gauge_invariant_seed < Constants.alphaInv := by
  rw [gauge_invariant_seed_eq_20pi]
  have hpi : Real.pi < (3.141593 : ℝ) := Real.pi_lt_d6
  have h1 : (20 : ℝ) * Real.pi < 63 := by nlinarith [hpi]
  have h2 : (137.030 : ℝ) < Constants.alphaInv := Numerics.alphaInv_gt
  linarith

/-- A reading of the α seed `4π·11` as a coupling normalization. The seed
equals `(4π) × (stiffness)` with `e² = 1` ONLY under three inputs, the third of
which is precisely the ledger-vs-gauge mismatch: the stiffness used is the
passive-edge (ledger channel) count, which is NOT the gauge-invariant cycle
rank. So this is an identification, not a gauge-theory theorem. -/
structure SeedNormalizationReading : Prop where
  /-- (i) MODEL: Heaviside–Lorentz convention `α = e²/(4π)`. -/
  hl_convention : True
  /-- (ii) IDENTIFICATION: bare charge quantum `e² = 1` (J-cost Hessian `= 1`;
  the particle/antiparticle double-entry factor of `2` is not independently
  ruled out here). -/
  charge_unit_one : True
  /-- (iii) IDENTIFICATION (the load-bearing one): the photon stiffness is taken
  to be the passive-edge ledger channel count `11`, which is not the candidate
  graph cycle-rank count `5`. -/
  stiffness_is_ledger_not_gauge : passive_field_edges D ≠ cube_cycle_rank

What this page does not claim

Not claimed: that the fine-structure constant is derived in this module. Not claimed: that either count 11 or 5 is a photon kinetic coefficient. Not claimed: that a U(1) gauge theory or Maxwell action is constructed from the cube.

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/U1Normalization.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: