selfSimilarityDefect_eq_one_iff
For real r > 1 the defect ratio r²/(r+1) equals 1 precisely when r obeys the quadratic r² = r + 1. Workers on the phi-ladder variational model cite the equivalence to locate the unique zero of simplified cascade cost. The proof unfolds the defect definition then splits the biconditional, clearing the denominator by field simplification and finishing each direction with linear arithmetic.
claimFor real $r > 1$, the defect ratio $r^2/(r+1)$ equals 1 if and only if $r^2 = r + 1$.
background
The defect ratio is defined by selfSimilarityDefect r := r²/(r+1). The module supplies a simplified variational model for the phi-ladder that quantifies the failure of any geometric ratio r > 1 to obey the self-similar closure r² = r + 1; the canonical cost of that defect is minimized exactly at r = phi. The upstream definition of selfSimilarityDefect supplies the explicit ratio whose level set at unity is characterized by the present equivalence.
proof idea
Unfold selfSimilarityDefect to obtain the equation r²/(r+1) = 1. Split the biconditional with constructor. The forward direction applies field_simp using r+1 ≠ 0 (from r > 1) then linarith. The reverse direction substitutes the quadratic hypothesis and repeats field_simp.
why it matters in Recognition Science
The equivalence is invoked inside simplifiedCascadeCost_eq_zero_iff to conclude that the simplified cascade cost vanishes precisely at r = phi. It therefore supplies the algebraic step that establishes phi as the unique optimal cascade ratio in the module, consistent with the self-similar fixed point forced at T6 of the Recognition Science chain.
scope and limits
- Does not extend the equivalence to r ≤ 1.
- Does not incorporate the full J-cost or Recognition Composition Law.
- Does not treat multi-scale or non-geometric cascades.
- Does not prove uniqueness of the positive root of the quadratic.
Lean usage
theorem use_site {r : ℝ} (hr : 1 < r) (h : selfSimilarityDefect r = 1) : r ^ 2 = r + 1 := (selfSimilarityDefect_eq_one_iff hr).1 hformal statement (Lean)
47theorem selfSimilarityDefect_eq_one_iff {r : ℝ} (hr : 1 < r) :
48 selfSimilarityDefect r = 1 ↔ r ^ 2 = r + 1 := by
proof body
Tactic-mode proof.
49 unfold selfSimilarityDefect
50 have hr1 : r + 1 ≠ 0 := by linarith
51 constructor
52 · intro h
53 field_simp [hr1] at h
54 linarith
55 · intro h
56 rw [h]
57 field_simp [hr1]
58