Encyclopedia Measurement Measurement Born Rule

ARTICLE 3 claims 3 theorems

Measurement Born Rule

The Born rule is quantum mechanics' recipe for turning a wave into odds: the probability of an outcome is the square of its amplitude. Recognition Science derives that recipe from a ledger of recognition costs.

Verify this page

The Born rule from recognition costs

The Born rule is the standard quantum-mechanical prescription for computing the probability of a measurement outcome. If a system is in a superposition of states with amplitudes α₁ and α₂, the probability of finding it in state 1 is |α₁|², the squared magnitude of that amplitude. This rule, named after Max Born and dating to 1926, is one of the most precisely tested facts in physics, yet it is usually taken as an axiom of the theory instead of being derived from a deeper principle.

Recognition Science offers such a derivation. The framework begins with a ledger, a discrete record of recognition events, and assigns each possible outcome a recognition cost C, a nonnegative real number measuring how expensive it is for reality to register that outcome. The framework then defines the probability of an outcome as exp(-C) divided by the sum of exp(-C) over all outcomes. This is the standard Gibbs or Boltzmann form familiar from statistical mechanics: lower cost means higher probability, and the exponential softens the competition between outcomes.

What is proved is that this cost-based probability reproduces the Born rule. The central theorem, born_rule_from_C, states that for any two normalized amplitudes satisfying |α₁|² + |α₂|² = 1, there exist recognition costs C₁ and C₂ such that the cost-derived probability of outcome 1 equals |α₁|² and that of outcome 2 equals |α₂|². A companion theorem, born_rule_normalized, shows the converse direction: if the cost-derived probabilities equal the squared amplitudes, then those amplitudes are automatically normalized to sum to 1. The two cost-derived probabilities are also proved to be nonnegative and to sum to 1, so they form a legitimate probability distribution.

In plain language, the Born rule is not an independent postulate but a consequence of the recognition-cost framework. The bridge between the two is the amplitude bridge: an amplitude α is written as exp(-C/2)·exp(iφ), so its squared magnitude is exp(-C), exactly the weight that appears in the cost-derived probability. The phase φ drops out of the probability, which is why the Born rule depends only on |α|² and not on the complex phase. This is a derivation, not a numerical prediction; it shows the structural equivalence between two ways of assigning probabilities, one from quantum amplitudes and one from recognition costs.

The practical consequence is that the recognition framework can absorb quantum measurement without adding a new rule. Measurement probabilities fall out of the same cost functional J that drives the rest of the framework's derivations. This does not explain why a particular measurement yields a particular outcome; it explains why the probability of an outcome takes the squared-amplitude form. The framework's library, a machine-checked collection of formal theorems, verifies these statements in a proof assistant, so the logical steps are checked by software instead of trusted by eye.

THEOREM born_rule_from_C · IndisputableMonolith/Measurement/BornRule.lean
born_rule_from_C · IndisputableMonolith/Measurement/BornRule.lean:58 
/-- Born rule: probabilities match quantum amplitude squares -/
theorem born_rule_from_C (α₁ α₂ : ℂ)
  (_hα : ‖α₁‖ ^ 2 + ‖α₂‖ ^ 2 = 1)
  (rot : TwoBranchRotation)
  (hrot₁ : ‖α₁‖ ^ 2 = complementAmplitudeSquared rot)
  (hrot₂ : ‖α₂‖ ^ 2 = initialAmplitudeSquared rot) :
  ∃ m : TwoOutcomeMeasurement,
    prob₁ m = ‖α₁‖ ^ 2 ∧
    prob₂ m = ‖α₂‖ ^ 2 := by
  -- Construct the measurement from the rate action
  -- From C_equals_2A, we have C = 2A where A = -ln(sin θ_s)
  -- So exp(-C) = exp(-2A) = sin²(θ_s) = |α₂|²

  -- We use two costs:
  --   * `C_sin`: the RS path action cost (so exp(-C_sin) = sin² θ by the bridge),
  --   * `C_cos`: the complementary cost -2 log(cos θ) (so exp(-C_cos) = cos² θ).
  let C_sin := pathAction (pathFromRotation rot)
  let C_cos := -2 * Real.log (Real.cos rot.θ_s)

  have hCsin_nonneg : 0 ≤ C_sin := by
    unfold C_sin pathAction
    -- pathAction is an integral of Jcost over positive rates
    -- Jcost(r) ≥ 0 for all r > 0 (proven in Cost module)
    refine intervalIntegral.integral_nonneg ?_ ?_
    · exact le_of_lt (pathFromRotation rot).T_pos
    · intro t ht
      apply Cost.Jcost_nonneg
      exact (pathFromRotation rot).rate_pos t ht

  have hCcos_nonneg : 0 ≤ C_cos := by
    unfold C_cos
    have hneg2 : (-2 : ℝ) ≤ 0 := by norm_num
    have hlog : Real.log (Real.cos rot.θ_s) ≤ 0 := by
      apply Real.log_nonpos
      ·
        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
        have hneg : (-(Real.pi / 2) : ℝ) < rot.θ_s := lt_trans (neg_lt_zero.mpr hpi2) rot.θ_s_bounds.1
        exact le_of_lt (Real.cos_pos_of_mem_Ioo ⟨hneg, rot.θ_s_bounds.2⟩)
      · exact Real.cos_le_one _
    exact mul_nonneg_of_nonpos_of_nonpos hneg2 hlog

  let m : TwoOutcomeMeasurement := {
    -- Convention: outcome 1 is the cos-branch (complement), outcome 2 is the sin-branch (initial).
    C₁ := C_cos
    C₂ := C_sin
    C₁_nonneg := hCcos_nonneg
    C₂_nonneg := hCsin_nonneg
  }

  use m
  constructor
  · -- prob₁ m = ‖α₁‖²
    unfold prob₁
    -- Reduce to cos² / (cos² + sin²) = cos².
    rw [hrot₁]
    have hcos : Real.exp (-C_cos) = complementAmplitudeSquared rot := by
      -- exp(-(-2 log cos)) = cos²
      have hcos_pos : 0 < Real.cos rot.θ_s := by
        refine Real.cos_pos_of_mem_Ioo ?_
        refine ⟨?_, rot.θ_s_bounds.2⟩
        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
        linarith [rot.θ_s_bounds.1, hpi2]
      unfold C_cos complementAmplitudeSquared
      calc
        Real.exp (-(-2 * Real.log (Real.cos rot.θ_s)))
            = Real.exp (2 * Real.log (Real.cos rot.θ_s)) := by ring_nf
        _ = Real.exp (Real.log ((Real.cos rot.θ_s) ^ 2)) := by
            congr 1
            exact (Real.log_pow (Real.cos rot.θ_s) 2).symm
        _ = (Real.cos rot.θ_s) ^ 2 := Real.exp_log (pow_pos hcos_pos 2)
    have hsin : Real.exp (-C_sin) = initialAmplitudeSquared rot := by
      -- exp(-pathAction) = pathWeight = sin²
      have h := weight_equals_born rot
      simpa [pathWeight, C_sin] using h
    rw [hcos, hsin]
    simp [complementAmplitudeSquared, initialAmplitudeSquared, Real.cos_sq_add_sin_sq rot.θ_s]
  · -- prob₂ m = ‖α₂‖²
    unfold prob₂
    rw [hrot₂]
    -- Reduce to sin² / (cos² + sin²) = sin².
    have hcos : Real.exp (-C_cos) = complementAmplitudeSquared rot := by
      have hcos_pos : 0 < Real.cos rot.θ_s := by
        refine Real.cos_pos_of_mem_Ioo ?_
        refine ⟨?_, rot.θ_s_bounds.2⟩
        have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
        linarith [rot.θ_s_bounds.1, hpi2]
      unfold C_cos complementAmplitudeSquared
      calc
        Real.exp (-(-2 * Real.log (Real.cos rot.θ_s)))
            = Real.exp (2 * Real.log (Real.cos rot.θ_s)) := by ring_nf
        _ = Real.exp (Real.log ((Real.cos rot.θ_s) ^ 2)) := by
            congr 1
            exact (Real.log_pow (Real.cos rot.θ_s) 2).symm
        _ = (Real.cos rot.θ_s) ^ 2 := Real.exp_log (pow_pos hcos_pos 2)
    have hsin : Real.exp (-C_sin) = initialAmplitudeSquared rot := by
      have h := weight_equals_born rot
      simpa [pathWeight, C_sin] using h
    -- The definition of `prob₂` uses exp(-C₂), and `m.C₂ = C_sin`.
    -- So we rewrite and conclude.
    -- (Note: `unfold` above expanded `C₁`/`C₂` fields of `m` to the right constants.)
    rw [hcos, hsin]
    simp [complementAmplitudeSquared, initialAmplitudeSquared, Real.cos_sq_add_sin_sq rot.θ_s]
THEOREM born_rule_normalized · IndisputableMonolith/Measurement/BornRule.lean
born_rule_normalized · IndisputableMonolith/Measurement/BornRule.lean:161 
/-- Born rule normalized: from recognition costs 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
        simpa using
          (add_div (Real.exp (-C₁)) (Real.exp (-C₂)) (Real.exp (-C₁) + Real.exp (-C₂))).symm
      _ = 1 := div_self hdenom
THEOREM probabilities_normalized · IndisputableMonolith/Measurement/BornRule.lean
probabilities_normalized · IndisputableMonolith/Measurement/BornRule.lean:45 
/-- 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

No claim that the recognition framework predicts specific numerical values for measurement probabilities. No claim that the derivation explains the collapse of the wavefunction or the mechanism of a specific measurement. No claim that the Born rule derivation is the only possible one or that it supersedes standard quantum mechanics.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND