cert
plain-language theorem explainer
The cert definition constructs a SolarWindCert structure by assigning its four fields directly from sibling theorems establishing positivity and strict inequality greater than one for the Alfvén-to-solar-wind ratio, vanishing J-cost at equal energies, and positivity of phi to the twentieth power. Astrophysicists using Recognition Science models would cite it to certify consistency of the solar wind outflow with phi-ladder scaling and Parker spiral energy balance. The construction is a direct record literal with no additional reasoning steps.
Claim. The definition cert supplies a SolarWindCert structure certifying that the Alfvén-to-solar-wind speed ratio $r$ satisfies $0 < r$ and $1 < r$, that the solar wind J-cost vanishes for any nonzero energy $e$ when the two energies are equal, and that $0 < phi^{20}$.
background
In the Solar Wind from MHD Recognition Dynamics module the solar wind is treated as a continuous plasma outflow whose speed scales as $v_{sw} = v_A phi^3$ and whose termination shock lies at $R_{ts} = R_odot phi^{20}$. The SolarWindCert structure packages four required properties: positivity and strict inequality greater than one for the Alfvén-to-solar-wind ratio, the identity solarWindCost $e$ $e$ = 0 for $e neq 0$, and positivity of $phi^{20}$. These properties are supplied by the upstream theorems alfvenToSolarWindRatio_pos, alfvenToSolarWindRatio_gt_one, solarWindCost_at_eq (which unfolds to Jcost_unit0), and phi20_pos (which applies pow_pos phi_pos). The module documentation describes the setting as a Tier B12 structural theorem with zero axioms or sorrys, confirming J-cost balance at the Parker spiral angle.
proof idea
The definition is a direct structure literal that populates each field of SolarWindCert by reference to the corresponding sibling theorem: alfven_ratio_pos from alfvenToSolarWindRatio_pos, alfven_ratio_gt_one from alfvenToSolarWindRatio_gt_one, cost_at_eq from solarWindCost_at_eq, and phi20_pos from phi20_pos. No tactics, reductions, or auxiliary lemmas are invoked beyond the record construction itself.
why it matters
This definition supplies the concrete SolarWindCert witness that closes the structural claims of the Astrophysics.SolarWindFromMHD module. It instantiates the RS predictions for solar wind speed scaling with $phi^3$ and termination shock radius scaling with $phi^{20}$, together with the J-cost equality at the Parker angle. Within the Recognition Science framework it confirms the self-similar fixed point phi and the eight-tick octave through the exponent 20. No downstream uses are recorded yet, but the certificate supports the module falsifier of solar wind speeds consistently outside the 300-700 km/s band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.