selfSimilarityDefect_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of the defect at r = phi.
- Does not treat the case r ≤ 1 or complex ratios.
- Does not invoke the Recognition Composition Law or the full eight-tick octave structure.
- Does not address stability under perturbations of the cascade model.
Lean usage
have hpos : 0 < selfSimilarityDefect r := selfSimilarityDefect_pos hrformal statement (Lean)
31theorem selfSimilarityDefect_pos {r : ℝ} (hr : 1 < r) :
32 0 < selfSimilarityDefect r := by
proof body
Term-mode proof.
33 unfold selfSimilarityDefect
34 positivity
35