Astrophysics Exoplanet Habitability Eccentricity Penalty

The eccentricity penalty

In astronomy, eccentricity measures how much an orbit deviates from a perfect circle. A value of zero means a circular orbit; values closer to one mean a more elongated ellipse. The Recognition Science framework's cost function, a measure of the price of a recognition event, provides a way to translate this orbital shape into a penalty on a planet's habitability score.

The declaration eccentricity_penalty defines this penalty as the cost function evaluated at 1 + e, where e is the eccentricity. The framework proves that this penalty is exactly zero when the orbit is perfectly circular (e = 0). It also proves the penalty is never negative for any physically possible orbit, where the eccentricity is greater than negative one. This means a circular orbit incurs no penalty, and any deviation from a circle can only reduce the habitability score, never improve it.

The habitability score itself is defined as 1 / (1 + eccentricity_penalty). This formula ensures the score is exactly 1 for a circular orbit, the maximum possible value, and decreases as the penalty grows. The framework's library proves these properties as formal theorems, establishing a clean mathematical relationship between orbital shape and its model of habitability.

This penalty is one of three contributions to the framework's overall habitability score, alongside a resonance term tied to a specific period and a bonus for companion moons of a certain mass. The framework explicitly does not claim that Earth's own Moon falls within its predicted optimal mass band; it only exposes the predicate for that band as a definition.

/-- The eccentricity penalty: `J(1 + e)`.  Zero at `e = 0`. -/
def eccentricity_penalty (e : ℝ) : ℝ := Jcost (1 + e)

/-- At zero eccentricity, penalty vanishes. -/
theorem eccentricity_penalty_zero :
    eccentricity_penalty 0 = 0 := by
  unfold eccentricity_penalty
  simp [Jcost_unit0]

/-- The eccentricity penalty is non-negative (as long as `1 + e > 0`). -/
theorem eccentricity_penalty_nonneg (e : ℝ) (h : -1 < e) :
    0 ≤ eccentricity_penalty e := by
  unfold eccentricity_penalty
  exact Jcost_nonneg (by linarith)

/-- Habitability score (additive form).  Higher is better.  Built
    from `1 / (1 + eccentricity_penalty)` and `T_RS resonance`. -/
def habitability_score (e : ℝ) : ℝ :=
  1 / (1 + eccentricity_penalty e)

What this page does not claim

This penalty is a proven law of physics; it is a definitional choice within the framework. The framework claims Earth's Moon is inside its predicted optimal mass band; it explicitly does not. A circular orbit is proven to be the most habitable in reality; the framework only shows its score is maximized at zero eccentricity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/ExoplanetHabitability.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: