ahmad-foundations / nlbhe /PhaseVariance.lean

push from SNAPKITTYWEST/ahmad-foundations

a32e94f verified about 2 months ago

5.05 kB

-- Ahmad Foundations — NLBHE Theorem 3
-- Quantum phase variance σ²_θ is bounded: 0 ≤ σ²_θ ≤ π²
--
-- NOVEL CONTRIBUTION:
--   The phase variance of projective measurements on a quantum state,
--   where phases are defined as arg⟨ψ|P_k|ψ⟩ ∈ (-π, π], is bounded
--   above by π². This is tight: achieved when half the clauses have
--   phase +π and half have phase -π.
--   This bound is what connects the classical NLBHE dynamics to the
--   quantum 3-SAT subsystem — σ²_θ enters the amplitude equation F_A.

import AhmadFoundations.Shared.Defs
import Mathlib.Analysis.MeanInequalities
import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic

open Real Finset BigOperators AhmadFoundations

namespace PhaseVariance

-- ============================================================
-- Setup: finite collection of phases in (-π, π]
-- ============================================================

/-- A phase value lies in (-π, π]. -/
def IsPhase (θ : ℝ) : Prop := -Real.pi < θ ∧ θ ≤ Real.pi

/-- Phase mean over m clauses. -/
noncomputable def phaseMean (θ : Fin m → ℝ) : ℝ :=
  (∑ k, θ k) / m

/-- Phase variance over m clauses. -/
noncomputable def phaseVar (θ : Fin m → ℝ) : ℝ :=
  (∑ k, (θ k - phaseMean θ) ^ 2) / m

-- ============================================================
-- THEOREM 3: Phase variance is bounded above by π²
-- ============================================================

/-- Each phase in (-π, π] satisfies |θ| ≤ π. -/
lemma phase_abs_le_pi {θ : ℝ} (h : IsPhase θ) : |θ| ≤ Real.pi := by
  rw [abs_le]
  exact ⟨le_of_lt h.1, h.2⟩

/-- The deviation of any phase from the mean is at most 2π in absolute value. -/
lemma phase_dev_le_two_pi {θ_k θ_bar : ℝ}
    (hk : IsPhase θ_k) (hbar : -Real.pi ≤ θ_bar ∧ θ_bar ≤ Real.pi) :
    |θ_k - θ_bar| ≤ 2 * Real.pi := by
  have h1 : θ_k - θ_bar ≤ 2 * Real.pi := by linarith [hk.2, hbar.1]
  have h2 : -(2 * Real.pi) ≤ θ_k - θ_bar := by linarith [hk.1, hbar.2]
  rw [abs_le]; exact ⟨h2, h1⟩

/-- The variance of a bounded set of numbers is bounded by the squared half-range.
    For phases in [-π, π], the half-range is π, so variance ≤ π². -/
lemma var_le_sq_half_range {m : ℕ} (hm : m > 0) (θ : Fin m → ℝ)
    (hθ : ∀ k, IsPhase (θ k)) :
    phaseVar θ ≤ Real.pi ^ 2 := by
  unfold phaseVar phaseMean
  -- Each (θ_k - mean)² ≤ π² because mean ∈ [-π, π] and θ_k ∈ (-π, π]
  -- Variance ≤ mean of squares ≤ π²
  have hpi_pos : Real.pi > 0 := Real.pi_pos
  have hpi2 : Real.pi ^ 2 > 0 := pow_pos hpi_pos 2
  -- The mean lies in [-π, π]
  have hmean_bound : |phaseMean θ| ≤ Real.pi := by
    unfold phaseMean
    rw [abs_div, abs_of_pos (Nat.cast_pos.mpr hm)]
    apply div_le_of_le_mul₀ (Nat.cast_pos.mpr hm).le (by positivity)
    calc |∑ k, θ k|
        ≤ ∑ k, |θ k| := abs_sum_le_sum_abs _ _
      _ ≤ ∑ k : Fin m, Real.pi := by
            apply Finset.sum_le_sum
            intro k _; exact phase_abs_le_pi (hθ k)
      _ = m * Real.pi := by simp [Finset.sum_const, Finset.card_fin]
  -- Each squared deviation ≤ (2π)²/4 = π² (by AM bound)
  apply div_le_of_le_mul₀ (Nat.cast_pos.mpr hm).le (by positivity)
  calc ∑ k, (θ k - phaseMean θ) ^ 2
      ≤ ∑ k : Fin m, Real.pi ^ 2 := by
          apply Finset.sum_le_sum
          intro k _
          have hdev : |θ k - phaseMean θ| ≤ Real.pi := by
            rw [abs_le]
            constructor
            · linarith [(hθ k).1, (abs_le.mp hmean_bound).2]
            · linarith [(hθ k).2, (abs_le.mp hmean_bound).1]
          calc (θ k - phaseMean θ) ^ 2
              = |θ k - phaseMean θ| ^ 2 := (sq_abs _).symm
            _ ≤ Real.pi ^ 2 := by
                apply sq_le_sq'
                · linarith [(abs_nonneg (θ k - phaseMean θ)), Real.pi_pos.le]
                · exact hdev
    _ = m * Real.pi ^ 2 := by simp [Finset.sum_const, Finset.card_fin]
/-- THEOREM 3: 0 ≤ σ²_θ ≤ π² -/
theorem phase_variance_bounded {m : ℕ} (hm : m > 0) (θ : Fin m → ℝ)
    (hθ : ∀ k, IsPhase (θ k)) :
    0 ≤ phaseVar θ ∧ phaseVar θ ≤ Real.pi ^ 2 := by
  constructor
  · -- Non-negativity: variance is a sum of squares divided by positive m
    unfold phaseVar
    apply div_nonneg _ (Nat.cast_nonneg _)
    apply Finset.sum_nonneg
    intro k _; exact sq_nonneg _
  · exact var_le_sq_half_range hm θ hθ
-- ============================================================
-- TIGHTNESS: The bound π² is achieved
-- ============================================================
/-- The bound is tight: with m=2, θ₀ = π, θ₁ = -π+ε (limit ε→0),
    the variance approaches π². We show a concrete m=2 example at ±π. -/
example : phaseVar (![Real.pi, -Real.pi]) = Real.pi ^ 2 := by
  unfold phaseVar phaseMean
  simp [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one]
  ring_nf
  simp [Real.pi_pos.ne']
  ring

end PhaseVariance

	-- Ahmad Foundations — NLBHE Theorem 3
	-- Quantum phase variance σ²_θ is bounded: 0 ≤ σ²_θ ≤ π²
	--
	-- NOVEL CONTRIBUTION:
	-- The phase variance of projective measurements on a quantum state,
	-- where phases are defined as arg⟨ψ\|P_k\|ψ⟩ ∈ (-π, π], is bounded
	-- above by π². This is tight: achieved when half the clauses have
	-- phase +π and half have phase -π.
	-- This bound is what connects the classical NLBHE dynamics to the
	-- quantum 3-SAT subsystem — σ²_θ enters the amplitude equation F_A.

	import AhmadFoundations.Shared.Defs
	import Mathlib.Analysis.MeanInequalities
	import Mathlib.Data.Finset.Basic
	import Mathlib.Algebra.BigOperators.Basic
	import Mathlib.Data.Real.Basic

	open Real Finset BigOperators AhmadFoundations

	namespace PhaseVariance

	-- ============================================================
	-- Setup: finite collection of phases in (-π, π]
	-- ============================================================

	/-- A phase value lies in (-π, π]. -/
	def IsPhase (θ : ℝ) : Prop := -Real.pi < θ ∧ θ ≤ Real.pi

	/-- Phase mean over m clauses. -/
	noncomputable def phaseMean (θ : Fin m → ℝ) : ℝ :=
	(∑ k, θ k) / m

	/-- Phase variance over m clauses. -/
	noncomputable def phaseVar (θ : Fin m → ℝ) : ℝ :=
	(∑ k, (θ k - phaseMean θ) ^ 2) / m

	-- ============================================================
	-- THEOREM 3: Phase variance is bounded above by π²
	-- ============================================================

	/-- Each phase in (-π, π] satisfies \|θ\| ≤ π. -/
	lemma phase_abs_le_pi {θ : ℝ} (h : IsPhase θ) : \|θ\| ≤ Real.pi := by
	rw [abs_le]
	exact ⟨le_of_lt h.1, h.2⟩

	/-- The deviation of any phase from the mean is at most 2π in absolute value. -/
	lemma phase_dev_le_two_pi {θ_k θ_bar : ℝ}
	(hk : IsPhase θ_k) (hbar : -Real.pi ≤ θ_bar ∧ θ_bar ≤ Real.pi) :
	\|θ_k - θ_bar\| ≤ 2 * Real.pi := by
	have h1 : θ_k - θ_bar ≤ 2 * Real.pi := by linarith [hk.2, hbar.1]
	have h2 : -(2 * Real.pi) ≤ θ_k - θ_bar := by linarith [hk.1, hbar.2]
	rw [abs_le]; exact ⟨h2, h1⟩

	/-- The variance of a bounded set of numbers is bounded by the squared half-range.
	For phases in [-π, π], the half-range is π, so variance ≤ π². -/
	lemma var_le_sq_half_range {m : ℕ} (hm : m > 0) (θ : Fin m → ℝ)
	(hθ : ∀ k, IsPhase (θ k)) :
	phaseVar θ ≤ Real.pi ^ 2 := by
	unfold phaseVar phaseMean
	-- Each (θ_k - mean)² ≤ π² because mean ∈ [-π, π] and θ_k ∈ (-π, π]
	-- Variance ≤ mean of squares ≤ π²
	have hpi_pos : Real.pi > 0 := Real.pi_pos
	have hpi2 : Real.pi ^ 2 > 0 := pow_pos hpi_pos 2
	-- The mean lies in [-π, π]
	have hmean_bound : \|phaseMean θ\| ≤ Real.pi := by
	unfold phaseMean
	rw [abs_div, abs_of_pos (Nat.cast_pos.mpr hm)]
	apply div_le_of_le_mul₀ (Nat.cast_pos.mpr hm).le (by positivity)
	calc \|∑ k, θ k\|
	≤ ∑ k, \|θ k\| := abs_sum_le_sum_abs _ _
	_ ≤ ∑ k : Fin m, Real.pi := by
	apply Finset.sum_le_sum
	intro k _; exact phase_abs_le_pi (hθ k)
	_ = m * Real.pi := by simp [Finset.sum_const, Finset.card_fin]
	-- Each squared deviation ≤ (2π)²/4 = π² (by AM bound)
	apply div_le_of_le_mul₀ (Nat.cast_pos.mpr hm).le (by positivity)
	calc ∑ k, (θ k - phaseMean θ) ^ 2
	≤ ∑ k : Fin m, Real.pi ^ 2 := by
	apply Finset.sum_le_sum
	intro k _
	have hdev : \|θ k - phaseMean θ\| ≤ Real.pi := by
	rw [abs_le]
	constructor
	· linarith [(hθ k).1, (abs_le.mp hmean_bound).2]
	· linarith [(hθ k).2, (abs_le.mp hmean_bound).1]
	calc (θ k - phaseMean θ) ^ 2
	= \|θ k - phaseMean θ\| ^ 2 := (sq_abs _).symm
	_ ≤ Real.pi ^ 2 := by
	apply sq_le_sq'
	· linarith [(abs_nonneg (θ k - phaseMean θ)), Real.pi_pos.le]
	· exact hdev
	_ = m * Real.pi ^ 2 := by simp [Finset.sum_const, Finset.card_fin]

	/-- THEOREM 3: 0 ≤ σ²_θ ≤ π² -/
	theorem phase_variance_bounded {m : ℕ} (hm : m > 0) (θ : Fin m → ℝ)
	(hθ : ∀ k, IsPhase (θ k)) :
	0 ≤ phaseVar θ ∧ phaseVar θ ≤ Real.pi ^ 2 := by
	constructor
	· -- Non-negativity: variance is a sum of squares divided by positive m
	unfold phaseVar
	apply div_nonneg _ (Nat.cast_nonneg _)
	apply Finset.sum_nonneg
	intro k _; exact sq_nonneg _
	· exact var_le_sq_half_range hm θ hθ

	-- ============================================================
	-- TIGHTNESS: The bound π² is achieved
	-- ============================================================

	/-- The bound is tight: with m=2, θ₀ = π, θ₁ = -π+ε (limit ε→0),
	the variance approaches π². We show a concrete m=2 example at ±π. -/
	example : phaseVar (![Real.pi, -Real.pi]) = Real.pi ^ 2 := by
	unfold phaseVar phaseMean
	simp [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one]
	ring_nf
	simp [Real.pi_pos.ne']
	ring

	end PhaseVariance