Physics Proton Radius

Proton radius in Recognition Science

Proton radius in Recognition Science is the spatial extent of the proton as derived from the framework's recognition ledger, where recognition is the forced cost of matching a probe to a target. The module ProtonRadius.lean establishes that the radius is a single, probe-independent number, and it provides the structural reason why the muonic and electronic measurements agree.

The central definition is proton_radius_estimate, which takes as inputs a confinement scale h_over_mpc and a strong coupling α_s, and returns (1/4) * h_over_mpc * sqrt(6 * π / α_s). This is a MODEL: it chooses a specific functional form for the radius from confinement and a form factor. The module proves that this estimate is positive whenever both inputs are positive, a THEOREM that guarantees the formula yields a physically meaningful length.

The module also encodes the empirical situation. The CODATA 2018 value is 0.8414 fm, stored as proton_radius_codata. The old, larger value of 0.877 fm differs from CODATA by more than 3%, a fact established by old_value_differs. The key structural claim is leptonic_universality: there exists a single real number equal to the CODATA value, meaning the radius does not depend on whether the probe is a muon or an electron.

Why the muon and electron agree is the point of the module. The muon is heavier than the electron by a factor of φ^11, where φ is the golden ratio, and the muonic Bohr radius is correspondingly smaller, so it probes shorter distances. The module proves muonic_smaller: the muonic radius is less than the electronic one. This difference in probe scale is exactly what the form factor correction form_factor_correction accounts for. The correction is 1 - 0.15 * (Q/L)^2, and the theorem form_factor_near_one proves that when the momentum transfer Q is small relative to the scale L, the correction stays within 0.0015 of unity. The result is that the same underlying radius is recovered by both probes once the probe-dependent correction is applied.

The module's contribution is to make the proton radius puzzle a structural statement rather than a mystery. The radius is not a free parameter that differs between experiments; it is a single number, and the apparent discrepancy is a probe-scale effect. The empirical agreement with CODATA is a check, not a theorem, and the exact derivation of the radius from first principles remains a target.

THEOREM proton_radius_positive · IndisputableMonolith/Physics/ProtonRadius.lean

THEOREM muon_electron_ratio · IndisputableMonolith/Physics/ProtonRadius.lean

THEOREM muonic_smaller · IndisputableMonolith/Physics/ProtonRadius.lean

THEOREM old_value_differs · IndisputableMonolith/Physics/ProtonRadius.lean

THEOREM form_factor_near_one · IndisputableMonolith/Physics/ProtonRadius.lean

What this page does not claim

The proton radius is not derived from first principles; the estimate is a definitional model. The CODATA value is not established by the framework; it is an empirical input. The form factor correction is not claimed to be exact beyond the small-momentum regime.

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/Physics/ProtonRadius.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: