pith. sign in
module module high

IndisputableMonolith.Climate.GeoengineeringRiskFromJCost

show as:
view Lean formalization →

This module applies the Canonical J-Cost Band template to climate geoengineering risks. It defines GeoengineeringApproach types and constructs GeoengineeringRiskCert using the six-clause J-cost conditions on risk ratios. Researchers working on Recognition Science domain certificates would cite it for the climate instantiation. The module supplies definitions and a certificate without new proofs.

claimThe module defines an inductive type of geoengineering methods and a certificate structure ensuring $J(1)=0$ together with $J(r)≥0$ for risk ratios $r>0$, where $J(x)=(x+x^{-1})/2-1$.

background

The module sits in the climate domain and reuses the six-clause J-cost template imported from CanonicalJBand. That template requires matched-zero at unity and nonnegativity for positive arguments, with the J function given by the standard hyperbolic form. Sibling definitions introduce GeoengineeringApproach, approachCount, and the risk certificate that packages the template clauses for geoengineering ratios.

proof idea

This is a definition module, no proofs. It imports the CanonicalJBand template and builds the domain-specific GeoengineeringRiskCert by direct application of the six clauses to risk ratios.

why it matters in Recognition Science

The module supplies one of the Plan v7 domain certificates in the master cert chain. It feeds the B-tier whole-science openings by instantiating the J-cost template for climate geoengineering risks, completing the required nonnegativity and zero-at-unity conditions for that domain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)