IndisputableMonolith.Verification.ProbabilityNormalizationCert

   1import Mathlib
   2import IndisputableMonolith.Measurement.BornRuleLight
   3
   4/-!
   5# Probability Normalization Certificate
   6
   7This certificate proves that recognition-weighted probabilities are properly normalized:
   8any two recognition costs C₁ and C₂ produce probabilities that sum to 1.
   9
  10## The Key Theorem
  11
  12For any costs C₁, C₂ ∈ ℝ:
  13```
  14exp(-C₁)/(exp(-C₁) + exp(-C₂)) + exp(-C₂)/(exp(-C₁) + exp(-C₂)) = 1
  15```
  16
  17This is the algebraic foundation ensuring that Recognition Science's two-outcome
  18measurement model produces valid probability distributions.
  19
  20## Why This Matters
  21
  22This property ensures:
  231. **Probability conservation**: Outcomes always sum to 100%
  242. **No missing probability**: The model is complete
  253. **No excess probability**: The model is consistent
  26
  27The proof uses only:
  28- Positivity of `exp` function: `exp(x) > 0` for all x
  29- Division algebra: `a/d + b/d = (a+b)/d`
  30- Self-division: `x/x = 1` for x ≠ 0
  31
  32## Non-Circularity
  33
  34This is a pure algebraic fact about exponentials - no physical assumptions needed.
  35The proof is from elementary real analysis (Mathlib's `exp_pos` and `div_self`).
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Verification
  40namespace ProbabilityNormalization
  41
  42open Real
  43
  44/-- Probability from recognition cost C₁ relative to C₂. -/
  45noncomputable def prob_from_cost (C₁ C₂ : ℝ) : ℝ :=
  46  Real.exp (-C₁) / (Real.exp (-C₁) + Real.exp (-C₂))
  47
  48/-- Exponentials are always positive. -/
  49lemma exp_sum_pos (C₁ C₂ : ℝ) : 0 < Real.exp (-C₁) + Real.exp (-C₂) :=
  50  add_pos (exp_pos _) (exp_pos _)
  51
  52/-- Exponentials sum to non-zero. -/
  53lemma exp_sum_ne_zero (C₁ C₂ : ℝ) : Real.exp (-C₁) + Real.exp (-C₂) ≠ 0 :=
  54  (exp_sum_pos C₁ C₂).ne'
  55
  56/-- Probability is non-negative. -/
  57lemma prob_nonneg (C₁ C₂ : ℝ) : 0 ≤ prob_from_cost C₁ C₂ := by
  58  unfold prob_from_cost
  59  apply div_nonneg
  60  · exact (exp_pos _).le
  61  · exact (exp_sum_pos C₁ C₂).le
  62
  63/-- Probability is at most 1. -/
  64lemma prob_le_one (C₁ C₂ : ℝ) : prob_from_cost C₁ C₂ ≤ 1 := by
  65  unfold prob_from_cost
  66  rw [div_le_one (exp_sum_pos C₁ C₂)]
  67  exact le_add_of_nonneg_right (exp_pos _).le
  68
  69/-- Core theorem: probabilities from recognition costs sum to 1. -/
  70theorem prob_normalization (C₁ C₂ : ℝ) :
  71    prob_from_cost C₁ C₂ + prob_from_cost C₂ C₁ = 1 := by
  72  unfold prob_from_cost
  73  rw [add_comm (Real.exp (-C₂)) (Real.exp (-C₁))]
  74  rw [← add_div]
  75  exact div_self (exp_sum_ne_zero C₁ C₂)
  76
  77structure ProbabilityNormalizationCert where
  78  deriving Repr
  79
  80/-- Verification predicate: recognition-weighted probabilities are normalized.
  81
  82Certifies:
  831. prob_from_cost produces non-negative values
  842. prob_from_cost produces values at most 1
  853. Two complementary probabilities sum to exactly 1
  86-/
  87@[simp] def ProbabilityNormalizationCert.verified (_c : ProbabilityNormalizationCert) : Prop :=
  88  -- 1) Probabilities are non-negative
  89  (∀ C₁ C₂ : ℝ, 0 ≤ prob_from_cost C₁ C₂) ∧
  90  -- 2) Probabilities are at most 1
  91  (∀ C₁ C₂ : ℝ, prob_from_cost C₁ C₂ ≤ 1) ∧
  92  -- 3) Complementary probabilities sum to 1
  93  (∀ C₁ C₂ : ℝ, prob_from_cost C₁ C₂ + prob_from_cost C₂ C₁ = 1)
  94
  95/-- Top-level theorem: the probability normalization certificate verifies. -/
  96@[simp] theorem ProbabilityNormalizationCert.verified_any (c : ProbabilityNormalizationCert) :
  97    ProbabilityNormalizationCert.verified c := by
  98  refine ⟨?nonneg, ?le_one, ?sum_one⟩
  99  · exact prob_nonneg
 100  · exact prob_le_one
 101  · exact prob_normalization
 102
 103end ProbabilityNormalization
 104end Verification
 105end IndisputableMonolith
 106