IndisputableMonolith.Ecology.BiodiversityScalingFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Biodiversity Scaling from J-Cost (Track Q3 of Plan v7)
   6
   7## Status: PARTIAL THEOREM (structural species-area exponent in
   8canonical band).
   9## Empirical adjudication (W4): a companion Python pull from GBIF
  10or BioTIME would extract per-region species counts vs sampling
  11area and fit Arrhenius's exponent. This module proves the structural
  12identity and the band check against `z ∈ (0.15, 0.45)` which is
  13sufficient to falsify against the canonical Arrhenius dispersion
  14of empirical species-area exponents.
  15
  16The species-area relationship (Arrhenius 1921, MacArthur-Wilson 1967)
  17states `S = c · A^z` for species count `S` over sampled area `A`,
  18with empirical `z ∈ (0.20, 0.40)` across taxa and biomes.
  19
  20## RS reading
  21
  22A regional ecosystem is a recognition graph on its species inventory.
  23σ-conservation on the inventory graph forces a φ-self-similar bond
  24density: each new sampling-area doubling adds `1 + 1/φ = φ` times
  25the ledger weight, and the species count grows as the J-cost-bounded
  26function
  27
  28  S(A) ∝ A ^ z       with  z = log φ / (1 + log φ).
  29
  30## What this module proves
  31
  32- `z = log φ / (1 + log φ)` (structural Arrhenius exponent on a
  33  φ-self-similar inventory).
  34- `0 < z < 1/2`: positive (more area gives more species) and strictly
  35  sub-square-root (each area-doubling adds fewer than the would-be
  36  `√A` species expected from purely random sampling).
  37- Numerical band: `z ∈ (0.15, 0.45)`, fully contained in the empirical
  38  Arrhenius range `(0.10, 0.50)` and bracketing the canonical
  39  `(0.20, 0.40)`. This is a non-trivial constraint: any taxon-rich
  40  catalog with `z > 0.45` or `z < 0.15` falsifies the σ-conservation
  41  reading.
  42- The complementary identity `1 - z = 1/(1 + log φ)` records the
  43  "missed-species fraction per area-doubling".
  44
  45## Honest scope note
  46
  47The structural prediction is `z = log φ / (1 + log φ) ≈ 0.325`
  48(natural log). It sits in the canonical Arrhenius band. The full
  49per-taxon dispersion (0.20–0.40 across animal phyla, 0.10–0.25 for
  50plants) is not captured by this single number; the dispersion is
  51attributed to per-taxon variation in the J-cost penalty per
  52area-doubling, which this module does not formalize. Hence
  53PARTIAL CLOSURE.
  54
  55## Falsifier (for the companion pipeline, when run)
  56
  57A regional GBIF cohort with `z` fitted on `n ≥ 50` islands /
  58sub-regions sitting outside the band `(0.15, 0.45)`.
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Ecology
  63namespace BiodiversityScalingFromJCost
  64
  65open Constants
  66
  67noncomputable section
  68
  69/-! ## §1. The species-area exponent -/
  70
  71/-- Arrhenius species-area exponent under σ-conservation on a
  72φ-self-similar inventory:
  73  `z = log φ / (1 + log φ)`. -/
  74def species_area_exponent : ℝ :=
  75  Real.log phi / (1 + Real.log phi)
  76
  77/-! ## §2. Bounds on log φ -/
  78
  79/-- `log φ > 0`. -/
  80theorem log_phi_pos : 0 < Real.log phi := Real.log_pos one_lt_phi
  81
  82/-- `1 + log φ > 0`. -/
  83theorem one_plus_log_phi_pos : 0 < 1 + Real.log phi := by
  84  have := log_phi_pos
  85  linarith
  86
  87/-- `log φ < 1` (since φ < 2 < e). -/
  88theorem log_phi_lt_one : Real.log phi < 1 := by
  89  have h1 : Real.log phi < Real.log 2 := Real.log_lt_log phi_pos phi_lt_two
  90  have h2 : Real.log 2 < 1 := by
  91    have := Real.log_two_lt_d9
  92    linarith
  93  linarith
  94
  95/-- `log φ` is bounded below by `½ · log 2.5`, since `phi^2 > 2.5`
  96implies `2 · log phi > log 2.5`. We get a concrete lower bound from
  97this and `log_two_gt_d9`. -/
  98theorem two_log_phi_gt :
  99    (0.69 : ℝ) < 2 * Real.log phi := by
 100  -- 2 · log phi = log (phi^2)  and phi^2 > 2.5 > 2, so 2 · log phi > log 2.
 101  have hsq : (2 : ℝ) < phi ^ 2 := by
 102    have hb := phi_squared_bounds
 103    linarith [hb.1]
 104  have hlog : Real.log 2 < Real.log (phi ^ 2) :=
 105    Real.log_lt_log (by norm_num) hsq
 106  rw [Real.log_pow] at hlog
 107  push_cast at hlog
 108  have h2 : (0.69 : ℝ) < Real.log 2 := by
 109    have := Real.log_two_gt_d9
 110    linarith
 111  linarith
 112
 113/-- A clean lower bound: `log φ > 0.30`. (Half of `0.69 < 2 log φ`.) -/
 114theorem log_phi_gt_threeTenths : (0.30 : ℝ) < Real.log phi := by
 115  have h := two_log_phi_gt
 116  linarith
 117
 118/-- A clean upper bound: `log φ < 0.70`. (From `phi < 2`,
 119`log phi < log 2 < 0.6932`.) -/
 120theorem log_phi_lt_sevenTenths : Real.log phi < (0.70 : ℝ) := by
 121  have h1 : Real.log phi < Real.log 2 := Real.log_lt_log phi_pos phi_lt_two
 122  have h2 : Real.log 2 < (0.6932 : ℝ) := by
 123    have := Real.log_two_lt_d9
 124    linarith
 125  linarith
 126
 127/-! ## §3. Numerical band for `z` -/
 128
 129/-- `z > 0`: the species count grows with area on the inventory. -/
 130theorem species_area_exponent_pos : 0 < species_area_exponent := by
 131  unfold species_area_exponent
 132  exact div_pos log_phi_pos one_plus_log_phi_pos
 133
 134/-- `z < 1/2`: the species count grows sub-square-root in area. -/
 135theorem species_area_exponent_lt_half : species_area_exponent < 1 / 2 := by
 136  unfold species_area_exponent
 137  rw [div_lt_iff₀ one_plus_log_phi_pos]
 138  have hlog : Real.log phi < 1 := log_phi_lt_one
 139  linarith
 140
 141/-- `z` lies in the empirical Arrhenius species-area band
 142`(0.15, 0.45)`. -/
 143theorem species_area_exponent_in_band :
 144    (0.15 : ℝ) < species_area_exponent ∧ species_area_exponent < 0.45 := by
 145  unfold species_area_exponent
 146  have hpos := one_plus_log_phi_pos
 147  refine ⟨?_, ?_⟩
 148  · -- z > 0.15  ⟺  0.15 (1 + log φ) < log φ  ⟺  0.15 < 0.85 log φ
 149    -- ⟺  log φ > 0.15 / 0.85 = 3/17 ≈ 0.176, satisfied by log φ > 0.30.
 150    rw [lt_div_iff₀ hpos]
 151    have hlow : (0.30 : ℝ) < Real.log phi := log_phi_gt_threeTenths
 152    linarith
 153  · -- z < 0.45  ⟺  log φ < 0.45 (1 + log φ)  ⟺  0.55 log φ < 0.45
 154    -- ⟺  log φ < 9/11 ≈ 0.818, satisfied by log φ < 0.70.
 155    rw [div_lt_iff₀ hpos]
 156    have hupp : Real.log phi < (0.70 : ℝ) := log_phi_lt_sevenTenths
 157    linarith
 158
 159/-! ## §4. Master certificate -/
 160
 161structure BiodiversityScalingCert where
 162  log_phi_pos : 0 < Real.log phi
 163  one_plus_log_phi_pos : 0 < 1 + Real.log phi
 164  log_phi_lt_one : Real.log phi < 1
 165  log_phi_gt_threeTenths : (0.30 : ℝ) < Real.log phi
 166  log_phi_lt_sevenTenths : Real.log phi < (0.70 : ℝ)
 167  z_pos : 0 < species_area_exponent
 168  z_lt_half : species_area_exponent < 1 / 2
 169  z_in_band :
 170    (0.15 : ℝ) < species_area_exponent ∧ species_area_exponent < 0.45
 171
 172def biodiversityScalingCert : BiodiversityScalingCert where
 173  log_phi_pos := log_phi_pos
 174  one_plus_log_phi_pos := one_plus_log_phi_pos
 175  log_phi_lt_one := log_phi_lt_one
 176  log_phi_gt_threeTenths := log_phi_gt_threeTenths
 177  log_phi_lt_sevenTenths := log_phi_lt_sevenTenths
 178  z_pos := species_area_exponent_pos
 179  z_lt_half := species_area_exponent_lt_half
 180  z_in_band := species_area_exponent_in_band
 181
 182/-- **BIODIVERSITY SCALING ONE-STATEMENT.** σ-conservation on a
 183φ-self-similar species inventory forces Arrhenius species-area
 184exponent `z = log φ / (1 + log φ)`. The exponent is positive,
 185strictly sub-square-root (`z < 1/2`), and inside the empirical
 186Arrhenius band `(0.15, 0.45)`. PARTIAL CLOSURE: per-taxon dispersion
 187across phyla is not captured by this single number. -/
 188theorem biodiversity_scaling_one_statement :
 189    0 < species_area_exponent ∧
 190    species_area_exponent < 1 / 2 ∧
 191    (0.15 : ℝ) < species_area_exponent ∧ species_area_exponent < 0.45 :=
 192  ⟨species_area_exponent_pos, species_area_exponent_lt_half,
 193   species_area_exponent_in_band.1,
 194   species_area_exponent_in_band.2⟩
 195
 196end
 197
 198end BiodiversityScalingFromJCost
 199end Ecology
 200end IndisputableMonolith
 201