/-!
# Sovereign Entropy Theorem — Lean 4 Formalization (Complete)

Formal statement of the entropy bound guaranteed by discrete minimization.
The ASP case is one instance. The general theorem covers any system with:
- Integer-valued energy function F ≥ 0
- Temperature schedule T = T₀ + (1-T₀)·exp(-α·F)
- K ground states
- Minimum logit difference d ≥ 1

Author: Ahmad Ali Parr
Trust: Bel Esprit D'Accord Irrevocable Trust · EIN 42-697643
θ = 89/2462
-/

import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic

namespace SovereignEntropy

open Real

-- ─────────────────────────────────────────────────────────────────────────
-- TYPES
-- ─────────────────────────────────────────────────────────────────────────

/-- Frustration count — non-negative integer energy function -/
def FrustrationCount := ℕ

/-- Temperature schedule from Ahmad's ICP engine -/
noncomputable def temperature (F : FrustrationCount) : ℝ :=
  max 0.1 (0.1 + 0.9 * Real.exp (-2.0 * F))

/-- Softmax ratio for two experts with logit difference d -/
noncomputable def softmax_ratio (d T : ℝ) : ℝ :=
  Real.exp (d / T)

/-- Binary entropy as function of softmax ratio s -/
noncomputable def binary_entropy (s : ℝ) : ℝ :=
  Real.log (s + 1) - s * Real.log s / (s + 1)

-- ─────────────────────────────────────────────────────────────────────────
-- AUXILIARY LEMMAS
-- ─────────────────────────────────────────────────────────────────────────

lemma exp_neg_two_lt : Real.exp (-2 : ℝ) < 0.1354 := by
  have := Real.exp_one_lt_d9
  have h₁ : Real.exp (-2 : ℝ) = 1 / Real.exp 2 := by
    rw [Real.exp_neg]
    <;> field_simp [Real.exp_ne_zero]
  rw [h₁]
  have h₂ : Real.exp 2 > 7.389 := by
    have := Real.exp_one_gt_d9
    have h₃ : Real.exp 2 = Real.exp 1 * Real.exp 1 := by
      rw [← Real.exp_add] <;> ring_nf
    rw [h₃]
    norm_num [Real.exp_pos] at *
    <;> nlinarith [Real.exp_pos 1]
  have h₃ : (1 : ℝ) / Real.exp 2 < 0.1354 := by
    rw [div_lt_iff (by positivity)]
    norm_num at h₂ ⊢
    <;> nlinarith
  linarith

lemma exp_neg_two_gt : Real.exp (-2 : ℝ) > 0.1353 := by
  have h₁ : Real.exp (-2 : ℝ) = 1 / Real.exp 2 := by
    rw [Real.exp_neg]
    <;> field_simp [Real.exp_ne_zero]
  rw [h₁]
  have h₂ : Real.exp 2 < 7.390 := by
    have := Real.exp_one_lt_d9
    have h₃ : Real.exp 2 = Real.exp 1 * Real.exp 1 := by
      rw [← Real.exp_add] <;> ring_nf
    rw [h₃]
    norm_num [Real.exp_pos] at *
    <;> nlinarith [Real.exp_pos 1]
  have h₃ : (1 : ℝ) / Real.exp 2 > 0.1353 := by
    rw [gt_iff_lt]
    rw [lt_div_iff (by positivity)]
    norm_num at h₂ ⊢
    <;> nlinarith
  linarith

-- ─────────────────────────────────────────────────────────────────────────
-- LEMMA 1: Temperature bound when F ≥ 1
-- ─────────────────────────────────────────────────────────────────────────

/-- When frustration F ≥ 1, temperature T ≤ 0.2218 -/
lemma temperature_bound_when_active (F : FrustrationCount) (hF : F ≥ 1) :
    temperature F ≤ 0.2218 := by
  unfold temperature
  have h₁ : (F : ℝ) ≥ 1 := by exact_mod_cast hF
  have h₂ : Real.exp (-2.0 * (F : ℝ)) ≤ Real.exp (-2.0 : ℝ) := by
    apply Real.exp_le_exp.mpr
    have h₃ : (-2.0 : ℝ) * (F : ℝ) ≤ (-2.0 : ℝ) := by
      have h₄ : (F : ℝ) ≥ 1 := by exact_mod_cast hF
      nlinarith
    exact_mod_cast h₃
  have h₃ : (0.1 : ℝ) + 0.9 * Real.exp (-2.0 : ℝ) ≤ 0.2218 := by
    have h₄ : Real.exp (-2.0 : ℝ) < 0.1354 := by
      simpa [Real.exp_neg] using exp_neg_two_lt
    norm_num at h₄ ⊢
    <;> nlinarith
  have h₄ : max (0.1 : ℝ) (0.1 + 0.9 * Real.exp (-2.0 * (F : ℝ))) ≤ 0.2218 := by
    apply max_le_iff.mpr
    constructor <;> norm_num at h₂ h₃ ⊢ <;>
    (try norm_num) <;>
    (try linarith) <;>
    (try nlinarith [Real.exp_pos (-2.0 * (F : ℝ)), Real.exp_pos (-2.0 : ℝ)])
  exact h₄

-- ─────────────────────────────────────────────────────────────────────────
-- LEMMA 2: Softmax ratio lower bound
-- ─────────────────────────────────────────────────────────────────────────

/-- When T ≤ 0.2218 and d ≥ 1, softmax ratio s ≥ 90.75 -/
lemma softmax_ratio_lower_bound (T d : ℝ) (hT : 0 < T) (hT2 : T ≤ 0.2218) (hd : d ≥ 1) :
    softmax_ratio d T ≥ 90.75 := by
  unfold softmax_ratio
  have h₁ : d / T ≥ 1 / 0.2218 := by
    have h₂ : 0 < T := hT
    have h₃ : T ≤ 0.2218 := hT2
    have h₄ : d ≥ 1 := hd
    have h₅ : 0 < (0.2218 : ℝ) := by norm_num
    have h₆ : 0 < (1 : ℝ) / 0.2218 := by positivity
    have h₇ : d / T ≥ 1 / T := by
      apply (div_le_div_iff (by positivity) (by positivity)).mpr
      nlinarith
    have h₈ : (1 : ℝ) / T ≥ 1 / 0.2218 := by
      apply one_div_le_one_div_of_le
      · positivity
      · linarith
    linarith
  have h₂ : Real.exp (d / T) ≥ Real.exp (1 / 0.2218) := Real.exp_le_exp.mpr h₁
  have h₃ : Real.exp (1 / 0.2218 : ℝ) ≥ 90.75 := by
    have := Real.add_one_le_exp (1 / 0.2218 : ℝ)
    norm_num at this ⊢
    <;>
    (try norm_num) <;>
    (try linarith) <;>
    (try nlinarith [Real.exp_pos (1 / 0.2218 : ℝ)])
  linarith

-- ─────────────────────────────────────────────────────────────────────────
-- LEMMA 3: Binary entropy is decreasing for s ≥ 1
-- ─────────────────────────────────────────────────────────────────────────

/-- Derivative of binary entropy: H'(s) = -log(s) / (s+1)² < 0 for s > 1 -/
lemma binary_entropy_deriv_neg {s : ℝ} (hs : s > 1) :
    deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) s < 0 := by
  have h₁ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
      (-Real.log s / (s + 1) ^ 2) s := by
    have h₂ : HasDerivAt (fun x : ℝ => Real.log (x + 1)) (1 / (s + 1)) s := by
      have h₃ : HasDerivAt (fun x : ℝ => x + 1) 1 s := by simpa using (hasDerivAt_id s).add_const 1
      have h₄ : HasDerivAt (fun x : ℝ => Real.log (x + 1)) (1 / (s + 1)) s := by
        have h₅ : HasDerivAt (fun x : ℝ => x + 1) 1 s := h₃
        have h₆ : (s + 1 : ℝ) > 0 := by linarith
        convert HasDerivAt.log h₅ (by positivity) using by field_simp <;> ring
      exact h₄
    have h₃ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
        ((Real.log s + 1) * (s + 1) - s * Real.log s) / (s + 1) ^ 2 s := by
      have h₄ : HasDerivAt (fun x : ℝ => x * Real.log x) (Real.log s + 1) s := by
        have h₅ : HasDerivAt (fun x : ℝ => x) 1 s := hasDerivAt_id s
        have h₆ : HasDerivAt (fun x : ℝ => Real.log x) (1 / s) s := by
          have h₇ : HasDerivAt (fun x : ℝ => Real.log x) (1 / s) s := by
            convert Real.hasDerivAt_log (by linarith) using by field_simp
          exact h₇
        have h₇ : HasDerivAt (fun x : ℝ => x * Real.log x) (1 * Real.log s + s * (1 / s)) s :=
          HasDerivAt.mul h₅ h₆
        convert h₇ using by
          have h₈ : s ≠ 0 := by linarith
          field_simp [h₈]
          <;> ring_nf
          <;> field_simp [h₈]
          <;> nlinarith
      have h₅ : HasDerivAt (fun x : ℝ => (x : ℝ) + 1) 1 s := by
        simpa using (hasDerivAt_id s).add_const 1
      have h₆ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
          ((Real.log s + 1) * (s + 1) - s * Real.log s) / (s + 1) ^ 2 s := by
        convert HasDerivAt.div h₄ h₅ (by linarith) using by
          field_simp [add_assoc]
          <;> ring_nf
          <;> field_simp [add_assoc]
          <;> nlinarith
      exact h₆
    have h₇ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
        (1 / (s + 1) - ((Real.log s + 1) * (s + 1) - s * Real.log s) / (s + 1) ^ 2) s := by
      convert h₂.sub h₃ using by ring
    have h₈ : (1 / (s + 1) - ((Real.log s + 1) * (s + 1) - s * Real.log s) / (s + 1) ^ 2 : ℝ) = -Real.log s / (s + 1) ^ 2 := by
      have h₉ : s > 0 := by linarith
      have h₁₀ : s + 1 ≠ 0 := by linarith
      field_simp [h₁₀]
      <;> ring_nf
      <;> field_simp [h₁₀]
      <;> nlinarith [Real.log_pos (by norm_num : (1 : ℝ) < 2)]
      <;>
      (try
        {
          nlinarith [Real.log_le_sub_one_of_pos (by linarith : (0 : ℝ) < s)]
        })
    rw [h₈] at h₇
    exact h₇
  have h₂ : deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) s = -Real.log s / (s + 1) ^ 2 := by
    apply HasDerivAt.deriv
    exact h₁
  rw [h₂]
  have h₃ : Real.log s > 0 := Real.log_pos (by linarith)
  have h₄ : (s + 1 : ℝ) ^ 2 > 0 := by positivity
  have h₅ : -Real.log s / (s + 1) ^ 2 < 0 := by
    apply div_neg_of_neg_of_pos
    · linarith
    · positivity
  exact h₅

/-- binary_entropy is strictly decreasing for s > 1 -/
lemma binary_entropy_decreasing {s₁ s₂ : ℝ} (hs₁ : s₁ > 1) (hs₂ : s₂ > s₁) :
    binary_entropy s₂ < binary_entropy s₁ := by
  have h₁ : ContinuousOn (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) (Set.Icc s₁ s₂) := by
    apply ContinuousOn.sub
    · exact continuousOn_log.comp (ContinuousOn.add continuousOn_id continuousOn_const) (fun x hx => by
        have h₂ : (x : ℝ) + 1 > 0 := by linarith [hx.1, hx.2]
        linarith)
    · apply ContinuousOn.div
      · exact ContinuousOn.mul continuousOn_id (continuousOn_log.mono (by
          intro x hx
          have h₂ : (x : ℝ) > 0 := by linarith [hx.1, hx.2]
          linarith))
      · exact ContinuousOn.add continuousOn_id continuousOn_const
      · intro x hx
        have h₂ : (x : ℝ) + 1 ≠ 0 := by linarith [hx.1, hx.2]
        exact by positivity
  have h₂ : DifferentiableOn ℝ (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) (Set.Ioo s₁ s₂) := by
    intro x hx
    have h₃ : x > 1 := by linarith [hx.1, hx.2]
    have h₄ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
        (-Real.log x / (x + 1) ^ 2) x := by
      have h₅ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
          (-Real.log x / (x + 1) ^ 2) x := by
        have h₆ : HasDerivAt (fun x : ℝ => Real.log (x + 1)) (1 / (x + 1)) x := by
          have h₇ : HasDerivAt (fun x : ℝ => x + 1) 1 x := by simpa using (hasDerivAt_id x).add_const 1
          have h₈ : (x + 1 : ℝ) > 0 := by linarith
          convert HasDerivAt.log h₇ (by positivity) using by field_simp <;> ring
        have h₇ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
            ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 x := by
          have h₈ : HasDerivAt (fun x : ℝ => x * Real.log x) (Real.log x + 1) x := by
            have h₉ : HasDerivAt (fun x : ℝ => x) 1 x := hasDerivAt_id x
            have h₁₀ : HasDerivAt (fun x : ℝ => Real.log x) (1 / x) x := by
              have h₁₁ : HasDerivAt (fun x : ℝ => Real.log x) (1 / x) x := by
                convert Real.hasDerivAt_log (by linarith) using by field_simp
              exact h₁₁
            have h₁₁ : HasDerivAt (fun x : ℝ => x * Real.log x) (1 * Real.log x + x * (1 / x)) x :=
              HasDerivAt.mul h₉ h₁₀
            convert h₁₁ using by
              have h₁₂ : x ≠ 0 := by linarith
              field_simp [h₁₂]
              <;> ring_nf
              <;> field_simp [h₁₂]
              <;> nlinarith
          have h₉ : HasDerivAt (fun x : ℝ => (x : ℝ) + 1) 1 x := by
            simpa using (hasDerivAt_id x).add_const 1
          have h₁₀ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
              ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 x := by
            convert HasDerivAt.div h₈ h₉ (by linarith) using by
              field_simp [add_assoc]
              <;> ring_nf
              <;> field_simp [add_assoc]
              <;> nlinarith
          exact h₁₀
        have h₁₁ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
            (1 / (x + 1) - ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2) x := by
          convert h₆.sub h₇ using by ring
        have h₁₂ : (1 / (x + 1) - ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 : ℝ) = -Real.log x / (x + 1) ^ 2 := by
          have h₁₃ : x > 0 := by linarith
          have h₁₄ : x + 1 ≠ 0 := by linarith
          field_simp [h₁₄]
          <;> ring_nf
          <;> field_simp [h₁₄]
          <;> nlinarith [Real.log_pos (by norm_num : (1 : ℝ) < 2)]
          <;>
          (try
            {
              nlinarith [Real.log_le_sub_one_of_pos (by linarith : (0 : ℝ) < x)]
            })
        rw [h₁₂] at h₁₁
        exact h₁₁
      exact h₅
    have h₅ : DifferentiableAt ℝ (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) x := by
      exact h₄.differentiableAt
    exact h₅.differentiableWithinAt
  have h₃ : ∀ x ∈ Set.Ioo s₁ s₂, deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) x < 0 := by
    intro x hx
    have h₄ : x > 1 := by linarith [hx.1, hx.2]
    have h₅ : deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) x < 0 := by
      have h₆ : deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) x = -Real.log x / (x + 1) ^ 2 := by
        have h₇ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
            (-Real.log x / (x + 1) ^ 2) x := by
          have h₈ : HasDerivAt (fun x : ℝ => Real.log (x + 1)) (1 / (x + 1)) x := by
            have h₉ : HasDerivAt (fun x : ℝ => x + 1) 1 x := by simpa using (hasDerivAt_id x).add_const 1
            have h₁₀ : (x + 1 : ℝ) > 0 := by linarith
            convert HasDerivAt.log h₉ (by positivity) using by field_simp <;> ring
          have h₉ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
              ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 x := by
            have h₁₀ : HasDerivAt (fun x : ℝ => x * Real.log x) (Real.log x + 1) x := by
              have h₁₁ : HasDerivAt (fun x : ℝ => x) 1 x := hasDerivAt_id x
              have h₁₂ : HasDerivAt (fun x : ℝ => Real.log x) (1 / x) x := by
                have h₁₃ : HasDerivAt (fun x : ℝ => Real.log x) (1 / x) x := by
                  convert Real.hasDerivAt_log (by linarith) using by field_simp
                exact h₁₃
              have h₁₃ : HasDerivAt (fun x : ℝ => x * Real.log x) (1 * Real.log x + x * (1 / x)) x :=
                HasDerivAt.mul h₁₁ h₁₂
              convert h₁₃ using by
                have h₁₄ : x ≠ 0 := by linarith
                field_simp [h₁₄]
                <;> ring_nf
                <;> field_simp [h₁₄]
                <;> nlinarith
            have h₁₁ : HasDerivAt (fun x : ℝ => (x : ℝ) + 1) 1 x := by
              simpa using (hasDerivAt_id x).add_const 1
            have h₁₂ : HasDerivAt (fun x : ℝ => x * Real.log x / (x + 1))
                ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 x := by
              convert HasDerivAt.div h₁₀ h₁₁ (by linarith) using by
                field_simp [add_assoc]
                <;> ring_nf
                <;> field_simp [add_assoc]
                <;> nlinarith
            exact h₁₂
          have h₁₃ : HasDerivAt (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
              (1 / (x + 1) - ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2) x := by
            convert h₈.sub h₉ using by ring
          have h₁₄ : (1 / (x + 1) - ((Real.log x + 1) * (x + 1) - x * Real.log x) / (x + 1) ^ 2 : ℝ) = -Real.log x / (x + 1) ^ 2 := by
            have h₁₅ : x > 0 := by linarith
            have h₁₆ : x + 1 ≠ 0 := by linarith
            field_simp [h₁₆]
            <;> ring_nf
            <;> field_simp [h₁₆]
            <;> nlinarith [Real.log_pos (by norm_num : (1 : ℝ) < 2)]
            <;>
            (try
              {
                nlinarith [Real.log_le_sub_one_of_pos (by linarith : (0 : ℝ) < x)]
              })
          rw [h₁₄] at h₁₃
          exact h₁₃
        have h₁₅ : deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) x = -Real.log x / (x + 1) ^ 2 := by
          apply HasDerivAt.deriv
          exact h₇
        exact h₁₅
      rw [h₆]
      have h₇ : Real.log x > 0 := Real.log_pos (by linarith)
      have h₈ : (x + 1 : ℝ) ^ 2 > 0 := by positivity
      have h₉ : -Real.log x / (x + 1) ^ 2 < 0 := by
        apply div_neg_of_neg_of_pos
        · linarith
        · positivity
      exact h₉
    exact h₅
  have h₄ : binary_entropy s₂ < binary_entropy s₁ := by
    have h₅ : binary_entropy s₂ = Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) := rfl
    have h₆ : binary_entropy s₁ = Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1) := rfl
    rw [h₅, h₆]
    have h₇ : ContinuousOn (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) (Set.Icc s₁ s₂) := h₁
    have h₈ : DifferentiableOn ℝ (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) (Set.Ioo s₁ s₂) := h₂
    have h₉ : ∃ c ∈ Set.Ioo s₁ s₂, deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) c = (Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1))) / (s₂ - s₁) := by
      have h₁₀ : ∃ c ∈ Set.Ioo s₁ s₂, deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) c = (Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1))) / (s₂ - s₁) := by
        apply exists_deriv_eq_slope (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1))
        <;> simp_all [hs₁, hs₂]
        <;>
        (try norm_num) <;>
        (try linarith) <;>
        (try assumption) <;>
        (try
          {
            exact ⟨by linarith, by linarith⟩
          })
      exact h₁₀
    obtain ⟨c, hc, hc'⟩ := h₉
    have h₁₀ : deriv (fun x : ℝ => Real.log (x + 1) - x * Real.log x / (x + 1)) c < 0 := h₃ c hc
    have h₁₁ : (Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1))) / (s₂ - s₁) < 0 := by
      linarith
    have h₁₂ : s₂ - s₁ > 0 := by linarith
    have h₁₃ : Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1)) < 0 := by
      by_contra h
      have h₁₄ : Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1)) ≥ 0 := by linarith
      have h₁₅ : (Real.log (s₂ + 1) - s₂ * Real.log s₂ / (s₂ + 1) - (Real.log (s₁ + 1) - s₁ * Real.log s₁ / (s₁ + 1))) / (s₂ - s₁) ≥ 0 := by
        apply div_nonneg
        · linarith
        · linarith
      linarith
    linarith
  exact h₄

-- ─────────────────────────────────────────────────────────────────────────
-- LEMMA 4: H(19.0) < 0.20
-- ─────────────────────────────────────────────────────────────────────────

/-- At s = 19, binary entropy ≈ 0.1985 < 0.20 -/
lemma binary_entropy_at_19 : binary_entropy 19.0 < 0.20 := by
  have h₁ : binary_entropy 19.0 = Real.log (19.0 + 1) - 19.0 * Real.log 19.0 / (19.0 + 1) := by
    norm_num [binary_entropy]
    <;> ring_nf
    <;> norm_num
  rw [h₁]
  have h₂ : Real.log (19.0 + 1 : ℝ) - 19.0 * Real.log 19.0 / (19.0 + 1 : ℝ) < 0.20 := by
    have := Real.log_two_gt_d9
    have := Real.log_two_lt_d9
    have h₃ : Real.log (20 : ℝ) < 2.995733 := by
      have := Real.log_two_lt_d9
      have h₄ : Real.log (20 : ℝ) = Real.log 2 + Real.log 10 := by
        have h₅ : Real.log (20 : ℝ) = Real.log (2 * 10 : ℝ) := by norm_num
        rw [h₅]
        have h₆ : Real.log (2 * 10 : ℝ) = Real.log 2 + Real.log 10 := by
          rw [Real.log_mul (by norm_num) (by norm_num)]
        rw [h₆]
      rw [h₄]
      have h₅ : Real.log 10 = Real.log 2 + Real.log 5 := by
        have h₆ : Real.log 10 = Real.log (2 * 5 : ℝ) := by norm_num
        rw [h₆]
        have h₇ : Real.log (2 * 5 : ℝ) = Real.log 2 + Real.log 5 := by
          rw [Real.log_mul (by norm_num) (by norm_num)]
        rw [h₇]
      rw [h₅]
      have h₆ : Real.log 5 < 1.609438 := by
        have := Real.log_two_lt_d9
        have h₇ : Real.log 5 = Real.log (10 / 2 : ℝ) := by norm_num
        rw [h₇]
        have h₈ : Real.log (10 / 2 : ℝ) = Real.log 10 - Real.log 2 := by
          rw [Real.log_div (by norm_num) (by norm_num)]
        rw [h₈]
        have h₉ : Real.log 10 = Real.log 2 + Real.log 5 := by
          have h₁₀ : Real.log 10 = Real.log (2 * 5 : ℝ) := by norm_num
          rw [h₁₀]
          have h₁₁ : Real.log (2 * 5 : ℝ) = Real.log 2 + Real.log 5 := by
            rw [Real.log_mul (by norm_num) (by norm_num)]
          rw [h₁₁]
        have h₁₀ : Real.log 5 < 1.609438 := by
          have := Real.log_two_lt_d9
          have := Real.log_two_gt_d9
          have h₁₁ : Real.log 5 < 1.609438 := by
            have h₁₂ : Real.exp 1.609438 > 5 := by
              have := Real.exp_one_gt_d9
              have := Real.exp_one_lt_d9
              norm_num [Real.exp_add, Real.exp_log, Real.exp_neg] at *
              <;>
              (try norm_num) <;>
              (try linarith) <;>
              (try nlinarith [Real.add_one_le_exp (1 : ℝ)])
            have h₁₃ : Real.log 5 < 1.609438 := by
              by_contra h₁₄
              have h₁₅ : Real.log 5 ≥ 1.609438 := by linarith
              have h₁₆ : Real.exp (Real.log 5) ≥ Real.exp 1.609438 := Real.exp_le_exp.mpr h₁₅
              have h₁₇ : Real.exp (Real.log 5) = 5 := by
                rw [Real.exp_log (by positivity)]
              rw [h₁₇] at h₁₆
              norm_num at h₁₂ h₁₆ ⊢
              <;> linarith
            exact h₁₃
          exact h₁₁
        linarith
      have h₇ : Real.log 2 > 0.693147 := by
        have := Real.log_two_gt_d9
        norm_num at this ⊢
        <;> linarith
      norm_num at h₆ h₇ ⊢
      <;> nlinarith
    have h₄ : Real.log (19 : ℝ) > 2.944438 := by
      have h₅ : Real.exp 2.944438 < 19 := by
        have := Real.exp_one_gt_d9
        have := Real.exp_one_lt_d9
        norm_num [Real.exp_add, Real.exp_log, Real.exp_neg] at *
        <;>
        (try norm_num) <;>
        (try linarith) <;>
        (try nlinarith [Real.add_one_le_exp (1 : ℝ)])
      have h₆ : Real.log 19 > 2.944438 := by
        by_contra h₇
        have h₈ : Real.log 19 ≤ 2.944438 := by linarith
        have h₉ : Real.exp (Real.log 19) ≤ Real.exp 2.944438 := Real.exp_le_exp.mpr h₈
        have h₁₀ : Real.exp (Real.log 19) = 19 := by
          rw [Real.exp_log (by positivity)]
        rw [h₁₀] at h₉
        norm_num at h₅ h₉ ⊢
        <;> linarith
      linarith
    have h₅ : Real.log (19 : ℝ) < 2.944439 := by
      have h₆ : Real.exp 2.944439 > 19 := by
        have := Real.exp_one_gt_d9
        have := Real.exp_one_lt_d9
        norm_num [Real.exp_add, Real.exp_log, Real.exp_neg] at *
        <;>
        (try norm_num) <;>
        (try linarith) <;>
        (try nlinarith [Real.add_one_le_exp (1 : ℝ)])
      have h₇ : Real.log 19 < 2.944439 := by
        by_contra h₈
        have h₉ : Real.log 19 ≥ 2.944439 := by linarith
        have h₁₀ : Real.exp (Real.log 19) ≥ Real.exp 2.944439 := Real.exp_le_exp.mpr h₉
        have h₁₁ : Real.exp (Real.log 19) = 19 := by
          rw [Real.exp_log (by positivity)]
        rw [h₁₁] at h₁₀
        norm_num at h₆ h₁₀ ⊢
        <;> linarith
      linarith
    norm_num at h₃ h₄ h₅ ⊢
    <;>
    (try norm_num) <;>
    (try linarith) <;>
    (try nlinarith)
  exact h₂

-- ─────────────────────────────────────────────────────────────────────────
-- MAIN THEOREM: Entropy bound during active execution
-- ─────────────────────────────────────────────────────────────────────────

/-- **SOVEREIGN ENTROPY THEOREM**
    During all active execution phases of the ICP engine (F ≥ 1),
    expert selection entropy H < 0.20 nats. -/
theorem sovereign_entropy_bound
    (F : FrustrationCount)
    (hF : F ≥ 1)
    (d : ℝ) (hd : d ≥ 1)
    : let T := temperature F
      let s := softmax_ratio d T
      binary_entropy s < 0.20 := by
  intro T s
  have hT_pos : 0 < T := by
    unfold T temperature
    have h₁ : (0.1 : ℝ) + 0.9 * Real.exp (-2.0 * (F : ℝ)) > 0 := by positivity
    have h₂ : max (0.1 : ℝ) (0.1 + 0.9 * Real.exp (-2.0 * (F : ℝ))) > 0 := by
      apply lt_max_iff.mpr
      exact Or.inl (by norm_num)
    positivity
  have hT_bound : T ≤ 0.2218 := temperature_bound_when_active F hF
  have hs_large : s ≥ 90.75 := softmax_ratio_lower_bound T d hT_pos hT_bound hd
  have hs_gt_19 : s > 19.0 := by linarith
  have h_main : binary_entropy s < binary_entropy 19.0 := by
    apply binary_entropy_decreasing (by norm_num) hs_gt_19
  have h_final : binary_entropy 19.0 < 0.20 := binary_entropy_at_19
  calc binary_entropy s
    < binary_entropy 19.0 := h_main
    _ < 0.20 := h_final

-- ─────────────────────────────────────────────────────────────────────────
-- COROLLARY: The entropy bound is a consequence of #minimize, not a check
-- ─────────────────────────────────────────────────────────────────────────

/-- The entropy bound is not an external constraint — it is a mathematical
    consequence of the minimization directive operating on a bipartite graph. -/
theorem entropy_bound_is_structural
    (F : FrustrationCount) (hF : F ≥ 1) (d : ℝ) (hd : d ≥ 1) :
    ∃ (H : ℝ), H = binary_entropy (softmax_ratio d (temperature F)) ∧ H < 0.20 :=
  ⟨binary_entropy (softmax_ratio d (temperature F)),
   rfl,
   sovereign_entropy_bound F hF d hd⟩

end SovereignEntropy