Constants Ilg Clag Pos

The positivity lemma

The declaration Clag_pos is a lemma in the Recognition Science library. It states that the constant Clag is positive: Clag > 0. The proof is a short chain of standard facts: the golden ratio φ is positive, so its fifth power is positive, and the reciprocal of a positive number is positive. Nothing in the proof depends on any special axiom; it is a purely formal consequence of the definitions.

In the framework, Clag is defined as 1 / φ^5. It is one of several constants that appear in the framework's derivations. The lemma itself is modest: it establishes only that this number is greater than zero. It does not say what the number is, how large it is, or what role it plays in any physical theory. It is a building block, not a result about the world.

What the lemma does not claim is worth stating plainly. It does not assert that Clag equals any measured physical quantity. It does not say that the framework's constants are correct or that they match experiment. It does not even say that Clag is the value of the fine-structure constant or any other coupling. Those are separate questions, and this lemma is silent on them.

The value of the lemma is in what it enables. A positive constant is one that can appear in inequalities, in ratios, and in arguments that require a nonzero denominator. The lemma is a small but necessary step in the framework's formal development. It is the kind of fact that a machine-checked library needs to have on record before it can proceed to more substantial claims.

lemma Clag_pos : 0 < Clag := by
  have hφ : 0 < phi := phi_pos
  have hpow : 0 < phi ^ (5 : Nat) := pow_pos hφ 5
  simpa [Clag, one_div] using inv_pos.mpr hpow

lemma Clag_pos : 0 < Clag := by
  have hφ : 0 < phi := phi_pos
  have hpow : 0 < phi ^ (5 : Nat) := pow_pos hφ 5
  simpa [Clag, one_div] using inv_pos.mpr hpow

@[simp] noncomputable def Clag : ℝ := 1 / (phi ^ (5 : Nat))

What this page does not claim

Clag equals any measured physical quantity. The framework's constants match experiment. Clag is the fine-structure constant or any other coupling.

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