Encyclopedia Measurement Measurement Born Rule Two Outcome Measurement

ARTICLE 2 claims 2 theorems

Measurement Born Rule Two Outcome Measurement

In quantum mechanics, the probability of an outcome is the square of its amplitude; Recognition Science derives this rule from a cost of recognition, not from a postulate.

Verify this page

The two-outcome rule

The Born rule is a central law of quantum mechanics: when a measurement can yield two outcomes, the probability of each is the square of the absolute value of its quantum amplitude. For a system in a superposition of two states, with amplitudes α₁ and α₂, the rule states P(1) = |α₁|² and P(2) = |α₂|², provided the total probability sums to one. This rule, named after Max Born, who proposed it in 1926, is normally taken as an axiom of the theory, a basic assumption that is not derived from anything deeper.

Recognition Science offers a different starting point. It models a measurement as a two-outcome event with a recognition cost for each outcome, a number that represents how hard it is for reality to register that particular result. The framework then defines the probability of an outcome as the exponential of the negative cost, divided by the sum of such exponentials for all outcomes. For a two-outcome measurement with costs C₁ and C₂, the probability of outcome 1 is exp(-C₁) / (exp(-C₁) + exp(-C₂)), and similarly for outcome 2.

This definition is not arbitrary. The framework proves, in its machine-checked library of formal theorems, that these probabilities are always non-negative and that they sum to one, which is the normalization condition every probability distribution must satisfy. More significantly, the framework proves that for any two amplitudes whose squared magnitudes sum to one, there exists a two-outcome measurement whose probabilities exactly match those squared magnitudes. In other words, the Born rule emerges as a consequence of the cost structure, not as a separate assumption.

In Recognition Science, this is a derivation of the Born rule from the recognition cost functional and the amplitude bridge, the relationship that connects cost to amplitude. The framework does not claim that all measurements are two-outcome, nor does it specify what the costs C₁ and C₂ are for any particular physical system. It establishes the mathematical form of the rule and its internal consistency, leaving the physical interpretation of the costs as a separate question.

THEOREM prob₁_nonneg · prob₂_nonneg · 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)
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]

What this page does not claim

This answer does not claim that all quantum measurements are two-outcome measurements. This answer does not claim that the recognition costs C₁ and C₂ are known or specified for any particular physical system. This answer does not claim that the Born rule holds for 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND