ExoplanetHabitabilityCert
plain-language theorem explainer
The ExoplanetHabitabilityCert structure assembles five conditions certifying exoplanet habitability under RS resonance: positive resonant period, vanishing eccentricity penalty at zero, non-negative penalty for e greater than -1, unit habitability score at zero eccentricity, and unit dimensionless year. Researchers modeling exoplanet orbital stability would cite it when validating coherence against the phi-ladder. The declaration is a direct structure definition whose fields invoke the sibling period, penalty, and score functions.
Claim. The master certificate is the structure asserting $0 < T_{RS}$ with $T_{RS} := 1 · ϕ³/45$, the eccentricity penalty $J(1+e)$ satisfying $J(1+0)=0$ and $J(1+e) ≥ 0$ for $e > -1$, the habitability score equaling 1 at $e=0$, and the dimensionless year equaling 1.
background
The module defines the habitability score from three RS contributions: orbital resonance via the Earth-resonant period $T_{RS} = year · ϕ³/45$, the eccentricity penalty given by the J-cost $J(1+e)$, and a moon-mass stabilization band. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ from the forcing chain. The local setting is the initial closure of the exoplanet habitability row, with the score taking the form $1/(1 + J(1+e))$, matching the Rare Earth hypothesis for 1 AU systems with Moon-class satellites.
proof idea
The declaration is a structure definition collecting the five properties. It directly references the definitions of T_RS_period, eccentricity_penalty, and habitability_score, along with their established positivity and normalization results from sibling lemmas.
why it matters
This structure supplies the master certificate for the exoplanet habitability row in the Recognition Science framework. It is inhabited by the downstream exoplanetHabitabilityCert construction, which populates the fields using T_RS_period_pos, eccentricity_penalty_zero, and related results. The certificate encodes the ϕ³ resonant tick and J-cost penalty, supporting the Rare Earth hypothesis for 1 AU systems with Moon-class companions. It leaves open the incorporation of full multi-planet dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.