Encyclopedia Measurement Measurement Born Rule Born Rule Normalized

ARTICLE 3 claims 3 theorems

Measurement Born Rule Born Rule Normalized

A machine-checked theorem shows that when probabilities are built from recognition costs, they are forced to add up to one, mirroring the quantum Born rule.

Verify this page

The normalization theorem

The Born rule is the quantum mechanical prescription that turns a wavefunction into a probability: for a two-outcome measurement, the probability of outcome I is the squared magnitude of its amplitude, P(I) = |αI|². The rule was named after Max Born, who proposed it in 1926, and it remains a postulate of standard quantum theory: it tells you what the mathematics means at the moment of measurement, but it does not say why that particular formula, instead of some other, should hold.

The Recognition Science framework attempts to derive the rule from a different starting point. In this account, the universe keeps a ledger, a discrete record of recognition events, and the cost of recognition is a forced quantity, not a free choice. From a proved cost function J(x) = (x + 1/x)/2 - 1, the framework defines a bridge from cost to amplitude, 𝓪 = exp(-C/2)·exp(iφ), where C is the recognition cost and φ is a phase. The probability of an outcome is then taken to be the exponential of its negative cost, normalized against all possible outcomes.

In this framework, the declaration born_rule_normalized establishes a precise consequence: if you define the probability of outcome 1 as exp(-C₁)/(exp(-C₁) + exp(-C₂)) and the probability of outcome 2 as exp(-C₂)/(exp(-C₁) + exp(-C₂)), where C₁ and C₂ are the recognition costs for the two outcomes, then the two probabilities sum to 1. The theorem is proved in the framework's machine-checked library of formal theorems, with the full statement: given the two cost-to-probability equations and the two amplitudes α₁ and α₂, it follows that |α₁|² + |α₂|² = 1. This is the normalization condition of quantum mechanics, derived here from the structure of recognition costs rather than assumed as a separate axiom.

What the declaration does not claim is just as important. It does not claim that the Born rule itself is derived from scratch; that is the job of a separate theorem, born_rule_from_C, which requires additional structure, a two-branch rotation, to connect costs to amplitudes. The normalized theorem only shows that if you accept the cost-to-probability map, then normalization follows. It does not say which costs C₁ and C₂ are realized in nature, nor does it explain why the amplitude bridge takes the exponential form. Those are modeling choices, not consequences of this theorem.

The practical consequence is a consistency check. In the framework, the normalization of probabilities is not an independent postulate but a forced result of the cost structure. A reader who accepts the framework's cost function and its bridge from cost to amplitude gets normalization for free. A reader who does not accept those premises sees only a conditional statement: if the probabilities are defined this way, they sum to one. The theorem itself is silent on which reading is correct.

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 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 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 the Born rule is derived without additional assumptions; the normalized theorem is conditional on the cost-to-probability map. This answer does not claim that the framework identifies which recognition costs C₁ and C₂ are realized in physical 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