geoengineeringRiskCert
plain-language theorem explainer
This definition constructs the geoengineering risk certificate by packaging a decidable count of five approaches with the canonical J-cost threshold. Climate analysts working inside the Recognition Science framework cite it when mapping intervention-induced flux ratios to cascade costs. The construction is a direct structure record that pulls the cardinality from a finite-type decision procedure and pairs it with the pre-established canonical certificate.
Claim. The geoengineering risk certificate is the structure whose first component is a proof that the set of geoengineering approaches has cardinality five and whose second component is the canonical certificate for the J-cost risk threshold.
background
Recognition Science evaluates geoengineering by the induced change in recognition ratio r equal to post-intervention flux over baseline flux. The J-cost of an intervention is J(r); the intervention is safe precisely when this cost remains inside the canonical band around J(φ). The module enumerates five canonical approaches (stratospheric aerosol injection, marine cloud brightening, ocean iron fertilisation, direct air capture, enhanced weathering) and treats their number as the configuration dimension D = 5.
proof idea
The definition is a direct record construction. It assigns the theorem that decides the cardinality of the finite type of approaches to the first field and assigns the imported canonical certificate to the risk-threshold field.
why it matters
The definition supplies the terminal certificate required for any Recognition Science assessment of climate-engineering risk. It closes the interface to the canonical J-band and thereby connects the five-approach count to the broader forcing chain (T5 J-uniqueness and the recognition composition law). No downstream theorems are listed, so the object functions as a self-contained interface definition rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.