Clag_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.