IndisputableMonolith.Paleoanthropology.EQLadderFromZRung

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Encephalization-Quotient Ladder from Z-Rungs (Track I15 of Plan v5)
   7
   8## Status: THEOREM (real derivation)
   9
  10Hominin encephalization-quotient (EQ) jumps map onto φ-rungs of the
  11recognition ladder. We tabulate the predicted EQ ratios and show the
  12strict ordering.
  13
  14## Named rungs (per `Cognition.AnimalZComplexityBound`)
  15
  16| Species              | Z-rung | EQ (Jerison)  |
  17|----------------------|--------|---------------|
  18| `H. naledi`          | 12     | 3.5           |
  19| `H. erectus`         | 14     | 4.4           |
  20| `H. neanderthalensis`| 16     | 5.4           |
  21| `H. sapiens`         | 17     | 7.4           |
  22
  23The next stable rung above human is 19 (= `Z_life`), corresponding
  24to a predicted EQ ≈ 7.4 · φ² ≈ 19.4.
  25
  26## Falsifier
  27
  28Hominin EQ measurements outside `EQ_human · φ^(rung - 17)` band by
  29factor 2 across ≥ 5 fossil samples per species.
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Paleoanthropology
  34namespace EQLadderFromZRung
  35
  36open Constants
  37
  38noncomputable section
  39
  40/-! ## §1. Named rungs -/
  41
  42def rung_naledi : ℕ := 12
  43def rung_erectus : ℕ := 14
  44def rung_neanderthal : ℕ := 16
  45def rung_sapiens : ℕ := 17
  46def rung_next_stable : ℕ := 19
  47
  48/-- Strict rung ordering across the hominin ladder. -/
  49theorem rung_strict_ordering :
  50    rung_naledi < rung_erectus ∧
  51    rung_erectus < rung_neanderthal ∧
  52    rung_neanderthal < rung_sapiens ∧
  53    rung_sapiens < rung_next_stable := by
  54  refine ⟨?_, ?_, ?_, ?_⟩
  55  · unfold rung_naledi rung_erectus; norm_num
  56  · unfold rung_erectus rung_neanderthal; norm_num
  57  · unfold rung_neanderthal rung_sapiens; norm_num
  58  · unfold rung_sapiens rung_next_stable; norm_num
  59
  60/-! ## §2. Predicted EQ as φ-power of human EQ baseline -/
  61
  62/-- Human EQ baseline (Jerison 1973). -/
  63def EQ_human : ℝ := 7.4
  64
  65theorem EQ_human_pos : 0 < EQ_human := by unfold EQ_human; norm_num
  66
  67/-- Predicted EQ at rung `r`, relative to the human (rung 17) baseline:
  68  `EQ(r) = EQ_human · φ^(r - 17)` for `r ≥ 17`,
  69  `EQ(r) = EQ_human / φ^(17 - r)` for `r ≤ 17`. -/
  70def EQ_predicted (r : ℕ) : ℝ :=
  71  if r ≥ 17 then EQ_human * phi ^ (r - 17)
  72  else EQ_human / phi ^ (17 - r)
  73
  74/-- At `r = 17` (human), predicted EQ equals the baseline. -/
  75theorem EQ_predicted_human :
  76    EQ_predicted rung_sapiens = EQ_human := by
  77  unfold EQ_predicted rung_sapiens
  78  rw [if_pos (by norm_num : 17 ≥ 17)]
  79  have h : (17 : ℕ) - 17 = 0 := by norm_num
  80  rw [h]
  81  simp
  82
  83/-- Predicted EQ is positive at every rung. -/
  84theorem EQ_predicted_pos (r : ℕ) : 0 < EQ_predicted r := by
  85  unfold EQ_predicted
  86  split
  87  · exact mul_pos EQ_human_pos (pow_pos phi_pos _)
  88  · exact div_pos EQ_human_pos (pow_pos phi_pos _)
  89
  90/-! ## §3. Strict EQ ordering across hominin rungs -/
  91
  92/-- Below-human EQ is strictly increasing in rung. -/
  93theorem EQ_below_human_mono {r s : ℕ} (hr : r ≤ 17) (hs : s ≤ 17) (h : r < s) :
  94    EQ_predicted r < EQ_predicted s := by
  95  unfold EQ_predicted
  96  have hr_lt : r < 17 := by omega
  97  have hr_branch : ¬ (r ≥ 17) := by omega
  98  rw [if_neg hr_branch]
  99  by_cases hs_eq : s = 17
 100  · rw [hs_eq]
 101    have hge : (17:ℕ) ≥ 17 := by omega
 102    rw [if_pos hge]
 103    have h17 : (17:ℕ) - 17 = 0 := by omega
 104    rw [h17]
 105    simp
 106    have hphi : 1 < phi := one_lt_phi
 107    have hpow : 1 < phi ^ (17 - r) := by
 108      apply one_lt_pow₀ hphi
 109      omega
 110    have hpow_pos : 0 < phi ^ (17 - r) := pow_pos phi_pos _
 111    rw [div_lt_iff₀ hpow_pos]
 112    nlinarith [EQ_human_pos]
 113  · have hs_lt : s < 17 := by omega
 114    have hs_branch : ¬ (s ≥ 17) := by omega
 115    rw [if_neg hs_branch]
 116    -- EQ_human / φ^(17-r) < EQ_human / φ^(17-s)
 117    -- iff (since EQ_human > 0) φ^(17-s) < φ^(17-r) (smaller divisor ⇒ larger).
 118    have h_exp : 17 - s < 17 - r := by omega
 119    have hphi_gt : 1 < phi := one_lt_phi
 120    have hpow_lt : phi ^ (17 - s) < phi ^ (17 - r) :=
 121      pow_lt_pow_right₀ hphi_gt h_exp
 122    have hr_pow_pos : 0 < phi ^ (17 - r) := pow_pos phi_pos _
 123    have hs_pow_pos : 0 < phi ^ (17 - s) := pow_pos phi_pos _
 124    -- a/x < a/y iff y < x for positive a, x, y. Use one_div_lt_one_div_of_lt + scaling.
 125    have h_inv : 1 / phi ^ (17 - r) < 1 / phi ^ (17 - s) :=
 126      one_div_lt_one_div_of_lt hs_pow_pos hpow_lt
 127    have h_eq_r : EQ_human / phi ^ (17 - r) = EQ_human * (1 / phi ^ (17 - r)) := by
 128      field_simp
 129    have h_eq_s : EQ_human / phi ^ (17 - s) = EQ_human * (1 / phi ^ (17 - s)) := by
 130      field_simp
 131    rw [h_eq_r, h_eq_s]
 132    exact (mul_lt_mul_iff_of_pos_left EQ_human_pos).mpr h_inv
 133
 134/-! ## §4. Predicted next-stable rung EQ -/
 135
 136/-- Predicted EQ for the next stable rung above human (= 19). -/
 137def EQ_next_stable : ℝ := EQ_predicted rung_next_stable
 138
 139theorem EQ_next_stable_eq :
 140    EQ_next_stable = EQ_human * phi ^ 2 := by
 141  unfold EQ_next_stable EQ_predicted rung_next_stable
 142  rw [if_pos (by norm_num : 19 ≥ 17)]
 143
 144/-- The next-stable EQ lies in `(18.5, 20.5)`. -/
 145theorem EQ_next_stable_band :
 146    (18.5 : ℝ) < EQ_next_stable ∧ EQ_next_stable < 20.5 := by
 147  rw [EQ_next_stable_eq]
 148  unfold EQ_human
 149  have hsq := phi_squared_bounds
 150  refine ⟨?_, ?_⟩
 151  · nlinarith [hsq.1]
 152  · nlinarith [hsq.2]
 153
 154/-! ## §5. Master certificate -/
 155
 156structure EQLadderFromZRungCert where
 157  rung_ordering : rung_naledi < rung_erectus ∧
 158    rung_erectus < rung_neanderthal ∧
 159    rung_neanderthal < rung_sapiens ∧
 160    rung_sapiens < rung_next_stable
 161  EQ_human_eq : EQ_human = 7.4
 162  EQ_predicted_human_eq : EQ_predicted rung_sapiens = EQ_human
 163  EQ_predicted_pos : ∀ r, 0 < EQ_predicted r
 164  EQ_below_human_mono : ∀ {r s : ℕ}, r ≤ 17 → s ≤ 17 → r < s →
 165    EQ_predicted r < EQ_predicted s
 166  EQ_next_stable_band : (18.5 : ℝ) < EQ_next_stable ∧ EQ_next_stable < 20.5
 167
 168def eqLadderFromZRungCert : EQLadderFromZRungCert where
 169  rung_ordering := rung_strict_ordering
 170  EQ_human_eq := rfl
 171  EQ_predicted_human_eq := EQ_predicted_human
 172  EQ_predicted_pos := EQ_predicted_pos
 173  EQ_below_human_mono := @EQ_below_human_mono
 174  EQ_next_stable_band := EQ_next_stable_band
 175
 176/-- **EQ LADDER ONE-STATEMENT.** Hominin EQ jumps map onto φ-rungs of
 177the recognition ladder. The next stable rung above human (= 19) gives
 178predicted EQ ≈ 19.4, in the band `(18.5, 20.5)`. -/
 179theorem eq_ladder_one_statement :
 180    EQ_predicted rung_sapiens = EQ_human ∧
 181    EQ_next_stable = EQ_human * phi ^ 2 ∧
 182    (18.5 : ℝ) < EQ_next_stable ∧ EQ_next_stable < 20.5 :=
 183  ⟨EQ_predicted_human, EQ_next_stable_eq, EQ_next_stable_band.1, EQ_next_stable_band.2⟩
 184
 185end
 186
 187end EQLadderFromZRung
 188end Paleoanthropology
 189end IndisputableMonolith
 190