selfSimilarityDefect_pos
plain-language theorem explainer
The theorem establishes that the self-similarity defect ratio r²/(r+1) is strictly positive for every real r greater than 1. Researchers modeling the phi-ladder via variational cascade costs in fluid dynamics would cite this to guarantee that the cost function is well-defined and positive before minimization. The proof is a one-line wrapper that unfolds the defect definition and applies the positivity tactic.
Claim. For every real number $r$ with $r > 1$, the self-similarity defect ratio satisfies $r^2 / (r + 1) > 0$.
background
This result sits inside the module that formalizes a simplified variational model for the φ-ladder. The model measures the failure of a geometric ratio r > 1 to obey the self-similar closure r² = r + 1; the canonical defect is defined as r² / (r + 1) and then fed into the J-cost to produce the simplified cascade cost. The upstream definition states that selfSimilarityDefect is the self-similarity defect ratio for a geometric cascade, with the explicit formula r² / (r + 1).
proof idea
The proof is a one-line wrapper that unfolds selfSimilarityDefect and applies the positivity tactic to the resulting rational expression under the hypothesis r > 1.
why it matters
The lemma is invoked in the proofs of simplifiedCascadeCost_eq_zero_iff and simplifiedCascadeCost_nonneg, which together show that the simplified cascade cost vanishes if and only if r equals phi and is otherwise non-negative. This supports the Recognition Science claim that phi is the unique self-similar fixed point (T6) that minimizes the defect on (1, ∞) and therefore the unique optimal ratio on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.