Encyclopedia Foundation Foundation Born Rule Forcing Contextual Measure Phase Invariant

ARTICLE 3 claims 3 theorems

Foundation Born Rule Forcing Contextual Measure Phase Invariant

A theorem in the Recognition Science framework shows that the standard quantum probability rule, the Born rule, is the only possible choice once a few plain conditions are fixed.

Verify this page

The forced probability rule

The Born rule is the recipe quantum mechanics uses to turn a wavefunction into a probability. For a state made of eight discrete modes, it says the chance of finding the system in a particular set of modes is the sum of the squared magnitudes of the mode coefficients. The rule is normally taken as an axiom, a starting point that is not derived from anything deeper. The Recognition Science framework contains a machine-checked proof that this rule is forced, not chosen, once four conditions are imposed on any candidate probability measure.

The four conditions are plain. The measure must assign total probability one to a normalized state. It must be phase-invariant, meaning it depends only on the magnitude of each mode coefficient, not on its complex phase. It must be additive over disjoint sets of modes. And it must agree with a two-branch calibration, a simple two-mode case where the probability is known to be the squared cosine or sine of an angle. The theorem proves that any measure meeting these conditions is exactly the squared-magnitude sum. The result holds in the frequency basis as well, by Parseval's identity, so the same rule survives a Fourier transform.

The proof is not a single leap. A key lemma shows that a weight function that equals the square of the cosine on a small interval must equal the square everywhere on the unit interval. Another lemma shows that a local measure, one that assigns probability to a set by summing a function of each mode's magnitude, is uniquely the squared-magnitude rule. The final theorem packages these together. The framework's library of formal theorems checks every step, so the result carries the weight of a machine-verified proof.

What the declaration does not claim is just as important. The theorem does not say that the squared-magnitude rule is the only measure that is normalized, phase-invariant, and additive. It says that if you also demand consistency with the two-branch Born rule, then the squared-magnitude rule is the unique choice. The theorem also does not claim that the Born rule is derived from nothing. It is derived from four explicit conditions, and the proof shows that those conditions are enough. The framework's own contextual measure, which differs from the Born rule for states with more than two occupied modes, is a separate definition, not a counterexample to this theorem.

The consequence is that the Born rule, a key part of quantum theory, is not an arbitrary postulate in this framework. It is the inevitable outcome of a small set of structural requirements. This turns a rule that is usually accepted on empirical grounds into a theorem that follows from the framework's own logic. The reader can now see the Born rule as a forced consequence, not a mysterious given.

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 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

What this page does not claim

The theorem does not derive the Born rule from nothing; it derives it from four explicit conditions. The theorem does not apply to the framework's contextual measure, which differs for states with more than two occupied modes. The theorem does not claim the Born rule is the only normalized, phase-invariant, additive measure without the two-branch consistency condition.

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