Encyclopedia Foundation Foundation Born Rule Forcing Norm Complex Cos Of Real Of Nonneg

ARTICLE 3 claims 3 theorems

Foundation Born Rule Forcing Norm Complex Cos Of Real Of Nonneg

A small lemma about complex numbers, the cosine bridge, is the hinge that lets a forced probability rule reach its final form.

Verify this page

The cosine bridge

The complex cosine of a real angle, when the angle's cosine is not negative, has a magnitude equal to that real cosine. This is a basic fact of complex analysis, and it is the content of the declaration norm_complex_cos_of_real_of_nonneg. The proof is short: the complex cosine of a real number is the same as the real cosine, and the magnitude of a nonnegative real number is the number itself. The declaration is a bridge lemma, a step in a larger argument, not a result about physics or measurement on its own.

The larger argument is the forcing of the Born rule. In the framework's machine-checked library of formal theorems, the rule that assigns probabilities to measurement outcomes is not assumed; it is derived from four conditions on a measure over eight signal modes. The measure must be normalized, so the total probability is one. It must be phase-invariant, depending only on the magnitudes of the mode amplitudes, not their phases. It must be additive over disjoint sets of modes. And it must agree with a two-branch calibration, where a signal split between two modes with amplitudes cos θ and sin θ receives probabilities cos²θ and sin²θ. The theorem modeLocal_born_unique proves that the only measure satisfying these conditions is the sum of squared magnitudes, the standard Born rule.

The cosine bridge enters at the calibration step. The two-branch condition is stated for the real cosine and sine of the angle. The proof needs to move from those real values to the magnitudes of the complex amplitudes used in the signal. The lemma norm_complex_cos_of_real_of_nonneg supplies that move for the cosine, and its sine counterpart supplies it for the sine. Without this bridge, the calibration condition could not be applied to the complex signal space, and the uniqueness proof would not close.

The declaration does not claim that the Born rule is the only possible probability rule in all contexts. The library also defines a contextual measure that switches to a fourth-power rule for signals with more than two occupied modes, and a theorem proves that this contextual measure differs from the Born rule on a specific witness signal. The uniqueness theorem applies only under its four stated conditions, and the cosine bridge is a lemma about complex numbers, not a statement about measurement. The bridge is a necessary hinge, but it is not the door.

THEOREM norm_complex_cos_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean
norm_complex_cos_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean:271 
private theorem norm_complex_cos_of_real_of_nonneg {θ : ℝ}
    (h : 0 ≤ Real.cos θ) : ‖Complex.cos (θ : ℂ)‖ = Real.cos θ := by
  rw [← Complex.ofReal_cos]
  exact Complex.norm_of_nonneg h
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 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 cosine bridge lemma alone does not establish the Born rule; it is one step in a larger proof. The uniqueness theorem does not apply to the contextual measure, which violates the additivity condition. The declaration does not claim that the Born rule is the only possible probability rule in all physical contexts.

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