Measurement Born Rule Probabilities Normalized

Normalized probabilities

The Born rule is a central part of quantum mechanics. It states that when a quantum system is measured, the probability of a particular outcome equals the square of the absolute value of the corresponding amplitude. For a two-outcome measurement, if the amplitudes are α₁ and α₂, then the probabilities are |α₁|² and |α₂|². These probabilities always sum to one, because the total probability of any measurement outcome is certain.

In Recognition Science, this rule is not taken as a separate axiom. The framework models a measurement as a choice between two possible outcomes, each carrying a recognition cost, a number representing the effort the universe's ledger spends to register that outcome. The probability of an outcome is then defined as a decreasing exponential function of its cost: higher cost means lower probability. Specifically, for costs C₁ and C₂, the probability of outcome one is exp(-C₁) / (exp(-C₁) + exp(-C₂)), and similarly for outcome two.

The declaration probabilities_normalized is a theorem in the framework's machine-checked library of formal theorems. It proves that these two defined probabilities always sum to exactly one, for any non-negative costs. This is the normalization condition that any valid probability distribution must satisfy. The proof is a direct consequence of the definitions, relying on the fact that the denominator is the sum of the two numerator terms.

This normalization is a necessary step, but it is not the full Born rule. The framework also proves a separate theorem, born_rule_from_C, which shows that for any two amplitudes whose squares sum to one, there exist recognition costs such that the cost-based probabilities equal those amplitude squares. That theorem connects the cost model to the quantum mechanical rule. The normalization theorem alone only guarantees the internal consistency of the probability definitions.

What probabilities_normalized does not claim is that it, by itself, derives the Born rule from recognition costs. It establishes that the cost-based probabilities are properly normalized. The connection to quantum amplitudes is made by the separate born_rule_from_C theorem. The normalization theorem is a piece of the structure, not the whole derivation.

/-- Probabilities sum to 1 (normalization) -/
theorem probabilities_normalized (m : TwoOutcomeMeasurement) :
  prob₁ m + prob₂ m = 1 := by
  unfold prob₁ prob₂
  have hdenom : Real.exp (-m.C₁) + Real.exp (-m.C₂) ≠ 0 :=
    (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
  set denom : ℝ := Real.exp (-m.C₁) + Real.exp (-m.C₂)
  have hadd :
      Real.exp (-m.C₁) / denom + Real.exp (-m.C₂) / denom = (Real.exp (-m.C₁) + Real.exp (-m.C₂)) / denom := by
    simpa [denom] using (add_div (Real.exp (-m.C₁)) (Real.exp (-m.C₂)) denom).symm
  -- Finish.
  simpa [denom, hadd] using (div_self hdenom)

What this page does not claim

probabilities_normalized does not, by itself, derive the Born rule from recognition costs. The theorem does not assign any physical meaning to the recognition costs. The theorem does not address measurements 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/Measurement/BornRule.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: