Measurement Born Rule Light

The light Born rule

The Born rule is the quantum rule that turns a wavefunction's amplitude into the probability of an outcome: the probability equals the squared magnitude of the amplitude. In its usual textbook form, the rule requires a full quantum state and a measurement operator. The lightweight version, measurement born rule light, keeps only the algebraic core: if you have two amplitudes and two positive weights, and the weights match the squared amplitudes, then the squared amplitudes must sum to one. It is a minimal lemma, not a new physical law.

The setup uses two real numbers C₁ and C₂ that act as costs: larger cost means smaller weight, via the exponential exp(−C). The two weights, normalized so they add to one, are exp(−C₁)/(exp(−C₁)+exp(−C₂)) and exp(−C₂)/(exp(−C₁)+exp(−C₂)). The lemma assumes each normalized weight equals the squared magnitude of a complex amplitude, |α₁|² and |α₂|². The conclusion follows by algebra: the two normalized weights already sum to one, so the two squared amplitudes do too.

In Recognition Science, the framework models measurement as a discrete record of recognition events, and each possible outcome carries a cost. The light Born rule connects that cost picture to standard probability: when costs are exponentiated and normalized, they satisfy the same normalization condition that quantum probabilities satisfy. This result is verified in a machine-checked library of formal theorems, so the step from costs to probabilities is checked mechanically.

The practical point is that the Born rule's normalization is not an extra assumption; it follows from the way weights are built. If you define outcome weights as normalized exponentials of costs, you get probabilities that automatically sum to one. The result establishes that bridge in plain algebra, with no heavy quantum machinery. That is what the name means: a light, dependency-free version of the Born rule that still carries the essential normalization.

/-- Born rule normalized: from recognition weights to normalized probabilities. -/
theorem born_rule_normalized (C₁ C₂ : ℝ) (α₁ α₂ : ℂ)
  (h₁ : Real.exp (-C₁) / (Real.exp (-C₁) + Real.exp (-C₂)) = ‖α₁‖ ^ 2)
  (h₂ : Real.exp (-C₂) / (Real.exp (-C₁) + Real.exp (-C₂)) = ‖α₂‖ ^ 2) :
  ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 = 1 := by
  have hdenom : Real.exp (-C₁) + Real.exp (-C₂) ≠ 0 :=
    (add_pos (Real.exp_pos _) (Real.exp_pos _)).ne'
  calc ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2
      = Real.exp (-C₁) / (Real.exp (-C₁) + Real.exp (-C₂)) +
        Real.exp (-C₂) / (Real.exp (-C₁) + Real.exp (-C₂)) := by
          rw [← h₁, ← h₂]
      _ = (Real.exp (-C₁) + Real.exp (-C₂)) / (Real.exp (-C₁) + Real.exp (-C₂)) := by
          rw [div_add_div_same]
      _ = 1 := div_self hdenom

What this page does not claim

This result does not derive the full quantum measurement postulate; it only proves a normalization identity. The lemma does not explain why probabilities equal squared amplitudes; it assumes that equality as a premise. No claim is made that costs are observable or that the exponential form is unique.

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/BornRuleLight.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: