Verification Probability Normalization Cert

The normalization certificate

In probability theory, a set of outcomes is normalized when their probabilities add up to exactly 1, meaning 100%. This certificate is a machine-checked proof that Recognition Science's two-outcome measurement model always satisfies this property. The model assigns a probability to each of two possible outcomes based on their recognition costs, which are real numbers representing the price of recognizing each outcome.

The probability of the first outcome is computed as exp(-C₁) / (exp(-C₁) + exp(-C₂)), where C₁ and C₂ are the two costs. The probability of the second outcome swaps the roles: exp(-C₂) / (exp(-C₁) + exp(-C₂)). The certificate proves that these two expressions always sum to exactly 1, for any real costs C₁ and C₂. The proof relies only on elementary facts: exponentials are always positive, so the denominator is never zero, and division algebra shows the sum of the two fractions equals 1.

The certificate also verifies two supporting properties. First, each individual probability is non-negative, meaning it can never be below 0. Second, each probability is at most 1, meaning it can never exceed 100%. Together with the sum-to-1 theorem, these three properties guarantee the model produces a valid probability distribution: no outcome is impossible, no outcome is certain beyond the model's scope, and the two outcomes together account for all probability.

In Recognition Science, this certificate provides a foundational check. The framework models recognition events through costs, and this certificate confirms that the two-outcome measurement model is internally consistent. The proof is a pure algebraic fact about exponentials, requiring no physical assumptions. It is formalized in a machine-checked library of formal theorems, meaning the proof has been verified by a computer to be correct.

The practical consequence is that anyone using this model can rely on its probabilities summing correctly. This is a necessary condition for any probabilistic model to be meaningful, and the certificate establishes it rigorously. The result is not an approximation or a heuristic; it is an exact theorem that holds for all real-valued costs.

/-- Core theorem: probabilities from recognition costs sum to 1. -/
theorem prob_normalization (C₁ C₂ : ℝ) :
    prob_from_cost C₁ C₂ + prob_from_cost C₂ C₁ = 1 := by
  unfold prob_from_cost
  rw [add_comm (Real.exp (-C₂)) (Real.exp (-C₁))]
  rw [← add_div]
  exact div_self (exp_sum_ne_zero C₁ C₂)

/-- Probability is non-negative. -/
lemma prob_nonneg (C₁ C₂ : ℝ) : 0 ≤ prob_from_cost C₁ C₂ := by
  unfold prob_from_cost
  apply div_nonneg
  · exact (exp_pos _).le
  · exact (exp_sum_pos C₁ C₂).le

/-- Probability is at most 1. -/
lemma prob_le_one (C₁ C₂ : ℝ) : prob_from_cost C₁ C₂ ≤ 1 := by
  unfold prob_from_cost
  rw [div_le_one (exp_sum_pos C₁ C₂)]
  exact le_add_of_nonneg_right (exp_pos _).le

/-- Exponentials are always positive. -/
lemma exp_sum_pos (C₁ C₂ : ℝ) : 0 < Real.exp (-C₁) + Real.exp (-C₂) :=
  add_pos (exp_pos _) (exp_pos _)

What this page does not claim

This certificate does not prove that the cost function itself is unique or derived. It does not establish any physical interpretation of the costs beyond their algebraic role. It does not cover probability models with more than two outcomes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/ProbabilityNormalizationCert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: