Pith. sign in
module module high

IndisputableMonolith.Verification.PDGComparison

show as:
view Lean formalization →

Reference table of CODATA 2022 and PDG experimental anchors used to audit Recognition Science predictions. It records the inverse fine-structure constant with uncertainty, electron/muon/tau masses with sigmas, and the RS interval for α⁻¹. Anyone checking numerical agreement of the α pipeline or lepton ladder against published data cites this module. Content is pure constant definitions; no proofs.

claimModule of experimental anchors and RS comparison bounds: CODATA 2022 $\alpha^{-1} = 137.035999177(21)$ with explicit low/high edges; PDG masses $m_e$, $m_\mu$, $m_\tau$ each with one-sigma uncertainties; and the RS-derived interval $[\alpha^{-1}_{\mathrm{RS,lo}}, \alpha^{-1}_{\mathrm{RS,hi}}]$ for direct numerical comparison.

background

Recognition Science predicts dimensionless constants and mass ratios from the forcing chain and the φ-ladder, with no free fit parameters. The inverse fine-structure constant is obtained from a closed α pipeline whose single gap term is $f_{\mathrm{gap}} = w_8 \ln\varphi$, where $w_8$ is the parameter-free 8-tick projection weight. Interval arithmetic then supplies rigorous bounds on $\alpha^{-1}$ (imported from the AlphaBounds numerics module).

Lepton masses sit on the same φ-ladder via the generation definitions (T10 lepton-generation defs): a yardstick times $\varphi$ raised to a rung corrected by a gap term in $Z$. To claim contact with experiment one needs frozen external anchors, not ad-hoc floats.

This module is that anchor layer. It stores CODATA 2022 $\alpha^{-1}$ (central value and $\sigma$, plus explicit lo/hi edges) and PDG central values and sigmas for $e$, $\mu$, $\tau$, side by side with the RS lo/hi interval for $\alpha^{-1}$.

proof idea

Definition module only: no theorems and no tactic proofs. Each declaration is a numeric constant (CODATA/PDG central value, uncertainty, or derived lo/hi edge) or the imported RS interval endpoints for $\alpha^{-1}$. Comparison logic and certified inequalities live downstream; this file only freezes the reference numbers and the RS bound pair.

why it matters in Recognition Science

Verification layer for the no-free-parameters claim. The primer fixes $\alpha^{-1}$ inside roughly $(137.030, 137.039)$; this module supplies the CODATA 2022 target $137.035999177(21)$ and the RS interval endpoints so that containment or tension can be stated as a machine-checkable fact rather than a notebook plot.

It also freezes PDG lepton masses against which the φ-ladder mass formula (yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) is audited. Upstream inputs are Constants (including $\tau_0$), the Alpha and GapWeight pipeline ($w_8$, $f_{\mathrm{gap}}$), AlphaBounds interval certificates, and LeptonGenerations.Defs. No downstream edges are recorded yet; the module is the shared reference surface for later comparison theorems.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (29)