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

ARTICLE 3 claims 3 theorems

Foundation Born Rule Forcing Norm Complex Sin Of Real Of Nonneg

A small formal lemma about the sine function, and the role it plays in a larger proof about measurement.

Verify this page

The helper lemma

The declaration norm_complex_sin_of_real_of_nonneg is a small, private lemma inside a larger formal proof. It states a fact about the sine function: if a real number θ has a nonnegative sine, then the complex absolute value of the complex sine of θ equals that real sine. In symbols, for 0 ≤ sin θ, one has |sin(θ + 0i)| = sin θ. The lemma is a helper, not a standalone result; it exists to simplify a step in a proof about probability measures.

The proof of the lemma is direct. It rewrites the complex sine of a real number as the real sine, using the standard embedding of real numbers into complex numbers, and then applies the fact that the absolute value of a nonnegative real number is the number itself. The declaration is marked private, meaning it is not intended for use outside the file in which it is defined.

The lemma appears in the context of a theorem about the Born rule, the quantum-mechanical rule that the probability of an outcome is the squared magnitude of the corresponding amplitude. In the Recognition Science framework, this rule is not assumed but derived from conditions on a measure over eight discrete modes. The lemma about the sine function is a technical ingredient in that derivation, used to handle a specific case involving a two-branch rotation.

The lemma does not claim anything about the Born rule itself, about the physical meaning of sine or cosine, or about any empirical prediction. It is a piece of pure mathematics, a fact about complex analysis, that the framework's machine-checked library uses as a stepping stone. Its role is confined to the formal proof; it has no independent physical content.

THEOREM norm_complex_sin_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean
norm_complex_sin_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean:276 
private theorem norm_complex_sin_of_real_of_nonneg {θ : ℝ}
    (h : 0 ≤ Real.sin θ) : ‖Complex.sin (θ : ℂ)‖ = Real.sin θ := by
  rw [← Complex.ofReal_sin]
  exact Complex.norm_of_nonneg h
THEOREM norm_complex_sin_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean
norm_complex_sin_of_real_of_nonneg · IndisputableMonolith/Foundation/BornRuleForcing.lean:276 
private theorem norm_complex_sin_of_real_of_nonneg {θ : ℝ}
    (h : 0 ≤ Real.sin θ) : ‖Complex.sin (θ : ℂ)‖ = Real.sin θ := by
  rw [← Complex.ofReal_sin]
  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

What this page does not claim

The lemma does not assert any physical law or empirical fact. The lemma does not prove the Born rule; it is only a technical step in a larger proof. The lemma does not make any claim about the physical interpretation of sine or cosine.

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