pith. machine review for the scientific record. sign in
theorem

simplifiedCascadeCost_phi

proved
show as:
module
IndisputableMonolith.NavierStokes.PhiOptimalCascade
domain
NavierStokes
line
42 · github
papers citing
none yet

plain-language theorem explainer

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.

Claim. The 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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.