RationalCertificateSearch.lean

1 import KomorebiLSM.RationalFeasibility
2 import Mathlib.Logic.Encodable.Pi
3 import Mathlib.Data.Rat.Encodable
4 
5 /-! P45: executable exhaustive rational certificate enumeration. A rational right
6 inverse witnesses full row rank; all other checks are rational equalities or signs.
7 The finite-fuel interface is resumable by increasing fuel and makes no negative
8 existence claim. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.RationalSearch
11 open scoped BigOperators
12 
13 /-- Width, synthesis, branch lifts, initial coefficients and a right inverse. -/
14 abbrev Candidate (r s : ℕ) := Σ m : ℕ,
15   (Matrix (Fin r) (Fin m) ℚ ×
16    (Fin s → Matrix (Fin m) (Fin m) ℚ) ×
17    (Fin m → ℚ) × Matrix (Fin m) (Fin r) ℚ)
18 
19 instance candidateEncodable (r s : ℕ) : Encodable (Candidate r s) := by
20   unfold Candidate Matrix
21   infer_instance
22 
23 def synthesis {r s : ℕ} (c : Candidate r s) := c.2.1
24 def lifts {r s : ℕ} (c : Candidate r s) := c.2.2.1
25 def initial {r s : ℕ} (c : Candidate r s) := c.2.2.2.1
26 def rightInverse {r s : ℕ} (c : Candidate r s) := c.2.2.2.2
27 
28 instance rationalLE (a b : ℚ) : Decidable (a ≤ b) :=
29   inferInstanceAs (Decidable (b.blt a = false))
30 
31 instance rationalMatrixDecidableEq (n m : ℕ) : DecidableEq (Matrix (Fin n) (Fin m) ℚ) :=
32   inferInstanceAs (DecidableEq (Fin n → Fin m → ℚ))
33 
34 /-- Every condition is finite and decidable over exact rationals. -/
35 def Valid {r s : ℕ} (l z : Fin r → ℚ) (B : Fin s → Matrix (Fin r) (Fin r) ℚ)
36     (c : Candidate r s) : Prop :=
37   (∀ j, ∑ i, l i * synthesis c i j = 1) ∧
38   synthesis c * rightInverse c = 1 ∧
39   (∀ t, B t * synthesis c = synthesis c * lifts c t) ∧
40   (∀ t i j, 0 ≤ lifts c t i j) ∧
41   (∀ j, 0 ≤ initial c j) ∧
42   (∑ j, initial c j) = 1 ∧
43   (synthesis c).mulVec (initial c) = z
44 
45 instance validDecidable {r s : ℕ} (l z : Fin r → ℚ)
46     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s) : Decidable (Valid l z B c) :=
47 by
48   rcases c with ⟨m,V,A,alpha,R⟩
49   unfold Valid synthesis lifts initial rightInverse
50   dsimp only
51   letI : ∀ t i j, Decidable (0 ≤ A t i j) := fun t i j => rationalLE 0 (A t i j)
52   letI : ∀ j, Decidable (0 ≤ alpha j) := fun j => rationalLE 0 (alpha j)
53   infer_instance
54 
55 /-- Decode one natural number and check the entire witness exactly. -/
56 def checkCode {r s : ℕ} (l z : Fin r → ℚ) (B : Fin s → Matrix (Fin r) (Fin r) ℚ)
57     (k : ℕ) : Option (Candidate r s) :=
58   (Encodable.decode k).filter (fun c => decide (Valid l z B c))
59 
60 /-- Exhaustive dovetailing over widths and every rational entry. -/
61 def search {r s : ℕ} (l z : Fin r → ℚ) (B : Fin s → Matrix (Fin r) (Fin r) ℚ) :
62     ℕ → Option (Candidate r s)
63   | 0 => none
64   | n+1 => (search l z B n).or (checkCode l z B n)
65 
66 theorem checkCode_sound {r s : ℕ} (l z : Fin r → ℚ)
67     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (k : ℕ) (c : Candidate r s)
68     (h : checkCode l z B k = some c) : Valid l z B c := by
69   unfold checkCode at h
70   cases hd : (Encodable.decode k : Option (Candidate r s)) with
71   | none => simp [hd] at h
72   | some d =>
73     simp [hd] at h
74     exact h.2
75 
76 theorem checkCode_encode {r s : ℕ} (l z : Fin r → ℚ)
77     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
78     (h : Valid l z B c) : checkCode l z B (Encodable.encode c) = some c := by
79   simp [checkCode,Encodable.encodek,h]
80 
81 theorem search_sound {r s : ℕ} (l z : Fin r → ℚ)
82     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (n : ℕ) (c : Candidate r s)
83     (h : search l z B n = some c) : Valid l z B c := by
84   induction n with
85   | zero => simp [search] at h
86   | succ n ih =>
87     cases hn : search l z B n with
88     | none => exact checkCode_sound l z B n c (by simpa [search,hn] using h)
89     | some d =>
90       have he : d = c := by simpa [search,hn] using h
91       subst d
92       exact ih hn
93 
94 theorem search_complete_rational {r s : ℕ} (l z : Fin r → ℚ)
95     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
96     (h : Valid l z B c) : ∃ d, search l z B (Encodable.encode c + 1) = some d := by
97   cases hn : search l z B (Encodable.encode c) with
98   | none => exact ⟨c, by simp [search,hn,checkCode_encode l z B c h]⟩
99   | some d => exact ⟨d, by simp [search,hn]⟩
100 
101 theorem search_persistent {r s : ℕ} (l z : Fin r → ℚ)
102     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (n k : ℕ) (c : Candidate r s)
103     (h : search l z B n = some c) : search l z B (n+k) = some c := by
104   induction k with
105   | zero => simpa using h
106   | succ k ih => simp [search,ih]
107 
108 /-- In the absence of a rational certificate every finite prefix returns none.
109 No bounded prefix is promoted to a proof of absence. -/
110 theorem search_no_certificate {r s : ℕ} (l z : Fin r → ℚ)
111     (B : Fin s → Matrix (Fin r) (Fin r) ℚ)
112     (h : ¬ ∃ c : Candidate r s, Valid l z B c) (n : ℕ) : search l z B n = none := by
113   cases he : search l z B n with
114   | none => rfl
115   | some c => exact False.elim (h ⟨c,search_sound l z B n c he⟩)
116 
117 /-- Exact model equations and signs over the real interpretation of the witness. -/
118 def realMatrix {n m : ℕ} (M : Matrix (Fin n) (Fin m) ℚ) : Matrix (Fin n) (Fin m) ℝ :=
119   fun i j => M i j
120 
121 theorem realMatrix_mul {n m k : ℕ} (M : Matrix (Fin n) (Fin m) ℚ)
122     (N : Matrix (Fin m) (Fin k) ℚ) : realMatrix (M*N) = realMatrix M * realMatrix N := by
123   ext i j
124   simp [realMatrix,Matrix.mul_apply]
125 
126 theorem realMatrix_one (n : ℕ) : realMatrix (1 : Matrix (Fin n) (Fin n) ℚ) = 1 := by
127   ext i j
128   simp [realMatrix,Matrix.one_apply,apply_ite]
129 
130 theorem real_synthesis_surjective {r s : ℕ} (l z : Fin r → ℚ)
131     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
132     (h : Valid l z B c) : Function.Surjective (realMatrix (synthesis c)).mulVecLin := by
133   intro x
134   refine ⟨(realMatrix (rightInverse c)).mulVec x, ?_⟩
135   change (realMatrix (synthesis c)).mulVec ((realMatrix (rightInverse c)).mulVec x) = x
136   rw [Matrix.mulVec_mulVec,← realMatrix_mul,h.2.1,realMatrix_one,Matrix.one_mulVec]
137 
138 /-- Real surjectivity of a rational synthesis yields an enumeratable rational
139 right inverse. This is not an extra rational-inverse hypothesis. -/
140 theorem rational_right_inverse {r m : ℕ} (V : Matrix (Fin r) (Fin m) ℚ)
141     (hv : Function.Surjective (realMatrix V).mulVecLin) :
142     ∃ R : Matrix (Fin m) (Fin r) ℚ, V * R = 1 := by
143   classical
144   have hc : ∀ j : Fin r, ∃ q : Fin m → ℚ, ∀ i,
145       ∑ k, V i k * q k = (1 : Matrix (Fin r) (Fin r) ℚ) i j := by
146     intro j
147     obtain ⟨x,hx⟩ := hv (fun i => (1 : Matrix (Fin r) (Fin r) ℝ) i j)
148     apply rational_solution m V (fun i => (1 : Matrix (Fin r) (Fin r) ℚ) i j) x
149     intro i
150     have := congrFun hx i
151     simpa [Matrix.mulVecLin_apply,Matrix.mulVec, dotProduct,realMatrix,Matrix.one_apply,apply_ite] using this
152   choose q hq using hc
153   refine ⟨fun k j => q j k, ?_⟩
154   ext i j
155   exact hq j i
156 
157 /-- The real witnesses in P39 can be rationalized while retaining the supplied
158 rational generator matrix, including all zero entries and boundary faces. -/
159 theorem rationalize_certificate {r s m : ℕ} (l z : Fin r → ℚ)
160     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (V : Matrix (Fin r) (Fin m) ℚ)
161     (hv : Function.Surjective (realMatrix V).mulVecLin)
162     (hn : ∀ j, ∑ i, l i * V i j = 1)
163     (A : Fin s → Matrix (Fin m) (Fin m) ℝ) (alpha : Fin m → ℝ)
164     (ha : ∀ t i j, 0 ≤ A t i j) (hpos : ∀ j, 0 ≤ alpha j)
165     (hinit : ∀ i, ∑ j, (V i j : ℝ) * alpha j = (z i : ℝ))
166     (hmass : ∑ j, alpha j = 1)
167     (hinter : ∀ t, realMatrix (B t) * realMatrix V = realMatrix V * A t) :
168     ∃ c : Candidate r s, Valid l z B c := by
169   classical
170   obtain ⟨R,hR⟩ := rational_right_inverse V hv
171   have hc : ∀ t j, ∃ q : Fin m → ℚ, (∀ k, 0 ≤ q k) ∧
172       (∀ i, ∑ k, V i k * q k = (B t * V) i j) := by
173     intro t j
174     apply rational_nonnegative_solution m V (fun i => (B t * V) i j)
175       (fun k => A t k j) (fun k => ha t k j)
176     intro i
177     have he := congrFun (congrFun (hinter t) i) j
178     have hr := congrFun (congrFun (realMatrix_mul (B t) V) i) j
179     exact he.symm.trans hr.symm
180   choose Aq hAq hEq using hc
181   let W : (Fin r ⊕ Unit) → Fin m → ℚ
182     | .inl i => V i
183     | .inr _ => fun _ => 1
184   let zz : (Fin r ⊕ Unit) → ℚ | .inl i => z i | .inr _ => 1
185   have heq : ∀ i, ∑ j, (W i j : ℝ) * alpha j = (zz i : ℝ) := by
186     intro i
187     cases i with
188     | inl i => exact hinit i
189     | inr _ => simpa [W,zz] using hmass
190   obtain ⟨q,hq,he⟩ := rational_nonnegative_solution m W zz alpha hpos heq
191   refine ⟨⟨m,V,(fun t i j => Aq t j i),q,R⟩,hn,hR,?_,?_,hq,?_,?_⟩
192   · intro t
193     ext i j
194     exact (hEq t j i).symm
195   · intro t i j
196     exact hAq t j i
197   · simpa [W,zz,initial] using he (.inr ())
198   · funext i
199     exact he (.inl i)
200 
201 /-- P45 conditional termination, with exactly the rational-generator hypothesis.
202 Real nonnegative lifts are converted by finite weak rational elimination. -/
203 theorem rational_finite_certificate_search {r s m : ℕ} (l z : Fin r → ℚ)
204     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (V : Matrix (Fin r) (Fin m) ℚ)
205     (hv : Function.Surjective (realMatrix V).mulVecLin)
206     (hn : ∀ j, ∑ i, l i * V i j = 1)
207     (A : Fin s → Matrix (Fin m) (Fin m) ℝ) (alpha : Fin m → ℝ)
208     (ha : ∀ t i j, 0 ≤ A t i j) (hpos : ∀ j, 0 ≤ alpha j)
209     (hinit : ∀ i, ∑ j, (V i j : ℝ) * alpha j = (z i : ℝ))
210     (hmass : ∑ j, alpha j = 1)
211     (hinter : ∀ t, realMatrix (B t) * realMatrix V = realMatrix V * A t) :
212     ∃ n c, search l z B n = some c ∧ Valid l z B c := by
213   obtain ⟨c,hc⟩ := rationalize_certificate l z B V hv hn A alpha ha hpos hinit hmass hinter
214   obtain ⟨d,hd⟩ := search_complete_rational l z B c hc
215   exact ⟨_,d,hd,search_sound l z B _ d hd⟩
216 
217 end Komorebi.LSM.RationalSearch

Back to source controls