laminar_equilibrium
plain-language theorem explainer
The theorem shows the J-cost function equals zero at unit argument, modeling uniform laminar flow with no recognition cost. Researchers deriving hydrodynamics from recognition principles cite it as the equilibrium base case. It follows directly from the unit lemma for J-cost via term application.
Claim. For the recognition cost function $J(x) = (x-1)^2 / (2x)$, it holds that $J(1) = 0$, which models uniform laminar flow.
background
The J-cost function measures recognition cost of flow states via the squared ratio $J(x) = (x-1)^2 / (2x)$. In this module, hydrodynamics emerges from recognition on a fluid lattice with five regimes for configDim D = 5. Equilibrium corresponds to uniform flow where cost vanishes, while turbulence incurs positive cost. The upstream lemma establishes J(1) = 0 by simplification of the definition.
proof idea
The proof is a one-line term wrapper that applies the upstream unit lemma establishing Jcost at argument 1 equals zero by direct simplification.
why it matters
This supplies the laminar zero field in the HydrodynamicsCert definition, which bundles the five regimes with laminar at zero cost and turbulent at positive cost. It completes the equilibrium case in the RS hydrodynamics derivation, consistent with the module statement that at equilibrium J = 0 for uniform flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.