Constants Hartree Rydberg Score Card Row Hartree Over Rest Upper

The Hartree bound

The Hartree energy is the atomic unit of energy, roughly the scale of an electron's binding in a hydrogen atom. In the Recognition Science framework, its value is not stated in joules or electronvolts. Instead, the framework's machine-checked library of formal theorems records a unit-free ratio: the Hartree energy divided by the electron's rest energy, m_e c². The declaration row_hartree_over_rest_upper proves that this ratio is less than 5.33 × 10⁻⁵. A companion theorem, row_hartree_over_rest_lower, proves it is greater than 5.32 × 10⁻⁵. Together they bracket the ratio in a window one part in five thousand wide.

This bracket is not an empirical measurement. It is a theorem derived from the framework's certified inverse fine-structure constant, alphaInv, which itself is bounded between 137.030 and 137.039. The ratio is defined as alpha², and the interval follows by arithmetic from the bounds on alpha. The proof is axiom-clean, meaning it relies only on the standard logical foundations and no framework-specific assumptions. The result is a formal statement about a definition, not a new physical law.

The declaration does not claim to know the Hartree energy in SI units. That would require a separate bridge connecting the dimensionless ratio to measured values of the electron mass, Planck's constant, and the speed of light. The framework explicitly notes this gap. Its falsifier is concrete: if CODATA's inverse fine-structure constant ever fell outside (137.030, 137.039), or if an SI bridge failed to reproduce the Hartree and Rydberg measurements from these ratios, the score card would be wrong. Within the framework, the Hartree energy's place in the atomic scale is fixed relative to the electron's rest energy, and that is all this theorem asserts.

theorem row_hartree_over_rest_upper :
    row_hartree_over_rest < (5.33e-5 : ℝ) := by
  rw [row_hartree_over_rest_eq]
  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  rw [div_lt_iff₀ hpos]
  have hsq : (137.030 : ℝ) ^ 2 < alphaInv ^ 2 := by
    nlinarith [alphaInv_gt, alphaInv_lt]
  have hnum : 1 < (5.33e-5 : ℝ) * (137.030 : ℝ) ^ 2 := by norm_num
  nlinarith

theorem row_hartree_over_rest_lower :
    (5.32e-5 : ℝ) < row_hartree_over_rest := by
  rw [row_hartree_over_rest_eq]
  have hpos : 0 < alphaInv ^ 2 := sq_pos_of_ne_zero (ne_of_gt alphaInv_pos)
  rw [lt_div_iff₀ hpos]
  have hsq : alphaInv ^ 2 < (137.039 : ℝ) ^ 2 := by
    nlinarith [alphaInv_lt, alphaInv_gt]
  have hnum : (5.32e-5 : ℝ) * (137.039 : ℝ) ^ 2 < 1 := by norm_num
  nlinarith

/-- P1-C04 dimensionless Hartree/rest-energy ratio. -/
noncomputable def row_hartree_over_rest : ℝ := alpha ^ 2

What this page does not claim

The Hartree energy has a specific value in joules or electronvolts. The fine-structure constant alpha is derived from first principles within this module. The bracket is a measurement rather than a theorem about a defined ratio.

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