cruise_equilibrium
plain-language theorem explainer
In Recognition Science the J-cost vanishes at argument 1. Aerodynamic modelers cite the result to encode cruise equilibrium where net recognition cost is zero. The proof is a direct one-line application of the unit lemma for Jcost.
Claim. The recognition cost function satisfies $J(1)=0$.
background
J-cost is defined by $J(x)=(x-1)^2/(2x)$. The aerodynamics module treats flight as recognition-cost balance among five forces (lift, drag, thrust, weight, moment) with equilibrium at total J-cost zero. This rests on the upstream lemma Jcost_unit0 which states the zero value at unit argument.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This supplies the cruise-equilibrium component to the aerodynamicsCert definition. It instantiates the J=0 balance required for stable flight in the RS framework and links directly to the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.