Encyclopedia Measurement Measurement Born Rule Born Rule From C

ARTICLE 3 claims 2 theorems 1 model

Measurement Born Rule Born Rule From C

Quantum probabilities can be written as a ratio of recognition costs; the theorem shows the two forms are equivalent.

Verify this page

The Born rule from costs

In quantum mechanics, the Born rule is the prescription that the probability of a measurement outcome equals the squared magnitude of the corresponding complex amplitude. For a two-outcome measurement on a state with amplitudes α₁ and α₂, the rule states P(1) = |α₁|² and P(2) = |α₂|², with the normalization |α₁|² + |α₂|² = 1. This rule, named after Max Born, is one of the foundational postulates of the theory; it is not derived from deeper principles in the standard formulation.

The Recognition Science framework proposes a different starting point. It models each possible measurement outcome as carrying a recognition cost (a non-negative real number C₁ or C₂) that the system must pay to identify that outcome. The framework then defines the probability of an outcome as the exponential of its negative cost, normalized against the sum for all outcomes: P(1) = exp(−C₁) / (exp(−C₁) + exp(−C₂)). This is a definitional choice (tagged MODEL), not a theorem; it chooses how costs translate into probabilities.

What the framework's machine-checked library proves is that the two descriptions coincide. The theorem born_rule_from_C states that for any two normalized amplitudes (|α₁|² + |α₂|² = 1) satisfying a certain rotation condition, there exist recognition costs C₁ and C₂ such that the cost-derived probabilities exactly equal the squared amplitudes: exp(−C₁) / (exp(−C₁) + exp(−C₂)) = |α₁|². The same library proves the converse normalization: if the cost-derived probabilities equal the squared amplitudes, then the amplitudes are automatically normalized. Together these establish a formal equivalence: the Born rule's probability assignment can be reproduced exactly by choosing appropriate recognition costs.

This is a structural result about the mathematics, not a physical claim about how measurements actually happen. The theorem does not assert that recognition costs are physically real, that the rotation condition is always satisfied, or that the framework has derived the Born rule from first principles. It shows that the cost model is expressive enough to encode the standard rule, and that the two formalisms agree where the model's conditions hold. The library's proof is machine-checked, meaning the logical derivation is verified step by step, but the choice of the cost model itself remains a modeling assumption.

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]
MODEL prob₁ · IndisputableMonolith/Measurement/BornRule.lean

Lean source not resolved on this build host. The module path in the line above is the public reference.

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

What this page does not claim

The theorem does not claim that recognition costs are physically real quantities. It does not derive the Born rule from first principles; it shows the cost model can reproduce it. It does not assert that the rotation condition is satisfied for all quantum measurements.

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