vacuum_is_global_minimum
plain-language theorem explainer
The vacuum state achieves the global minimum J-cost over the entire climate phase space. Climate modelers working in Recognition Science would cite it to anchor the attractor as the equilibrium configuration. The proof is a one-line term reduction that rewrites the vacuum cost to zero and invokes non-negativity of the cost function.
Claim. For any natural number $N$ and any climate phase point $s$ (a real vector with $N$ components), the J-cost of the zero vector satisfies $J(0) ≤ J(s)$, where $J$ denotes the sum of per-component costs $Cost.Jcost(1 + s_i^2)$.
background
The Climate.AttractorStructure module formalizes the RS claim that climate dynamics possess an attractor whose J-cost is the global minimum on the phase-space energy/entropy field. A ClimatePhasePoint is an idealized real-valued state vector with $N$ components. The associated climateJCost is the sum over components of Cost.Jcost applied to $1 + s_i^2$ each.
proof idea
The term proof rewrites the left-hand side via the vacuum_climate_zero_cost lemma (which shows the zero vector has J-cost exactly zero) and then applies the climateJCost_nonneg theorem to the arbitrary state $s$.
why it matters
This result supplies the final ingredient for the master certificate attractorStructureCert, which packages non-negativity, zero vacuum cost, and global minimality. It directly supports the module's statement that long-term trajectories converge to the low-dimensional attractor of minimal J-cost, consistent with the J-uniqueness property in the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.