Clag_pos
Clag_pos establishes that the ILG constant Clag equals 1 over phi to the fifth power is strictly positive. Workers on the Recognition Science constants bundle or the Law of Existence structure would cite it to secure positivity when scaling quantities on the phi ladder. The proof is a compact term-mode chain that applies phi positivity, power positivity, and the reciprocal rule directly to the definition of Clag.
claimLet $Clag := 1/phi^5$. Then $Clag > 0$.
background
Clag is the noncomputable definition $1/(phi^5)$ appearing in the ILG submodule. Phi denotes the self-similar fixed point of the Recognition forcing chain. The upstream Constants structure from LawOfExistence packages several real constants (Knet, Cproj, Ceng, Cdisp) together with the hypothesis that Knet is nonnegative.
proof idea
The term proof first obtains 0 < phi from phi_pos, lifts it to 0 < phi^5 via pow_pos, then applies inv_pos.mpr to the reciprocal definition of Clag.
why it matters in Recognition Science
The lemma supplies the basic positivity fact required by the abstract Constants bundle in LawOfExistence, ensuring that Clag can appear safely in later inequalities. It closes a routine positivity obligation inside the ILG constants section of the Recognition Science framework. No downstream citations are recorded, but the result anchors any phi-ladder scaling that uses this constant.
scope and limits
- Does not compute a numerical value for Clag.
- Does not relate Clag to alpha, G, or other framework constants.
- Does not address physical units or interpretation.
formal statement (Lean)
45lemma Clag_pos : 0 < Clag := by
proof body
Term-mode proof.
46 have hφ : 0 < phi := phi_pos
47 have hpow : 0 < phi ^ (5 : Nat) := pow_pos hφ 5
48 simpa [Clag, one_div] using inv_pos.mpr hpow
49
50end Constants
51end IndisputableMonolith