Constants Codata C Pos

The positivity lemma

The speed of light in a vacuum is exactly 299,792,458 meters per second, a number fixed by the SI definition since 1983. In the Recognition Science framework's machine-checked library of formal theorems, this value lives in a quarantined module of empirical constants, kept separate from the framework's own derived quantities. The declaration c_pos is a lemma stating that this constant is greater than zero: 0 < c.

The proof is trivial. The constant c is defined as 299,792,458, and the lemma simply unfolds that definition and verifies the number is positive. The same pattern proves positivity for the reduced Planck constant and Newton's gravitational constant. These three lemmas exist so that other formal arguments can safely divide by these quantities or take their square roots without hitting a zero denominator.

In Recognition Science, the framework proves its own constants: hbar equals phi to the minus fifth power and G equals phi to the fifth over pi, both derived from the forcing chain rather than measured. The CODATA constants are deliberately quarantined because they are empirical inputs, not derived results. The c_pos lemma does not say the speed of light is a derived quantity, does not say it emerges from recognition costs, and does not claim any physical law. It only states a fact about a number that happens to be positive.

What the lemma does establish is a small piece of hygiene: the formal library can rely on c being nonzero whenever it needs to divide by the speed of light in a numeric comparison or empirical report. Without this lemma, any formal proof involving c in a denominator would require an extra side condition. With it, the library has a one-line certificate that the constant is usable.

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

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

What this page does not claim

The speed of light is derived from recognition costs or any framework principle. The positivity lemma establishes any physical law or measurement result. The CODATA constants are part of the framework's certified theorem 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: