Constants Derivation Units Self Consistent

The consistency theorem

In physics, a system of units is self-consistent when its definitions do not contradict one another. The Recognition Science library contains a machine-checked theorem, units_self_consistent, which establishes exactly this for its derived units. The theorem states that if you start with a positive time unit τ₀, a positive length unit ℓ₀, and a positive speed c', and you define them so that ℓ₀ = c'·τ₀, then the derived value of the reduced Planck constant ℏ' must equal π·c'⁵·τ₀²/G'. This is a formal statement that the framework's definitions of time, length, and speed are mutually compatible.

The theorem is proved in the machine-checked library of formal theorems, meaning it is a verified result with no gaps in its logical derivation. It is not a physical measurement or an empirical claim; it is a consistency check on the framework's own definitions. The theorem shows that if the framework's time unit τ₀ is defined as √(ℏ·G/(π·c³))/c, and the length unit ℓ₀ is defined as c·τ₀, then the derived value of ℏ from these units matches the original value. This is a mathematical identity, not a new physical law.

What the theorem does not claim is that these units are the only possible ones, or that they are preferred by nature. It does not claim that the speed of light is 299792458 m/s in any absolute sense; that value is a definition, not a derivation. The theorem also does not claim that the values of ℏ, G, and c used in the definitions are measured or derived from first principles. It merely shows that the framework's unit system is internally consistent, given those values as inputs.

The practical consequence is that the framework's constants do not contradict each other. If the time unit is defined one way and the length unit another, the speed of light derived from them is exactly the defined value. This is a necessary condition for the framework to be a coherent system of units, and the theorem verifies it formally.

theorem units_self_consistent :
    ∀ (ℏ' G' c' : ℝ), ℏ' > 0 → G' > 0 → c' > 0 →
    tau0 = sqrt (ℏ' * G' / (Real.pi * c' ^ 3)) / c' →
    ell0 = c' * tau0 →
    ℏ' = Real.pi * c' ^ 5 * tau0 ^ 2 / G' := by
  intro ℏ' G' c' hℏ hG hc htau _hell
  have hc_ne : c' ≠ 0 := ne_of_gt hc
  have hG_ne : G' ≠ 0 := ne_of_gt hG
  have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
  have hc3 : c' ^ 3 ≠ 0 := pow_ne_zero 3 hc_ne
  have hc5 : c' ^ 5 ≠ 0 := pow_ne_zero 5 hc_ne
  have hinner_nonneg : 0 ≤ ℏ' * G' / (Real.pi * c' ^ 3) := by
    apply div_nonneg (mul_nonneg (le_of_lt hℏ) (le_of_lt hG))
    exact le_of_lt (mul_pos Real.pi_pos (pow_pos hc 3))
  have hsq : tau0 ^ 2 = ℏ' * G' / (Real.pi * c' ^ 5) := by
    rw [htau, div_pow, sq_sqrt hinner_nonneg]
    field_simp
  rw [hsq]
  field_simp

def derivation_status : String :=
  "✓ tau0_sq_eq PROVEN\n" ++
  "✓ planck_relation_satisfied PROVEN\n" ++
  "✓ G_relation_satisfied PROVEN\n" ++
  "✓ tau0_planck_relation PROVEN\n" ++
  "✓ units_self_consistent PROVEN\n" ++
  "✓ NO PROOF HOLES"

What this page does not claim

The theorem does not claim that the framework's units are the only possible ones or that they are preferred by nature. The theorem does not claim that the speed of light is 299792458 m/s in any absolute sense; that value is a definition, not a derivation. The theorem does not claim that the values of ℏ, G, and c used in the definitions are measured or derived from first principles.

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