AttractorStructureCert
plain-language theorem explainer
The AttractorStructureCert structure packages three properties of the climate J-cost: non-negativity over all phase points, exact zero at the vacuum state, and global minimality of that vacuum. Climate modelers in the Recognition Science setting cite it to certify that the attractor occupies the lowest-cost configuration on the energy-entropy field. The definition simply bundles three already-proved lemmas on the summed J-cost function without additional reasoning steps.
Claim. Let $J$ be the J-cost on climate phase space, defined as the sum of per-component costs $Jcost(1 + s_i^2)$. The certificate asserts that $0 ≤ J(s)$ for every state vector $s ∈ ℝ^N$, that $J(0) = 0$, and that $J(0) ≤ J(s)$ for all $s$.
background
ClimatePhasePoint N is the type Fin N → ℝ, an idealized N-component real state vector in climate phase space. climateJCost sums Cost.Jcost(1 + (s i)^2) over all components, inheriting non-negativity from the upstream theorem cost_nonneg which states that the cost of any recognition event is non-negative. The module sets the local context as Element 84 in Domain B: the climate manifold possesses an attractor structure on which the long-term trajectory converges and the RS prediction requires the attractor's J-cost to be the global minimum.
proof idea
This is a structure definition whose three fields are filled by direct reference to sibling lemmas: climateJCost_nonneg supplies the non-negativity field, vacuum_climate_zero_cost supplies the vacuum-zero field, and vacuum_is_global_minimum supplies the vacuum-minimum field. No tactics or reductions occur inside the structure itself.
why it matters
The structure supplies the master certificate for the climate attractor in Element 84. It is instantiated by the downstream attractorStructureCert definition, which packages the three properties to support further climate modeling. The result aligns with the Recognition Science claim that the attractor's J-cost is the global minimum on the climate energy-entropy field and rests on the general non-negativity of J-cost established in ObserverForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.