Conventions.lean

1 import SemanticBridge
2 import Mathlib.Tactic.FieldSimp
3 import Mathlib.Tactic.Positivity
4 
5 set_option autoImplicit false
6 set_option maxHeartbeats 2000000
7 open scoped Matrix BigOperators
8 namespace Komorebi.QuantumArithmetic
9 
10 /-- The coordinate root is exactly the usual exponential twelfth root. -/
11 theorem root_is_exponential :
12     interpret zeta12 = Complex.exp (((Real.pi / 6 : ℝ) : ℂ) * Complex.I) := by
13   rw [Complex.exp_mul_I]
14   rw [← Complex.ofReal_cos, ← Complex.ofReal_sin, Real.cos_pi_div_six, Real.sin_pi_div_six]
15   apply Complex.ext <;> simp [interpret, zeta12]
16   ring
17 
18 theorem root_power_twelve : interpret zeta12 ^ 12 = 1 := by
19   simpa using congrArg interpret zeta12_order_certificate
20 
21 theorem rootPower_interpret (n : Nat) :
22     interpret (rootPower n) = interpret zeta12 ^ n := by
23   simp only [rootPower, interpret_pow]
24   exact (pow_eq_pow_mod n root_power_twelve).symm
25 
26 theorem sqrt_twelve : Real.sqrt 12 = 2 * Real.sqrt 3 := by
27   calc
28     Real.sqrt 12 = Real.sqrt (4 * 3) := by norm_num
29     _ = Real.sqrt 4 * Real.sqrt 3 := Real.sqrt_mul (by norm_num) _
30     _ = 2 * Real.sqrt 3 := by
31       rw [show Real.sqrt 4 = 2 from by
32         rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num)]]
33 
34 theorem sqrt_fortyeight : Real.sqrt 48 = 4 * Real.sqrt 3 := by
35   calc
36     Real.sqrt 48 = Real.sqrt (16 * 3) := by norm_num
37     _ = Real.sqrt 16 * Real.sqrt 3 := Real.sqrt_mul (by norm_num) _
38     _ = 4 * Real.sqrt 3 := by
39       rw [show Real.sqrt 16 = 4 from by
40         rw [show (16 : ℝ) = 4^2 by norm_num, Real.sqrt_sq (by norm_num)]]
41 
42 theorem fourierScale_interpret :
43     interpret fourierScale = ((1 / Real.sqrt 12 : ℝ) : ℂ) := by
44   apply Complex.ext <;> simp [interpret, fourierScale, sqrt_twelve]
45   have h : Real.sqrt 3 ≠ 0 := by positivity
46   field_simp
47   nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]
48 
49 theorem stateScale_interpret :
50     interpret stateScale = ((1 / Real.sqrt 48 : ℝ) : ℂ) := by
51   apply Complex.ext <;> simp [interpret, stateScale, sqrt_fortyeight]
52   have h : Real.sqrt 3 ≠ 0 := by positivity
53   field_simp
54   nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]
55 
56 /-- The matrix checked in the certificate is the standard positive sign Fourier matrix. -/
57 theorem fourier_entry_formula (i j : Index) :
58     F i j = ((1 / Real.sqrt 12 : ℝ) : ℂ) *
59       Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (i.val : ℂ) * (j.val : ℂ) / 12) := by
60   simp only [F, complexMatrix, exactFourier, interpret_mul, fourierScale_interpret,
61     rootPower_interpret, root_is_exponential]
62   rw [← Complex.exp_nat_mul]
63   congr 2
64   push_cast
65   ring
66 
67 theorem psi_entry_formula (i : Index) :
68     psi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (ramanujan12.getD i.val 0 : ℂ) := by
69   simp [psi, complexVector, exactPsi, stateScale_interpret]
70 
71 theorem chi_entry_formula (i : Index) :
72     chi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (absRamanujan12.getD i.val 0 : ℂ) := by
73   simp [chi, complexVector, exactChi, stateScale_interpret]
74 
75 theorem unitState_entry_formula (i : Index) :
76     unitState i = if Nat.gcd i.val 12 = 1 then (1/2 : ℂ) else 0 := by
77   by_cases h : Nat.gcd i.val 12 = 1 <;>
78     simp [unitState, complexVector, exactUnitState, h]
79 
80 theorem projector_entry_formula (i j : Index) :
81     P i j = (ramanujan12.getD ((i.val + 12 - j.val) % 12) 0 : ℂ) / 12 := by
82   simp [P, complexMatrix, exactProjector]
83 
84 theorem selector_idempotent : D * D = D := by
85   unfold D
86   rw [Matrix.diagonal_mul_diagonal]
87   congr 1
88   funext i
89   by_cases h : Nat.gcd i.val 12 = 1 <;> simp [h]
90 
91 theorem selector_selfAdjoint : Dᴴ = D := by
92   ext i j
93   by_cases h : i = j
94   · subst j
95     simp [D, Matrix.conjTranspose_apply, apply_ite star]
96   · simp [D, Matrix.conjTranspose_apply, h, Ne.symm h]
97 
98 theorem projector_idempotent_complex : P * P = P := by
99   rw [← projector_transport]
100   calc
101     (F * D * Fᴴ) * (F * D * Fᴴ) = F * D * (Fᴴ * F) * D * Fᴴ := by
102       simp only [Matrix.mul_assoc]
103     _ = F * D * Fᴴ := by rw [fourier_unitary_left, Matrix.mul_one, Matrix.mul_assoc F D D,
104       selector_idempotent]
105 
106 theorem projector_selfAdjoint_complex : Pᴴ = P := by
107   rw [← projector_transport]
108   simp [Matrix.conjTranspose_mul, selector_selfAdjoint, Matrix.mul_assoc]
109 
110 /-- Projection alone loses information: two distinct normalized states are distinguished exactly. -/
111 theorem complete_phase_separation :
112     totalProbability psi = 1 ∧ totalProbability chi = 1 ∧
113     (∀ i, Complex.normSq (psi i) = Complex.normSq (chi i)) ∧
114     (∑ i, star (psi i) * chi i) = 0 ∧
115     coprimeProbability (Fᴴ.mulVec psi) = 1 ∧
116     coprimeProbability (Fᴴ.mulVec chi) = 0 := by
117   exact ⟨psi_normalized, chi_normalized, same_initial_probabilities, states_orthogonal,
118     signed_state_recovers_arithmetic, unsigned_state_erases_arithmetic⟩
119 
120 end Komorebi.QuantumArithmetic

Back to source controls