w8
plain-language theorem explainer
The fine-structure weight w₈ is fixed at the real value 4. It is the numerical coefficient that enters the RS formula for α⁻¹ through the gap term w₈ log φ. Anyone assembling α⁻¹, the gap weight f_gap, or the countable RS field cites this constant. The body is a one-line real literal.
Claim. The fine-structure weight is the real constant $w_8 := 4$.
background
In the Primitive Recognition Calculus minimal-field module, the RS constants are adjoined as named reals so that the subfield they generate can be shown countable. The fine-structure weight $w_8$ is one such named real: it is the coefficient in the gap term that appears in the closed-form inverse fine-structure constant
$$\alpha^{-1} = 44\pi,\exp\bigl(-w_8\ln\varphi/(44\pi)\bigr).$$
The module doc and the local comment stress that the exact numerical value is irrelevant to countability: whatever fixed real is chosen is simply adjoined as an element of the generating set. Downstream, the same symbol feeds the gap weight $f_{\mathrm{gap}}(w_8)=w_8\log\varphi$ used in higher-order $\alpha$ expansions and in the gate-tightened admissibility class that pins the RS-assembled coupling.
proof idea
Pure definition: the real literal 4 is assigned to the constant. No lemmas, no tactics, no computation.
why it matters
This constant is the numerical seed for the RS fine-structure assembly. It is consumed by alphaInv in the same module, by the membership proof that $\alpha^{-1}$ lies in the countable field $T$, by the gap weight $f_{\mathrm{gap}}$ in higher-order $\alpha$ numerics, and by the gate-tightened class $L_{\alpha}^{\mathrm{RS}}$ that forces the candidate coupling to equal the RS formula. In the broader framework it sits next to the $\alpha^{-1}$ band $(137.030,137.039)$ and the $\varphi$-ladder mass formula: fixing $w_8=4$ makes the transcendental expression for $\alpha^{-1}$ a concrete element of the minimal RS field rather than a free parameter. Gravity-side star-kernel stationarity proofs also pull the symbol when class weights are specialized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.