climateJCost_nonneg
plain-language theorem explainer
The J-cost on any finite-dimensional climate phase point is non-negative. Climate modelers citing Recognition Science would use this to anchor the claim that the vacuum state realizes the global minimum cost on the attractor. The proof is a short tactic sequence that unfolds the sum definition and reduces each term to the core Jcost_nonneg lemma via Finset.sum_nonneg and positivity.
Claim. For any natural number $N$ and any climate phase point $s : Fin N → ℝ$, the climate J-cost satisfies $0 ≤ ∑_{i} J(1 + s_i^2)$, where $J$ is the Recognition Science cost function.
background
ClimatePhasePoint N is the type Fin N → ℝ, an idealized real-valued state vector with N components. climateJCost is defined as the Finset sum over i of Cost.Jcost(1 + (s i)^2). The module Climate.AttractorStructure formalizes the prediction that the climate manifold possesses an attractor on which the long-term trajectory spends most time and whose J-cost is the global minimum of the energy-entropy field.
proof idea
The proof unfolds climateJCost to expose the Finset sum, applies Finset.sum_nonneg to reduce to per-term non-negativity, invokes Cost.Jcost_nonneg on the positive argument 1 + (s i)^2, and closes with the positivity tactic.
why it matters
This supplies the cost_nonneg field of AttractorStructureCert, which certifies the master theorem vacuum_is_global_minimum asserting that the zero state is the global J-cost minimum. It fills the basic positivity requirement for Element 84 (Domain B: Climate Dynamics) in the Recognition Science forcing chain, confirming that attractor J-cost cannot be negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.