Quantum Born Rule

The Born rule

The Born rule is the quantum mechanical prescription for turning a wave function into probabilities. For a system described by a complex wave function ψ, the probability of finding it in a particular state is the square of the wave function's magnitude: P = |ψ|². This rule, named after Max Born who proposed it in 1926, is one of the few places in standard quantum mechanics where a fundamental postulate is needed. It is not derived from deeper principles within the conventional theory; it is simply accepted because it works.

The rule has two essential features that make it physically sensible. First, it is phase-invariant: multiplying a wave function by a complex phase e^{iθ} does not change the probability, since |e^{iθ}·ψ|² = |ψ|². Second, it is additive over disjoint possibilities: the probability of finding the system in one of several mutually exclusive states is the sum of the individual probabilities. These properties are what allow probabilities to be well-defined and to sum to one for a complete set of outcomes.

In Recognition Science, the Born rule is not a postulate. The framework models physical states as discrete records of recognition events, called a ledger, a structured list of what has been registered. The framework's central cost function, which measures the price of maintaining such a record, has been proved to take a specific form, and from that cost structure the Born rule is forced. The derivation works by decomposing any normalized state into eight orthogonal modes using a discrete Fourier transform, and then showing that the only probability assignment consistent with the cost structure is the squared modulus.

The machine-checked library of formal theorems proves that the sector measure, defined as the sum of squared moduli over a set of modes, is the unique probability assignment satisfying four conditions: normalization, phase invariance, additivity over disjoint mode sets, and consistency with a two-branch calibration. This last condition is what pins down the exponent: for a two-outcome measurement, the probability must match the exp(−C) Gibbs weighting, which forces the weight function to be r ↦ r². The result is a Gleason-style theorem: the Born rule is the unique probability measure compatible with the Recognition Science axioms.

What this means in plain language is that if you accept the framework's starting point, that reality keeps a discrete record and that the cost of recognition is forced, then the quantum mechanical probability rule is not an extra assumption. It is a consequence. The framework proves that any probability assignment satisfying the basic structural requirements must be the squared magnitude. This is a strong result: it removes one of the most mysterious postulates from quantum mechanics and shows it follows from a more fundamental principle about how recognition works.

/-- The Born rule follows from J-cost structure: on any normalised Signal8,
    the sector measure μ(S) = Σ_{k∈S} ‖ψ_k‖² is the unique probability
    assignment satisfying normalisation + phase invariance + additivity +
    two-branch calibration. -/
theorem born_rule_from_jcost (ψ : Signal8) (h : IsNormalized ψ)
    (S : Finset (Fin 8)) :
    (sectorMeasure ψ Finset.univ = 1) ∧
    (∀ θ : Fin 8 → ℝ,
      sectorMeasure (phaseRotate ψ θ) S = sectorMeasure ψ S) ∧
    (∀ T : Finset (Fin 8), Disjoint S T →
      sectorMeasure ψ (S ∪ T) = sectorMeasure ψ S + sectorMeasure ψ T) ∧
    (∀ rot : IndisputableMonolith.Measurement.TwoBranchRotation,
      sectorMeasure (twoBranchSignal rot) {0} =
        IndisputableMonolith.Verification.TwoOutcomeBorn.P_cos rot ∧
      sectorMeasure (twoBranchSignal rot) {1} =
        IndisputableMonolith.Verification.TwoOutcomeBorn.P_sin rot) :=
  dft8_sector_forcing ψ h S

/-- Gleason-style result: the sector measure is the unique probability
    assignment forced by the RS axioms (phase invariance, additivity,
    two-branch calibration via exp(-C) Gibbs weighting).
    The weight function is forced to be r ↦ r². -/
theorem gleason_from_rs (w : ℝ → ℝ)
    (hw : ∀ θ : ℝ, 0 < θ → θ < Real.pi / 2 →
          w (Real.cos θ) = (Real.cos θ) ^ 2) :
    ∀ r : ℝ, 0 < r → r < 1 → w r = r ^ 2 :=
  born_weight_forced w hw

/-- The Born rule is phase-independent: |r·e^{iθ}|² = r². -/
theorem born_rule_phase_independent (r θ : ℝ) :
    Complex.normSq (↑r * Complex.exp (θ * Complex.I)) = r^2 := by
  rw [Complex.normSq_mul, normSq_exp_I_eq_one, mul_one, Complex.normSq_ofReal]; ring

/-- Gleason-style result: the sector measure is the unique probability
    assignment forced by the RS axioms (phase invariance, additivity,
    two-branch calibration via exp(-C) Gibbs weighting).
    The weight function is forced to be r ↦ r². -/
theorem gleason_from_rs (w : ℝ → ℝ)
    (hw : ∀ θ : ℝ, 0 < θ → θ < Real.pi / 2 →
          w (Real.cos θ) = (Real.cos θ) ^ 2) :
    ∀ r : ℝ, 0 < r → r < 1 → w r = r ^ 2 :=
  born_weight_forced w hw

What this page does not claim

The Born rule is derived for all possible quantum systems, not just the eight-mode sector. The framework explains why the universe uses complex numbers rather than real ones. The derivation replaces the need for experimental verification of the Born rule.

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/Quantum/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: