solarWindCost_at_eq
plain-language theorem explainer
Establishes that the J-cost on the kinetic-to-thermal energy ratio vanishes exactly when the two energies are equal. Plasma modelers and Recognition Science users cite it to anchor the zero-cost equilibrium inside solar wind outflow calculations. The proof is a one-line term wrapper that unfolds the ratio definition, rewrites to unity, and applies the Jcost base-case lemma.
Claim. Let $e$ be a nonzero real number. Then the J-cost of the kinetic-to-thermal energy ratio is zero at equality: $Jcost(e/e)=0$.
background
The solarWindCost definition applies Jcost directly to the ratio of kinetic energy to thermal energy. The upstream Jcost_unit0 lemma states that Jcost(1)=0, which follows from the explicit squared-ratio form J(x)=(x-1)^2/(2x). This theorem lives inside the Solar Wind from MHD Recognition Dynamics module, whose module doc derives structural properties of coronal outflows from recognition dynamics, including the speed relation v_sw = v_A φ^3 and termination shock radius scaling as φ^20.
proof idea
One-line term-mode wrapper. It unfolds the solarWindCost definition to expose Jcost on the ratio, rewrites the ratio to 1 by div_self under the nonzero hypothesis, and applies the Jcost_unit0 lemma to obtain zero.
why it matters
Supplies the cost_at_eq field inside the SolarWindCert structure that certifies the overall solar wind model. It isolates the zero J-cost equilibrium point, consistent with the module's focus on J-cost at the Parker spiral angle. The result closes a basic case in the Recognition Science derivation of astrophysical outflows from the single J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.