RationalCertificateSoundness.lean

1 import KomorebiLSM.RationalCertificateSearch
2 import KomorebiLSM.PositiveLiftTopology
3 
4 /-! P45 soundness: accepted rational data instantiate the existing P39 cone and
5 positive-instrument theorem, not just a syntactic checker. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RationalSearch
8 open scoped BigOperators
9 open FiniteBayes FiniteInstruments PositiveLift
10 
11 noncomputable def readout {r : ℕ} (l : Fin r → ℚ) : (Fin r → ℝ) →ₗ[ℝ] ℝ where
12   toFun x := ∑ i, (l i : ℝ) * x i
13   map_add' x y := by simp [mul_add,Finset.sum_add_distrib]
14   map_smul' c x := by simp [Finset.mul_sum]; congr 1; funext i; ring
15 
16 theorem valid_normalized {r s : ℕ} (l z : Fin r → ℚ)
17     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
18     (h : Valid l z B c) :
19     (readout l).comp (realMatrix (synthesis c)).mulVecLin = mass := by
20   apply LinearMap.ext
21   intro x
22   simp only [LinearMap.comp_apply,readout,LinearMap.coe_mk,AddHom.coe_mk,
23     Matrix.mulVecLin_apply,Matrix.mulVec,dotProduct,realMatrix,mass_apply]
24   change (∑ i, (l i : ℝ) * ∑ j, (synthesis c i j : ℝ) * x j) = ∑ j, x j
25   simp_rw [Finset.mul_sum,← mul_assoc]
26   rw [Finset.sum_comm]
27   apply Finset.sum_congr rfl
28   intro j _
29   rw [← Finset.sum_mul]
30   have hn : ∑ i, (l i : ℝ) * (synthesis c i j : ℝ) = 1 := by exact_mod_cast h.1 j
31   rw [hn,one_mul]
32 
33 theorem valid_intertwining {r s : ℕ} (l z : Fin r → ℚ)
34     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
35     (h : Valid l z B c) (t : Fin s) :
36     (realMatrix (B t)).mulVecLin.comp (realMatrix (synthesis c)).mulVecLin =
37     (realMatrix (synthesis c)).mulVecLin.comp (realMatrix (lifts c t)).mulVecLin := by
38   rw [← Matrix.mulVecLin_mul,← Matrix.mulVecLin_mul,← realMatrix_mul,← realMatrix_mul,h.2.2.1 t]
39 
40 theorem valid_initial {r s : ℕ} (l z : Fin r → ℚ)
41     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (c : Candidate r s)
42     (h : Valid l z B c) :
43     IsPrior (fun j => (initial c j : ℝ)) ∧
44     (realMatrix (synthesis c)).mulVecLin (fun j => (initial c j : ℝ)) = fun i => (z i : ℝ) := by
45   refine ⟨⟨fun j => by
46     change (0 : ℝ) ≤ (initial c j : ℝ)
47     exact_mod_cast h.2.2.2.2.1 j, ?_⟩,?_⟩
48   · change (∑ j, (initial c j : ℝ)) = 1
49     exact_mod_cast h.2.2.2.2.2.1
50   · funext i
51     have he := congrFun h.2.2.2.2.2.2 i
52     change ∑ j, (synthesis c i j : ℝ) * (initial c j : ℝ) = (z i : ℝ)
53     exact_mod_cast he
54 
55 /-- An accepted certificate supplies a closed, pointed, generating invariant
56 cone containing the initial state, with normalized strictly positive mass. -/
57 theorem accepted_probability_domain {r s : ℕ} (l z : Fin r → ℚ)
58     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (n : ℕ) (c : Candidate r s)
59     (hs : search l z B n = some c) :
60     let V := (realMatrix (synthesis c)).mulVecLin
61     IsClosed (hull V) ∧ Submodule.span ℝ (hull V) = ⊤ ∧
62     PositivePackets.StrictMass (hull V) (readout l) ∧
63     (∀ x, x ∈ hull V → -x ∈ hull V → x = 0) ∧
64     ((fun i => (z i : ℝ)) ∈ hull V) ∧
65     (∀ t x, x ∈ hull V → (realMatrix (B t)).mulVecLin x ∈ hull V) := by
66   dsimp only
67   have h := search_sound l z B n c hs
68   have hn := valid_normalized l z B c h
69   have hi := valid_initial l z B c h
70   refine ⟨hull_closed _ _ hn,hull_spans _ (real_synthesis_surjective l z B c h),
71     hull_strict_mass _ _ hn,?_,?_,?_⟩
72   · intro x hx hmx
73     exact hull_pointed _ _ hn hx hmx
74   · exact ⟨_,hi.1.1,hi.2⟩
75   · intro t
76     apply (positive_lift_iff _ _).mpr
77     refine ⟨realMatrix (lifts c t),?_,valid_intertwining l z B c h t⟩
78     intro i j
79     change (0 : ℝ) ≤ (lifts c t i j : ℝ)
80     exact_mod_cast h.2.2.2.1 t i j
81 
82 /-- The rational per-action column identities imply the real functional mass
83 identity used by P39. -/
84 theorem rational_mass_identity {r s : ℕ} {A O : Type*} [Fintype O]
85     (code : A × O → Fin s) (l : Fin r → ℚ)
86     (B : Fin s → Matrix (Fin r) (Fin r) ℚ)
87     (hm : ∀ a j, ∑ o, ∑ i, l i * B (code (a,o)) i j = l j) :
88     ∀ a x, ∑ o, readout l ((realMatrix (B (code (a,o)))).mulVecLin x) = readout l x := by
89   intro a x
90   change (∑ o, ∑ i, (l i : ℝ) * ∑ j, (B (code (a,o)) i j : ℝ) * x j) =
91     ∑ j, (l j : ℝ) * x j
92   simp_rw [Finset.mul_sum,← mul_assoc]
93   conv_lhs => arg 2; ext o; rw [Finset.sum_comm]
94   rw [Finset.sum_comm]
95   apply Finset.sum_congr rfl
96   intro j _
97   simp_rw [← Finset.sum_mul]
98   have hh : ∑ o, ∑ i, (l i : ℝ) * (B (code (a,o)) i j : ℝ) = (l j : ℝ) := by
99     exact_mod_cast hm a j
100   rw [hh]
101 
102 /-- Exact mass identities turn every returned certificate into all-word
103 probabilities in [0,1], for any finite observation alphabet and action coding. -/
104 theorem accepted_all_word_probabilities {r s : ℕ} {A O : Type*} [Fintype O]
105     (code : A × O → Fin s) (l z : Fin r → ℚ)
106     (B : Fin s → Matrix (Fin r) (Fin r) ℚ) (n : ℕ) (c : Candidate r s)
107     (hs : search l z B n = some c)
108     (hm : ∀ a j, ∑ o, ∑ i, l i * B (code (a,o)) i j = l j) :
109     ∀ w : List (A × O),
110       0 ≤ readout l (wordAction (fun t => (realMatrix (B (code t))).mulVecLin) w
111         (fun i => (z i : ℝ))) ∧
112       readout l (wordAction (fun t => (realMatrix (B (code t))).mulVecLin) w
113         (fun i => (z i : ℝ))) ≤ 1 := by
114   have h := search_sound l z B n c hs
115   have hn := valid_normalized l z B c h
116   have hi := valid_initial l z B c h
117   have he := fun t => valid_intertwining l z B c h (code t)
118   have hp : ∀ t i j, 0 ≤ realMatrix (lifts c (code t)) i j := by
119     intro t i j
120     change (0 : ℝ) ≤ (lifts c (code t) i j : ℝ)
121     exact_mod_cast h.2.2.2.1 (code t) i j
122   have hh := finite_positive_lift_certificate
123     (fun t => (realMatrix (B (code t))).mulVecLin)
124     (realMatrix (synthesis c)).mulVecLin (readout l) hn (rational_mass_identity code l B hm)
125     (fun t => realMatrix (lifts c (code t))) he hp _ hi.1
126   rw [hi.2] at hh
127   exact hh.2.2
128 end Komorebi.LSM.RationalSearch

Back to source controls