exoplanetHabitabilityCert
plain-language theorem explainer
The declaration constructs an explicit inhabitant of the ExoplanetHabitabilityCert structure by supplying the required positivity and non-negativity properties. Astrophysicists working within the Recognition Science framework would cite this to confirm that the habitability score is well-defined and attains its maximum at zero eccentricity. The construction is a direct record that assembles five sibling lemmas for the individual certificate fields.
Claim. There exists a certificate asserting that the resonant period satisfies $0 < T_{RS}$, the eccentricity penalty $J(1+e)$ vanishes at $e=0$ and remains non-negative for $e>-1$, the composite habitability score equals 1 at zero eccentricity, and the dimensionless year equals 1.
background
In the Recognition Science treatment of exoplanet habitability the score combines orbital resonance with the RS period $T_{RS} =$ year $· φ^3 / 45$, the eccentricity penalty given by the J-cost $J(1+e)$, and a moon-mass stabilization term when the companion ratio lies in $[φ^{-7}, φ^{-6}]$. The module defines the composite habitability_score as an additive form that reaches its maximum of 1 when eccentricity vanishes. The upstream result T_RS_period_pos establishes positivity of the resonant period via the positivity of phi and its powers.
proof idea
The definition is a direct structure constructor that populates each field of ExoplanetHabitabilityCert by referencing the corresponding sibling theorem: T_RS_period_pos supplies the positivity assertion, eccentricity_penalty_zero supplies the vanishing at e=0, eccentricity_penalty_nonneg supplies the non-negativity bound, habitability_score_at_zero_ecc supplies the unit score, and rfl discharges the year equality.
why it matters
This definition closes the initial habitability model in the Astrophysics module by exhibiting an explicit certificate. It completes the §XXIII.C row on exoplanet habitability and supplies the five-field master certificate that downstream applications can invoke to guarantee the score properties. The construction relies on the J-cost non-negativity from the Cost module and the phi-based resonance period, aligning with the self-similar fixed point of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.