compression_has_cost
plain-language theorem explainer
The theorem establishes that the recognition cost J evaluated at the golden ratio φ is strictly positive. Turbine designers and fluid dynamicists modeling φ-scaled compression stages cite this to confirm that the self-similar fixed point carries positive though minimal cost. The proof is a direct algebraic reduction: rewrite J(φ) via its squared identity then apply standard positivity of squares and division over positives.
Claim. $0 < J(φ)$ where $J(x) = (x-1)^2/(2x)$ for $x > 0$.
background
In the Tesla turbine setting, fluid follows logarithmic spirals whose per-turn compression ratio equals φ when the pitch parameter κ equals 1. The J-cost function measures the multiplicative defect of a ratio x and admits the closed form J(x) = (x-1)^2/(2x) for x ≠ 0. Upstream lemmas supply 1 < φ together with φ ≠ 0 and φ > 0, which are the only arithmetic facts required here.
proof idea
Term-mode proof begins with phi_pos. It rewrites the goal by Jcost_eq_sq applied to phi_ne_zero, producing (φ-1)^2/(2φ). Positivity follows from div_pos whose numerator is shown positive by sq_pos_of_pos on (φ-1) > 0 (from one_lt_phi) and whose denominator is positive by mul_pos of 2 and phi_pos.
why it matters
The result supplies the positivity ingredient for tesla_turbine_master, which certifies the full φ-spiral engine: optimal disc spacing, κ=1 pitch, and Fibonacci disc counts all minimize J-cost. It directly supports the claim that φ is the unique self-similar fixed point with minimal non-trivial compression cost, closing the T6 step of the forcing chain inside the flight module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.