Constants Gap Weight

Gap weight and its derivation

Gap weight, written w₈, is a single number that Recognition Science uses to build the fine-structure constant. It is defined as w₈ = (348 + 210√2 − (204 + 130√2)φ) / 7, where φ is the golden ratio. Numerically it is approximately 2.49056927545. The number is not fitted. It is the Parseval-normalized 64-cell projection of the discrete Fourier transform of the canonical φ-pattern on eight ticks.

The derivation is a forced chain, not a choice. The pattern φ^t for t = 0, …, 7 is forced by the eight-tick cycle and the golden-ratio ladder. The discrete Fourier transform of that pattern has a closed form established by geometric-series summation. The spectral weight uses sin²(kπ/8), which is the spectrum of the discrete derivative on Z/8, and the φ⁻ᵏ factor is the conjugate ladder envelope. The 64 cells come from 8 ticks times 8 vertices, where the 8 vertices come from 2³. Combining these pieces, pairing modes (1,7), (2,6), (3,5), and clearing denominators lands on the closed form above. The integers 348, 210, 204, 130, and 7 are emergent from the algebra, not selected to match data.

The equality between the projected weight and the closed form is established by Lean theorem w8_from_eight_tick, with zero sorry and zero RS-specific axioms. A separate sanity-check certificate proves that the unnormalized sum over modes is not equal to the canonical w₈, which blocks the error of confusing the two. The canonical w₈ is the one that goes through Parseval and 64-cell scaling.

In the α pipeline, the gap term is f_gap = w₈ · ln(φ). The module also defines certified rational bounds for this value, packaged as a hypothesis f_gap_bounds_hypothesis. That hypothesis is a numerical bound claim, not a theorem; the exact value of α remains an open target.

MODEL w8_from_eight_tick · IndisputableMonolith/Constants/GapWeight.lean

THEOREM w8_from_eight_tick · IndisputableMonolith/Constants/GapWeight.lean

THEOREM w8_pos · IndisputableMonolith/Constants/GapWeight.lean

What this page does not claim

This page does not claim that the fine-structure constant is derived exactly. This page does not claim that the integers in the closed form were chosen to fit measured data. This page does not claim that the numerical bounds for f_gap are established theorems.

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