Publication.lean

1 import Conventions
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 2000000
5 open scoped Matrix BigOperators
6 namespace Komorebi.QuantumArithmetic
7 
8 /-- The exact root sum and the rational signal are the same indexed vector. -/
9 theorem exact_phase_signal_lookup (i : Index) :
10     ramanujanC12 i.val = cRat (ramanujan12.getD i.val 0) := by
11   decide +kernel +revert
12 
13 /-- The essay's phase sum is the actual complex Ramanujan signal, not only a coordinate table. -/
14 theorem complex_ramanujan_signal (i : Index) :
15     ((unitResidues12.map (fun a =>
16       Complex.exp (((Real.pi / 6 : ℝ) : ℂ) * Complex.I) ^ (a * i.val))).sum) =
17       (ramanujan12.getD i.val 0 : ℂ) := by
18   have h := congrArg interpret (exact_phase_signal_lookup i)
19   simpa [ramanujanC12, List.map_map, Function.comp_def, root_is_exponential] using h
20 
21 /-- The replacement state really takes the absolute value of the real signal. -/
22 theorem absolute_signal_lookup (i : Index) :
23     absRamanujan12.getD i.val 0 = |ramanujan12.getD i.val 0| := by
24   decide +kernel +revert
25 
26 /-- Exact orthogonality behind the numerical energy identity in the example. -/
27 theorem retained_discarded_orthogonal : dot ramanujan12 noise12 = 0 := by
28   decide +kernel +revert
29 
30 theorem signal_decomposition : vecAdd ramanujan12 noise12 = testSignal12 := by
31   decide +kernel +revert
32 
33 /-- Every signal is reconstructible from the retained and discarded components together. -/
34 theorem projector_residual_reconstructs (v : Index → ℂ) :
35     P.mulVec v + (1 - P).mulVec v = v := by
36   rw [Matrix.sub_mulVec, Matrix.one_mulVec]
37   exact add_sub_cancel _ _
38 
39 /-- No state reconstruction function can invert the initial probability histogram on both states. -/
40 theorem no_reconstruction_from_initial_probabilities :
41     ¬ ∃ R : (Index → ℝ) → (Index → ℂ),
42       R (fun i => Complex.normSq (psi i)) = psi ∧
43       R (fun i => Complex.normSq (chi i)) = chi := by
44   rintro ⟨R, hpsi, hchi⟩
45   have heq : (fun i => Complex.normSq (psi i)) =
46       (fun i => Complex.normSq (chi i)) := funext same_initial_probabilities
47   have hstate : psi = chi := by rw [← hpsi, ← hchi, heq]
48   have h := signed_state_recovers_arithmetic
49   rw [hstate, unsigned_state_erases_arithmetic] at h
50   norm_num at h
51 
52 /-- Exact probabilities in the recovered basis, connected to the normalized state. -/
53 theorem recovered_probability_at (i : Index) :
54     Complex.normSq (Fᴴ.mulVec psi i) =
55       if Nat.gcd i.val 12 = 1 then (1/4 : ℝ) else 0 := by
56   rw [state_recovery, unitState_entry_formula]
57   by_cases h : Nat.gcd i.val 12 = 1 <;> norm_num [h, Complex.normSq_apply]
58 
59 /-- The operator is not injective. Its nonzero normalized kernel state is explicit. -/
60 theorem projector_not_injective : ¬ Function.Injective P.mulVec := by
61   intro h
62   have hz : chi = 0 := h (by simp [projector_kills_chi])
63   have hp := chi_normalized
64   rw [hz] at hp
65   norm_num [totalProbability] at hp
66 
67 /-- Publication theorem gathering the complex identities stated in the worked example. -/
68 theorem publication_bridge :
69     Fᴴ * F = 1 ∧ F * Fᴴ = 1 ∧ F * D * Fᴴ = P ∧
70     P * P = P ∧ Pᴴ = P ∧ F.mulVec unitState = psi ∧
71     Fᴴ.mulVec psi = unitState ∧ totalProbability psi = 1 ∧
72     totalProbability chi = 1 ∧
73     (∀ i, Complex.normSq (psi i) = Complex.normSq (chi i)) ∧
74     (∑ i, star (psi i) * chi i) = 0 ∧
75     coprimeProbability (Fᴴ.mulVec psi) = 1 ∧
76     coprimeProbability (Fᴴ.mulVec chi) = 0 := by
77   exact ⟨fourier_unitary_left, fourier_unitary_right, projector_transport,
78     projector_idempotent_complex, projector_selfAdjoint_complex, state_preparation,
79     state_recovery, psi_normalized, chi_normalized, same_initial_probabilities,
80     states_orthogonal, signed_state_recovers_arithmetic, unsigned_state_erases_arithmetic⟩
81 
82 end Komorebi.QuantumArithmetic

Back to source controls