theorem proved term proof

`old_value_differs`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  58theorem old_value_differs : 0.877 - proton_radius_codata > 0.03 := by norm_num

Term-mode proof.

  59
  60/-- RS form factor correction from standard dipole. -/

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
proton_radius_codata in IndisputableMonolith.Physics.ProtonRadius decl_use