selfSimilarityDefect_eq_one_iff
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.