simplifiedCascadeCost_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the simplified cascade cost for every ratio r greater than one. Researchers modeling variational problems on the phi-ladder in fluid dynamics or recognition processes would cite this bound to control energy defects in cascade arguments. The proof is a one-line wrapper that unfolds the cost definition and applies the non-negativity lemma for the J-cost function to the positive self-similarity defect.
Claim. For every real number $r > 1$, the simplified cascade cost $C(r)$ satisfies $0 ≤ C(r)$, where $C(r)$ is the J-cost of the defect measuring deviation from the self-similar closure $r^2 = r + 1$.
background
Recognition Science derives the phi-ladder from the self-similar fixed point of the J-function under the Recognition Composition Law. This module defines a simplified variational model that quantifies the failure of a ratio r > 1 to satisfy r² = r + 1; the canonical cost of that defect is the J-cost applied to the defect term. The J-cost itself is non-negative for positive arguments by the upstream lemma Jcost_nonneg, which follows from the algebraic identity J(x) = (x - 1)² / (2x) and direct positivity verification.
proof idea
The proof is a one-line wrapper. It unfolds the definition of simplifiedCascadeCost to expose the J-cost of the self-similarity defect, then invokes the lemma Jcost_nonneg on the positivity fact supplied by selfSimilarityDefect_pos.
why it matters
This non-negativity result is invoked directly by the parent theorem phi_is_unique_optimal_ratio, which concludes that phi is the unique minimizer of the simplified cascade cost on (1, ∞). The declaration therefore supplies the lower-bound step needed for the variational characterization of the phi-ladder in the Navier-Stokes setting, aligning with the forcing-chain landmark that phi is the self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.