eccentricity_penalty_nonneg
plain-language theorem explainer
The theorem shows that the eccentricity penalty J(1 + e) stays non-negative whenever eccentricity e exceeds -1. Exoplanet modelers working in the Recognition Science framework cite it to keep the penalty term from subtracting from the overall habitability score. The proof is a direct term-mode reduction that unfolds the definition and invokes the J-cost non-negativity lemma after linear arithmetic confirms the argument is positive.
Claim. For every real number $e$ with $-1 < e$, one has $0 ≤ J(1 + e)$, where $J$ is the J-cost function.
background
The Exoplanet Habitability module constructs the RS habitability score from orbital resonance with period T_RS, the eccentricity penalty J(1 + e), and a moon-mass ratio check. The eccentricity penalty is defined as Jcost(1 + e) and vanishes at e = 0. Upstream results establish that J(x) ≥ 0 for x > 0 by the AM-GM inequality, as in the lemma whose doc-comment reads 'J(x) ≥ 0 for positive x (AM-GM inequality)'.
proof idea
The proof is a one-line term wrapper. It unfolds eccentricity_penalty to reach Jcost(1 + e), then applies Jcost_nonneg after linarith discharges the positivity hypothesis 0 < 1 + e implied by -1 < e.
why it matters
This theorem supplies the ecc_penalty_nonneg field inside the master certificate exoplanetHabitabilityCert. It thereby closes the positivity requirement for the eccentricity contribution to the composite habitability score in the §XXIII.C row. The result aligns with the J-uniqueness step (T5) of the forcing chain and ensures the additive structure of H(planet) remains non-negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.