selfSimilarityDefect_phi
plain-language theorem explainer
The theorem shows that the self-similarity defect ratio evaluates to exactly one at the golden ratio. Workers on simplified variational models for the phi-ladder in Navier-Stokes cascades cite this to confirm the minimum defect. The short tactic proof unfolds the defect definition, applies the algebraic identity phi squared equals phi plus one, and cancels the common factor after confirming the denominator is nonzero.
Claim. Let $r>1$ be a geometric ratio and define the self-similarity defect by $r^2/(r+1)$. Let $phi$ be the golden ratio. Then the defect at $r=phi$ equals 1.
background
In the module on phi as the unique optimal cascade ratio, the self-similarity defect for a geometric ratio r greater than one is defined as r squared over r plus one. This quantity measures how far r deviates from satisfying the self-similar closure relation r squared equals r plus one. The local setting is a simplified variational model for the phi-ladder in Navier-Stokes contexts.
proof idea
The proof unfolds the definition of selfSimilarityDefect to obtain phi squared over phi plus one. It first establishes that phi plus one is nonzero using phi_pos and linarith. Then it rewrites using the phi_sq_eq lemma to replace phi squared with phi plus one, yielding (phi plus one) over (phi plus one). Finally field_simp cancels the common factor to reach one.
why it matters
This result feeds directly into the theorem simplifiedCascadeCost_phi, which concludes that the simplified cascade cost at phi is zero by rewriting with this equality and applying Jcost_one. It fills the step showing that the defect vanishes exactly at the golden ratio, consistent with the module's claim that the canonical cost is minimized at r equals phi. In the Recognition framework this supports the forcing of phi as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.