Encyclopedia Foundation Foundation Born Rule Forcing Sector Measure Hybrid Witness Zero

ARTICLE 3 claims 3 theorems

Foundation Born Rule Forcing Sector Measure Hybrid Witness Zero

A machine-checked proof shows that the standard quantum probability rule is the only one that survives four plain conditions, and that a proposed alternative fails its own test.

Verify this page

The forced Born rule

The Born rule is the recipe quantum mechanics uses to turn a wave function into probabilities: the chance of finding a system in a particular state is the squared size of that state's amplitude. In 1926 Max Born introduced it, and it has survived a century of experiments. The Recognition Science framework contains a machine-checked library of formal theorems that derives this rule from a small set of assumptions about how a discrete record of events, its ledger, should behave.

The framework models a physical state as an eight-component signal, a list of eight complex numbers. A sector is a choice of some of those eight components. The question is how to assign a probability to each sector. The framework's central theorem, proved in its library, states that only one measure satisfies four conditions: it must assign total probability one to the whole set, it must ignore the phases of the components, it must add up over disjoint sets, and it must agree with the two-branch Born rule on simple two-component states. That unique measure is the squared norm of each component, summed over the sector, written μ(S) = Σ_{k∈S} ‖ψ_k‖².

The declaration named in the question, sectorMeasure_hybridWitness_zero, is a small but decisive piece of that proof. It concerns a specific eight-component state called the hybrid witness. The theorem computes the sector measure for the first component of that state: it equals one half. That number matters because the framework also defines an alternative measure, the contextual measure, which uses fourth powers of the amplitudes instead of squares. For the hybrid witness, the contextual measure assigns a different value to the first sector. The theorem contextualMeasure_ne_born proves that the two disagree. So the hybrid witness is a concrete counterexample: it satisfies the conditions that were meant to justify the fourth-power rule, but it fails to match the two-branch Born rule. The squared-norm measure survives; the alternative does not.

This is a result about the internal consistency of the framework's model. It does not claim to explain why the physical universe follows the Born rule, nor does it prove that the hybrid witness is a realizable physical state. It shows that within the framework's definitions, the standard rule is the only one that meets all four conditions, and it identifies a specific state that breaks a proposed rival. The proof is a theorem in the library, not an empirical measurement.

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 sectorMeasure_hybridWitness_zero · IndisputableMonolith/Foundation/BornRuleForcing.lean
sectorMeasure_hybridWitness_zero · IndisputableMonolith/Foundation/BornRuleForcing.lean:652 
private theorem sectorMeasure_hybridWitness_zero :
    sectorMeasure hybridWitness {0} = 1 / 2 := by
  simp [sectorMeasure, hybridWitness, Real.sq_sqrt]
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 proved for the physical universe, only for the framework's eight-component model. The hybrid witness state is physically realizable. The contextual measure is a viable alternative to 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