safeBand_contains_phi_point
plain-language theorem explainer
Verification that 0.118 lies strictly inside the safe-deployment band bounded by 0.11 and 0.13. Climate researchers applying Recognition Science to geoengineering strategies cite the result to confirm the canonical J(φ) point inhabits the permitted perturbation-ratio interval. The proof is a one-line wrapper that unfolds the two bound definitions and dispatches the inequalities by numerical normalization.
Claim. The lower bound of the safe-deployment band is less than 0.118 and 0.118 is less than the upper bound, i.e., $0.11 < 0.118 < 0.13$.
background
The module defines five canonical geoengineering approaches for configDim equal to 5: stratospheric aerosol injection, marine cloud brightening, ocean iron fertilisation, carbon dioxide removal, and cirrus cloud thinning. Each approach carries a risk profile on the recognition J-cost ladder, and the safe-deployment threshold is the canonical J(φ) band on the perturbation ratio, given explicitly as the open interval (0.11, 0.13).
proof idea
Unfolding safeBandLower and safeBandUpper exposes the constants 0.11 and 0.13. Refine splits the conjunction into two goals; norm_num then confirms both strict inequalities hold.
why it matters
The theorem supplies the band_inhabited field of geoengineeringCert, the structure that certifies the five approaches. It directly realizes the safe-deployment threshold as the J(φ) band stated in the module documentation. Within the Recognition framework the result confirms that the phi point at 0.118 lies inside the permitted interval on the perturbation ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.