climateJCost
plain-language theorem explainer
The climate J-cost sums the per-component J-costs of a phase-space vector s, with each term Jcost(1 + s(i)^2). Climate modelers working in the Recognition Science framework would cite this to quantify total recognition cost on the climate manifold. The definition is a direct finite sum over Fin N using the base Cost.Jcost function.
Claim. For a climate phase point $s$ with $N$ components, the climate J-cost is $J(s) = sum_{i=1}^N J(1 + s_i^2)$, where $J$ is the J-cost function and each $s_i$ is a real component of the state vector.
background
The Climate Attractor Structure module treats the climate manifold as having an attractor on which trajectories converge to a low-dimensional set. A ClimatePhasePoint is defined as an idealized real-valued state vector with N components, represented as a map from Fin N to the reals. The J-cost of a recognition event is the base cost function applied to the state; upstream definitions include the derived cost from multiplicative recognizers and the direct Jcost on recognition events.
proof idea
This is a definition that directly computes the sum over Finset.univ of Cost.Jcost applied to the transformed component (1 + (s i)^2). It aggregates the individual costs without additional lemmas or tactics beyond the standard sum operator.
why it matters
This definition supplies the cost function required by the master certificate AttractorStructureCert and the supporting theorems climateJCost_nonneg, vacuum_climate_zero_cost, and vacuum_is_global_minimum. It implements the J-cost aggregation for Element 84 (climate dynamics) in the Recognition Science chain, enabling the claim that the vacuum state realizes the global minimum cost on the climate field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.