no_compression_zero_cost
plain-language theorem explainer
J-cost vanishes at unit compression ratio. Turbine modelers would cite this to set the zero baseline for an uncompressed flow stage in phi-spiral geometries. The proof is a direct one-line application of the unit-cost lemma for the J function.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the cost function induced by the multiplicative recognizer.
background
In the Tesla turbine setting, fluid follows a logarithmic spiral between parallel discs with gap governed by phi scaling. The J-cost function, defined via the Cost module as the derived cost of a multiplicative recognizer comparator, quantifies recognition cost of a compression ratio x. Upstream lemma Jcost_unit0 states J(1) = 0 directly from the squared-ratio expression.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This anchors cost accounting for the turbine stack by confirming the trivial case has zero cost, feeding into phi_disc_spacing_optimal and spiral_pitch_one_is_phi results. It aligns with T5 J-uniqueness and non-negativity of cost in ObserverForcing. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.