eccentricity_penalty
plain-language theorem explainer
Eccentricity penalty maps orbital eccentricity e to Jcost(1 + e) and vanishes at e = 0. Researchers building Recognition Science models of exoplanet habitability cite it when assembling the composite score from resonance period, eccentricity penalty, and moon-mass ratio. The declaration is a one-line definition that applies the J-cost function directly to the shifted argument 1 + e.
Claim. The eccentricity penalty is the function sending orbital eccentricity $e$ to $J(1 + e)$, where $J$ is the J-cost function of Recognition Science (satisfying $J(1) = 0$).
background
The Exoplanet Habitability module constructs an RS habitability score from the orbital resonance period $T_{RS} =$ year · φ³ / 45, the eccentricity penalty, and the predicate that companion-moon mass ratio lies in [φ^{-7}, φ^{-6}]. The eccentricity term enters as J(1 + e) and is required to vanish at e = 0 so that the score reaches its maximum of 1. This implements the initial closure of the §XXIII.C habitability row and is collected into the master certificate ExoplanetHabitabilityCert together with positivity of $T_{RS}$ and non-negativity of the penalty.
proof idea
The declaration is a one-line definition that sets eccentricity_penalty e to Jcost(1 + e). No lemmas are invoked inside the definition; the zero-value and non-negativity properties are established in separate theorems by unfolding and applying Jcost_unit0 and Jcost_nonneg.
why it matters
This definition supplies the eccentricity contribution to the habitability score and is required by the master certificate ExoplanetHabitabilityCert. It realizes the eccentricity term in the Recognition Science habitability row and rests on J-uniqueness (T5) from the forcing chain. The construction predicts that circular orbits maximize habitability, consistent with the phi-ladder and self-similar fixed points. An open aspect noted in the module is whether the Earth-Moon mass ratio falls inside the predicted band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.