pith. machine review for the scientific record. sign in
theorem proved term proof high

simplifiedCascadeCost_phi

show as:
view Lean formalization →

The declaration establishes that the simplified cascade cost at the golden ratio φ equals zero. Researchers modeling self-similar structures in fluid dynamics or tracing the φ-ladder in Recognition Science would cite this normalization result. The proof is a direct term-mode reduction that unfolds the cost definition, substitutes the defect value at φ, and applies the J-cost normalization at unity.

claimThe J-cost of the self-similarity defect of the golden ratio φ vanishes: $J(δ(φ)) = 0$, where $δ(r)$ quantifies the deviation of ratio $r > 1$ from the closure $r^2 = r + 1$.

background

This module develops a simplified variational model for the φ-ladder in the Navier-Stokes setting. The self-similarity defect for a ratio $r > 1$ measures failure of the geometric closure $r^2 = r + 1$. The simplified cascade cost is defined as the J-cost applied to this defect value. Upstream, Jcost_one asserts the normalization axiom $J(1) = 0$. The companion result selfSimilarityDefect_phi shows the defect equals 1 exactly at φ.

proof idea

The proof is a one-line term-mode wrapper. It unfolds the definition of simplifiedCascadeCost to expose Jcost of the defect, rewrites the defect at φ to 1 via selfSimilarityDefect_phi, and concludes by exact application of Jcost_one.

why it matters in Recognition Science

This result normalizes the cascade cost to zero at φ and feeds directly into phi_is_unique_optimal_ratio, which proves φ is the unique minimizer of the cost on $(1, ∞)$ with equality only at φ. It instantiates the Recognition Science forcing of φ as the self-similar fixed point (T6) within the eight-tick octave. The theorem closes the normalization step required for the variational model of turbulence cascades.

scope and limits

formal statement (Lean)

  42theorem simplifiedCascadeCost_phi : simplifiedCascadeCost phi = 0 := by

proof body

Term-mode proof.

  43  unfold simplifiedCascadeCost
  44  rw [selfSimilarityDefect_phi]
  45  exact Jcost_one
  46

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.