ClimatePhasePoint
plain-language theorem explainer
ClimatePhasePoint is the type of an N-component real vector representing an idealized state in climate phase space. Climate dynamics researchers in the Recognition Science program cite it when stating theorems about J-cost minima on attractors. The declaration is a direct type abbreviation with no further axioms or computation.
Claim. For each natural number $N$, a climate phase point is an arbitrary function $s : [N] → ℝ$, where $[N]$ denotes the finite set of $N$ indices.
background
Module Climate.AttractorStructure develops Element 84 of Recognition Science: the climate manifold possesses an attractor on which the long-term trajectory spends most time, and RS asserts that this attractor realizes the global minimum of the J-cost functional. The J-cost itself is supplied by upstream definitions: ObserverForcing.cost sets the cost of any recognition event to Cost.Jcost of its state, while MultiplicativeRecognizerL4.cost extracts the same quantity from the comparator of a multiplicative recognizer. PhiForcingDerived.of and DAlembert.LedgerFactorization.of supply the underlying J structure and ledger factorization used to guarantee non-negativity.
proof idea
One-line type abbreviation that directly sets ClimatePhasePoint N equal to the function type Fin N → ℝ.
why it matters
The definition supplies the domain for the downstream master certificate AttractorStructureCert and the theorem vacuum_is_global_minimum, both of which prove that the zero vector is the unique global J-cost minimum on climate phase space. This anchors the module claim that the climate attractor is the J-cost minimum, consistent with the Recognition Composition Law and the non-negativity results imported from Cost and ObserverForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.