Constants Codata

The quarantined constants

The speed of light c is exactly 299,792,458 meters per second by the SI definition. The reduced Planck constant hbar is about 1.054571817 times 10 to the minus 34 joule-seconds. Newton's gravitational constant G is about 6.67430 times 10 to the minus 11 cubic meters per kilogram per second squared. These are the CODATA 2018 reference values, the standard empirical numbers physicists use for comparisons and reports.

The module proves only that each constant is positive and nonzero, which is what you need to divide by them safely. The real content is structural: the module deliberately keeps these empirical numbers out of the certified surface. The framework's own constants, such as hbar and G derived from the forcing chain, live in a different namespace. The two sets have the same names, so a name collision would break imports. The quarantine means the top-level certificate chain does not depend on the empirical values.

In plain language, the module is a storage room. It holds the measured constants for anyone who needs them, but it keeps them separate from the framework's derived results. The derived constants come from the forcing chain, not from measurement. The empirical values are for checking against the real world, not for building the theory.

/-- Speed of light (exact SI definition). -/
@[simp] noncomputable def c : ℝ := 299792458

lemma c_pos : 0 < c := by unfold c; norm_num

lemma hbar_pos : 0 < hbar := by unfold hbar; norm_num

lemma G_pos : 0 < G := by unfold G; norm_num

/-- Speed of light (exact SI definition). -/
@[simp] noncomputable def c : ℝ := 299792458

What this page does not claim

This module does not derive the constants from the forcing chain. The empirical constants are not part of the certified surface.

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