selfSimilarityDefect
plain-language theorem explainer
The declaration defines the self-similarity defect ratio for a geometric cascade as r squared over r plus one. Researchers analyzing variational models for the phi-ladder in Recognition Science would cite this when quantifying deviation from self-similar closure. The definition is a direct algebraic expression with no lemmas or reductions applied.
Claim. For a ratio $r$, the self-similarity defect ratio is defined by $d(r) = r^2 / (r + 1)$.
background
Recognition Science derives the phi-ladder from the self-similar fixed point of the J-function, where J(x) equals (x + x inverse)/2 minus 1. The module sets up a simplified variational model for cascades by measuring failure of a ratio r greater than 1 to obey the closure relation r squared equals r plus 1. The defect supplies the canonical cost that is minimized exactly at r equals phi.
proof idea
This is a direct definition that sets the defect ratio to the explicit algebraic form r squared divided by r plus one. No upstream lemmas are invoked; the expression is introduced as the primitive quantity for the cascade cost.
why it matters
The definition supplies the core quantity used by selfSimilarityDefect_phi to establish that the defect equals one at phi and by simplifiedCascadeCost to form the J-cost of the defect, which vanishes at phi. It fills the module's proposition that phi is the unique optimal cascade ratio, linking directly to the T6 self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.