simplifiedCascadeCost_eq_zero_iff
plain-language theorem explainer
The equivalence shows that the simplified cascade cost vanishes precisely when the ratio equals the golden ratio phi, for any r greater than 1. Researchers working on variational models of the phi-ladder in Recognition Science would cite this to establish uniqueness of the optimal ratio. The proof reduces the zero-cost condition to the self-similarity defect equaling one via the J-cost characterization, then applies uniqueness of the positive root above one.
Claim. For any real number $r > 1$, let $C(r)$ denote the simplified cascade cost, defined as the J-cost of the self-similarity defect $d(r) = r^2/(r+1)$. Then $C(r) = 0$ if and only if $r = phi$.
background
The module formalizes a simplified variational model for the phi-ladder by measuring the failure of a geometric ratio $r > 1$ to satisfy the self-similar closure $r^2 = r + 1$. The self-similarity defect is defined as $d(r) := r^2 / (r + 1)$, and the simplified cascade cost is the J-cost of this defect. The J-cost function satisfies $J(x) = 0$ if and only if $x = 1$ for $x > 0$, as established in the Cost module and the PhiLadderCutoff variant.
proof idea
The proof is a term-mode biconditional. One direction assumes the cost is zero, deduces that the defect equals one using Jcost_eq_zero_iff applied to the positive defect (from selfSimilarityDefect_pos), then invokes selfSimilarityDefect_eq_one_iff to obtain the quadratic equation, and concludes $r = phi$ by positive_root_unique_above_one. The converse substitutes $r = phi$ and applies the pre-proved simplifiedCascadeCost_phi.
why it matters
This theorem supplies the zero-cost characterization needed for the parent result phi_is_unique_optimal_ratio, which asserts that phi is the unique minimizer of the simplified cascade cost on $(1, ∞)$. It closes the loop on the variational model in the module, confirming that the cost vanishes exactly at the self-similar fixed point phi, consistent with the Recognition Science forcing chain where phi emerges as the unique solution to the self-similarity condition (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.