cert
plain-language theorem explainer
cert constructs the ThermohalineCert record by supplying zero equilibrium buoyancy cost, non-negative costs for positive weights, and positive AMOC timescale. Oceanographers modeling AMOC stability would cite it to anchor J-cost predictions in thermohaline dynamics. The definition is a direct record construction that delegates each field to a prior lemma.
Claim. Let $C(w,c) := J(w/c)$ denote buoyancy cost with $J$ the recognition cost. The certificate cert satisfies: $C(b,b)=0$ for all $b≠0$; $C(w,c)≥0$ whenever $w>0$ and $c>0$; and the AMOC timescale $τ>0$.
background
The module derives AMOC properties from the J-cost function. AMOC strength is a J-cost reading on the buoyancy ratio between warm saline inflow and cold freshwater deepening, with characteristic timescale φ^8 years. The ThermohalineCert structure bundles three properties: zero cost at equal buoyancy, non-negative cost for positive weights, and positive timescale. These rest on the upstream result that the cost of any recognition event is non-negative, together with local lemmas showing J(1)=0 after division and positivity of φ^8.
proof idea
The definition builds the record by assigning cost_at_equilibrium to buoyancyCost_at_equilibrium (which reduces to Jcost_unit0 after div_self), cost_nonneg to buoyancyCost_nonneg (which applies Jcost_nonneg to the positive ratio), and amoc_pos to amocTimescale_pos (which follows from pow_pos on phi_pos). It is a direct structure construction.
why it matters
This definition supplies the concrete certificate that realizes the structural theorem for the first Oceanography module. It embeds the general cost_nonneg result into the buoyancy cost and confirms the φ^8 timescale consistent with RAPID multi-decadal variability. The module doc identifies the falsifier as any observed AMOC timescale outside the (20,100) year band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.