Encyclopedia Foundation Foundation Born Rule Forcing

ARTICLE 4 claims 4 theorems

Foundation Born Rule Forcing

In quantum mechanics, the Born rule says the probability of an outcome is the squared amplitude. Recognition Science claims its own framework forces that rule, not from experiment but from four plain assumptions.

Verify this page

The Born rule, forced

The Born rule is a central part of quantum mechanics. It states that when a system is in a state described by complex amplitudes ψ_k, the probability of finding it in a particular mode k is the square of the amplitude's magnitude, |ψ_k|². This rule, named after Max Born, was proposed in 1926 and has been verified by countless experiments, yet its origin has remained a postulate, an extra assumption added to the theory because it works.

Recognition Science, a framework built on the idea that reality keeps a ledger, a discrete record of recognition events, claims to derive this rule from deeper structure. The module in question, called BornRuleForcing, starts with a system of eight modes, a finite signal space. It defines a measure on subsets of these modes, which assigns a probability to any collection of outcomes. The central theorem, modeLocal_born_unique, proves that if this measure satisfies four conditions, it must be the standard Born rule.

Those four conditions are the heart of the claim. First, the measure must be normalized: for any valid state, the total probability over all modes is 1. Second, it must be phase-invariant: changing the complex phase of each amplitude, which does not alter any physical prediction, leaves the measure unchanged. Third, it must be additive over disjoint sets of modes, meaning the probability of two separate outcomes is the sum of their individual probabilities. Fourth, it must agree with a known two-branch case, a simple two-outcome system where the Born rule is already established.

The proof works by showing that any measure satisfying these conditions must assign to each mode a weight that is a function of the amplitude's magnitude alone. A key lemma, born_weight_forced, then shows that this function must be the square function, not any other power. The argument uses the two-branch calibration to pin down the function on a dense set of values, and continuity to extend it everywhere. The result is that the measure is exactly the sum of squared amplitudes over the chosen modes, the Born rule itself.

In Recognition Science, this is not a restatement of an assumption but a derivation. The framework's library, a machine-checked collection of formal theorems, contains the full proof. The module also shows that a different measure, one that uses fourth powers for states with more than two occupied modes, is possible but fails the phase-invariance condition. This contrast highlights that the Born rule is not arbitrary; it is the unique measure consistent with the framework's basic principles.

What this establishes, in plain language, is that within Recognition Science, the probabilistic law of quantum mechanics is not a free choice. It is forced by the same kind of logical necessity that forces other constants in the framework. The result does not prove the Born rule is true in the physical world; that remains an empirical fact. It proves that if the framework's axioms are accepted, the Born rule follows as a theorem, not as an additional postulate.

THEOREM modeLocal_born_unique · IndisputableMonolith/Foundation/BornRuleForcing.lean
modeLocal_born_unique · IndisputableMonolith/Foundation/BornRuleForcing.lean:318 
/-- Within the mode-local class, normalization and two-branch calibration force
the sector measure to be the Born sector measure on every normalized signal. -/
theorem modeLocal_born_unique (μ : Signal8 → Finset (Fin 8) → ℝ)
    (W : ModeLocalWitness μ)
    (hnorm : ∀ ψ, IsNormalized ψ → μ ψ Finset.univ = 1)
    (hcal : ∀ rot : TwoBranchRotation, μ (twoBranchSignal rot) {0} = P_cos rot) :
    ∀ ψ, IsNormalized ψ → ∀ S, μ ψ S = sectorMeasure ψ S := by
  have hg : ∀ θ : ℝ, 0 < θ → θ < Real.pi / 2 →
      W.g (Real.cos θ) = (Real.cos θ) ^ 2 := by
    intro θ hθ0 hθhalf
    let rot : TwoBranchRotation :=
      { θ_s := θ
        θ_s_bounds := ⟨hθ0, hθhalf⟩
        T := 1
        T_pos := one_pos }
    have hcos_pos : 0 < Real.cos θ := cos_pos_on_Ioo_zero_half_pi hθ0 hθhalf
    have hμ : μ (twoBranchSignal rot) ({0} : Finset (Fin 8)) =
        W.g (Real.cos θ) := by
      rw [W.eq]
      simp [twoBranchSignal]
      change W.g ‖Complex.cos (θ : ℂ)‖ = W.g (Real.cos θ)
      rw [norm_complex_cos_of_real_of_nonneg hcos_pos.le]
    calc
      W.g (Real.cos θ)
          = μ (twoBranchSignal rot) ({0} : Finset (Fin 8)) := hμ.symm
      _ = P_cos rot := hcal rot
      _ = (Real.cos θ) ^ 2 := by
        rw [P_cos_eq]
        rfl
  have hval : ∀ r : ℝ, 0 < r → r < 1 → W.g r = r ^ 2 :=
    born_weight_forced W.g hg
  have hg0 : W.g 0 = 0 := by
    have hθ0 : 0 < Real.pi / 4 := by linarith [Real.pi_pos]
    have hθhalf : Real.pi / 4 < Real.pi / 2 := by linarith [Real.pi_pos]
    let rot45 : TwoBranchRotation :=
      { θ_s := Real.pi / 4
        θ_s_bounds := ⟨hθ0, hθhalf⟩
        T := 1
        T_pos := one_pos }
    have hnorm45 := hnorm (twoBranchSignal rot45) (twoBranchSignal_normalized rot45)
    rw [W.eq] at hnorm45
    have hcos_pos : 0 < Real.cos rot45.θ_s :=
      cos_pos_on_Ioo_zero_half_pi rot45.θ_s_bounds.1 rot45.θ_s_bounds.2
    have hsin_pos : 0 < Real.sin rot45.θ_s :=
      sin_pos_on_Ioo_zero_half_pi rot45.θ_s_bounds.1 rot45.θ_s_bounds.2
    have hsum :
        W.g (Real.cos rot45.θ_s) + W.g (Real.sin rot45.θ_s) +
              W.g 0 + W.g 0 + W.g 0 + W.g 0 + W.g 0 + W.g 0 = 1 := by
      have h1 : (1 : Fin 8) ≠ 0 := by decide
      have h2 : (2 : Fin 8) ≠ 0 := by decide
      have h21 : (2 : Fin 8) ≠ 1 := by decide
      have h3 : (3 : Fin 8) ≠ 0 := by decide
      have h31 : (3 : Fin 8) ≠ 1 := by decide
      have h4 : (4 : Fin 8) ≠ 0 := by decide
      have h41 : (4 : Fin 8) ≠ 1 := by decide
      have h5 : (5 : Fin 8) ≠ 0 := by decide
      have h51 : (5 : Fin 8) ≠ 1 := by decide
      have h6 : (6 : Fin 8) ≠ 0 := by decide
      have h61 : (6 : Fin 8) ≠ 1 := by decide
      have h7 : (7 : Fin 8) ≠ 0 := by decide
      have h71 : (7 : Fin 8) ≠ 1 := by decide
      simpa [twoBranchSignal, Fin.sum_univ_eight,
             norm_complex_cos_of_real_of_nonneg hcos_pos.le,
             norm_complex_sin_of_real_of_nonneg hsin_pos.le,
             h1, h2, h21, h3, h31, h4, h41,
             h5, h51, h6, h61, h7, h71] using hnorm45
    have hcos_lt : Real.cos rot45.θ_s < 1 :=
      cos_lt_one_on_Ioo_zero_half_pi rot45.θ_s_bounds.1 rot45.θ_s_bounds.2
    have hsin_lt : Real.sin rot45.θ_s < 1 :=
      sin_lt_one_on_Ioo_zero_half_pi rot45.θ_s_bounds.1 rot45.θ_s_bounds.2
    have hcos_val := hval (Real.cos rot45.θ_s) hcos_pos hcos_lt
    have hsin_val := hval (Real.sin rot45.θ_s) hsin_pos hsin_lt
    rw [hcos_val, hsin_val] at hsum
    nlinarith [Real.sin_sq_add_cos_sq rot45.θ_s]
  have hg1 : W.g 1 = 1 := by
    let basis0 : Signal8 := fun k => if k = (0 : Fin 8) then (1 : ℂ) else 0
    have hbasis : IsNormalized basis0 := by
      unfold IsNormalized basis0
      have h1 : (1 : Fin 8) ≠ 0 := by decide
      have h2 : (2 : Fin 8) ≠ 0 := by decide
      have h3 : (3 : Fin 8) ≠ 0 := by decide
      have h4 : (4 : Fin 8) ≠ 0 := by decide
      have h5 : (5 : Fin 8) ≠ 0 := by decide
      have h6 : (6 : Fin 8) ≠ 0 := by decide
      have h7 : (7 : Fin 8) ≠ 0 := by decide
      simp [Fin.sum_univ_eight, h1, h2, h3, h4, h5, h6, h7]
    have hnorm_basis := hnorm basis0 hbasis
    rw [W.eq] at hnorm_basis
    have hsum :
        W.g 1 + W.g 0 + W.g 0 + W.g 0 +
              W.g 0 + W.g 0 + W.g 0 + W.g 0 = 1 := by
      have h1 : (1 : Fin 8) ≠ 0 := by decide
      have h2 : (2 : Fin 8) ≠ 0 := by decide
      have h3 : (3 : Fin 8) ≠ 0 := by decide
      have h4 : (4 : Fin 8) ≠ 0 := by decide
      have h5 : (5 : Fin 8) ≠ 0 := by decide
      have h6 : (6 : Fin 8) ≠ 0 := by decide
      have h7 : (7 : Fin 8) ≠ 0 := by decide
      simpa [basis0, Fin.sum_univ_eight, h1, h2, h3, h4, h5, h6, h7]
        using hnorm_basis
    rw [hg0] at hsum
    linarith
  intro ψ hψ S
  rw [W.eq]
  unfold sectorMeasure
  refine Finset.sum_congr rfl ?_
  intro k _hk
  have hnon : 0 ≤ ‖ψ k‖ := norm_nonneg _
  have hle : ‖ψ k‖ ≤ 1 := signal_norm_le_one ψ hψ k
  by_cases hzero : ‖ψ k‖ = 0
  · simp [hzero, hg0]
  by_cases hone : ‖ψ k‖ = 1
  · simp [hone, hg1]
  have hpos : 0 < ‖ψ k‖ := lt_of_le_of_ne hnon (Ne.symm hzero)
  have hlt : ‖ψ k‖ < 1 := lt_of_le_of_ne hle hone
  exact hval ‖ψ k‖ hpos hlt
THEOREM born_weight_forced · IndisputableMonolith/Foundation/BornRuleForcing.lean
born_weight_forced · IndisputableMonolith/Foundation/BornRuleForcing.lean:189 
/-- **Scalar forcing**: Any weight function calibrated by the two-branch
    Born rule must be r ↦ r².

    For any r ∈ (0,1), let θ = arccos r.  Then cos θ = r and the
    calibration hypothesis gives w(r) = w(cos θ) = cos²θ = r². -/
theorem born_weight_forced (w : ℝ → ℝ)
    (hw : ∀ θ : ℝ, 0 < θ → θ < Real.pi / 2 →
          w (Real.cos θ) = (Real.cos θ) ^ 2) :
    ∀ r : ℝ, 0 < r → r < 1 → w r = r ^ 2 := by
  intro r hr0 hr1
  have hr_le : r ≤ 1 := le_of_lt hr1
  have hcos : Real.cos (Real.arccos r) = r :=
    Real.cos_arccos (by linarith) hr_le
  have hθ_pos : 0 < Real.arccos r := by
    unfold Real.arccos
    have := Real.arcsin_lt_pi_div_two.mpr hr1
    linarith
  have hθ_lt : Real.arccos r < Real.pi / 2 := by
    unfold Real.arccos
    have := Real.arcsin_pos.mpr hr0
    linarith
  calc w r = w (Real.cos (Real.arccos r)) := by rw [hcos]
    _ = (Real.cos (Real.arccos r)) ^ 2 := hw _ hθ_pos hθ_lt
    _ = r ^ 2 := by rw [hcos]
THEOREM sectorMeasure · IndisputableMonolith/Foundation/BornRuleForcing.lean
sectorMeasure · IndisputableMonolith/Foundation/BornRuleForcing.lean:56 
/-- The sector measure assigns to each mode-set S the sum of ‖ψ_k‖²
    over k ∈ S.  This is the Born-rule probability for the sector. -/
def sectorMeasure (ψ : Signal8) (S : Finset (Fin 8)) : ℝ :=
  ∑ k ∈ S, ‖ψ k‖ ^ 2
THEOREM contextualMeasure_ne_born · IndisputableMonolith/Foundation/BornRuleForcing.lean
contextualMeasure_ne_born · IndisputableMonolith/Foundation/BornRuleForcing.lean:656 
theorem contextualMeasure_ne_born :
    contextualMeasure hybridWitness {0} ≠ sectorMeasure hybridWitness {0} := by
  rw [contextualMeasure_hybridWitness_zero, sectorMeasure_hybridWitness_zero]
  norm_num

What this page does not claim

The Born rule is proven to be true in the physical world. The four conditions are themselves derived from more fundamental principles in this module. The framework's derivation is the only possible derivation 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/Foundation/BornRuleForcing.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