phi_is_unique_optimal_ratio
plain-language theorem explainer
φ uniquely minimizes the simplified cascade cost among ratios r > 1. Researchers modeling self-similar cascades in fluid dynamics via variational principles cite this uniqueness. The argument first invokes non-negativity of the cost, substitutes the known zero value at φ to obtain the inequality, then reduces equality of costs to the zero-set characterization.
Claim. Let $C(r)$ denote the J-cost of the self-similarity defect for a ratio $r > 1$. Then $C(φ) ≤ C(r)$, with equality if and only if $r = φ$.
background
The simplified cascade cost is defined as the J-cost applied to the self-similarity defect of ratio r. The defect measures deviation from the self-similar closure relation r² = r + 1. Upstream lemmas establish that this cost is nonnegative for r > 1, equals zero at φ, and vanishes precisely when r equals φ.
proof idea
The proof obtains non-negativity of the cost at arbitrary r from the nonnegativity lemma. It substitutes the zero value at φ to produce the inequality. For the equality direction, cost equality is reduced to the cost being zero, which forces r = φ by the zero-iff lemma; the converse follows by direct substitution of the zero value at φ.
why it matters
This result confirms φ as the unique optimal ratio in the simplified variational model for the φ-ladder. It aligns with the self-similar fixed point forced at T6 of the unified forcing chain and supports the eight-tick octave structure. The theorem is terminal in its module, with no listed downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.