Block10Examples.lean

1 import KomorebiLSM.RationalCertificateSoundness
2 
3 /-! Exact examples and failures for P45. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Block10Examples
6 open scoped BigOperators
7 open RationalSearch
8 
9 def oneCertificate : Candidate 1 1 := ⟨1,1,(fun _ => 1),(fun _ => 1),1⟩
10 def zeroBranchCertificate : Candidate 1 2 :=
11   ⟨1,1,(fun t => if t = 0 then 1 else 0),(fun _ => 1),1⟩
12 def signedCertificate : Candidate 1 1 := ⟨1,1,(fun _ => -1),(fun _ => 1),1⟩
13 def singularCertificate : Candidate 2 1 := ⟨1,(fun _ _ => 1),(fun _ => 1),(fun _ => 1),0⟩
14 
15 theorem one_certificate_valid : Valid (fun _ => 1) (fun _ => 1) (fun _ => 1) oneCertificate := by
16   unfold oneCertificate Valid synthesis lifts initial rightInverse
17   dsimp only
18   norm_num [Matrix.mul_apply,Matrix.mulVec,dotProduct,Matrix.one_apply,
19     funext_iff,Fin.forall_fin_one,Fin.forall_fin_two]
20 
21 theorem zero_branch_certificate_valid : Valid (fun _ => 1) (fun _ => 1)
22     (fun t => if t = 0 then 1 else 0) zeroBranchCertificate := by
23   unfold zeroBranchCertificate Valid synthesis lifts initial rightInverse
24   dsimp only
25   norm_num [Matrix.mul_apply,Matrix.mulVec,dotProduct,Matrix.one_apply,
26     funext_iff,Fin.forall_fin_one,Fin.forall_fin_two]
27 
28 theorem signed_lift_rejected : ¬ Valid (fun _ => 1) (fun _ => 1) (fun _ => -1) signedCertificate := by
29   unfold signedCertificate Valid synthesis lifts initial rightInverse
30   dsimp only
31   norm_num [Matrix.mul_apply,Matrix.mulVec,dotProduct,Matrix.one_apply,
32     funext_iff,Fin.forall_fin_one,Fin.forall_fin_two]
33 
34 theorem singular_generators_rejected : ¬ Valid (fun i => if i = 0 then 1 else 0)
35     (fun _ => 1) (fun _ => 1) singularCertificate := by
36   unfold singularCertificate Valid synthesis lifts initial rightInverse
37   dsimp only
38   norm_num [Matrix.mul_apply,Matrix.mulVec,dotProduct,Matrix.one_apply,
39     funext_iff,Fin.forall_fin_one,Fin.forall_fin_two]
40   intro h
41   have hh := congrFun (congrFun h 0) 0
42   change (∑ _k : Fin 1, (1 : ℚ) * 0) = 1 at hh
43   norm_num at hh
44 
45 theorem exact_checker_finds_encoded : checkCode (fun _ => 1) (fun _ => 1) (fun _ => 1)
46     (Encodable.encode oneCertificate) = some oneCertificate :=
47   checkCode_encode _ _ _ _ one_certificate_valid
48 
49 theorem bounded_failure_not_impossibility :
50     search (fun _ => 1) (fun _ => 1) (fun _ => 1) 0 = (none : Option (Candidate 1 1)) ∧
51     ∃ c : Candidate 1 1, Valid (fun _ => 1) (fun _ => 1) (fun _ => 1) c :=
52   ⟨rfl,oneCertificate,one_certificate_valid⟩
53 
54 theorem rational_boundary_solution :
55     ∃ q : Fin 2 → ℚ, (∀ j, 0 ≤ q j) ∧ q 0 = 0 ∧ q 1 = 1 := by
56   refine ⟨![0,1],?_,rfl,rfl⟩
57   intro j
58   fin_cases j <;> norm_num
59 
60 /-- Exact mass alone does not establish branch positivity. -/
61 theorem mass_without_positivity :
62     (2 : ℚ) + (-1) = 1 ∧ ¬ 0 ≤ (-1 : ℚ) := by norm_num
63 
64 end Komorebi.LSM.Block10Examples

Back to source controls