habitability_score
plain-language theorem explainer
The habitability score is a real-valued function of eccentricity that equals one at zero eccentricity and decreases as eccentricity grows. Astrophysicists applying Recognition Science to exoplanet classification would cite this definition inside the master habitability certificate. It is introduced by a direct one-line definition that composes the reciprocal of one plus the eccentricity penalty.
Claim. The habitability score for eccentricity $e$ is $H(e) = 1 / (1 + J(1 + e))$, where $J$ is the J-cost function.
background
The ExoplanetHabitability module builds a composite score for an exoplanet from orbital resonance with the RS period $T_{RS} = $ year$·φ^3/45$, the eccentricity penalty $J(1+e)$ that vanishes at $e=0$, and a moon-mass-ratio bonus when the ratio lies in $[φ^{-7}, φ^{-6}]$. This definition isolates the eccentricity factor as the reciprocal of one plus that penalty. It depends on the upstream eccentricity_penalty definition, which applies the J-cost function, and on the general cost-model score.
proof idea
The declaration is a direct definition that returns the reciprocal of one plus the eccentricity penalty. No lemmas or tactics are required beyond the definition itself.
why it matters
This definition supplies the eccentricity component required by the ExoplanetHabitabilityCert structure, which records that the score equals 1 at zero eccentricity. It completes the §XXIII.C exoplanet-habitability row by linking the J-cost penalty to the $T_{RS}$ resonance and the phi-ladder. The certificate aggregates this term with resonance positivity and moon-stabilization bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.