Generated.lean

1 import ProofPath.Binary
2 
3 namespace ProofPath.Generated
4 open Matrix
5 
6 def one_bit_M : Matrix (Fin 2) (Fin 3) (ZMod 2) := ![![1, 1, 1], ![1, 0, 0]]
7 def one_bit_b : Fin 2 → ZMod 2 := ![0, 0]
8 theorem one_bit_positive : ∃ y, one_bit_M.mulVec y = one_bit_b := by
9   exact ⟨![0, 0, 0], by decide⟩
10 theorem one_bit_count : (Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
11     one_bit_M.mulVec y = one_bit_b)).card = 2 := by decide
12 def one_bit_Q : Matrix (Fin 1) (Fin 3) (ZMod 2) := ![![0, 1, 0]]
13 theorem one_bit_observations : ((Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
14     one_bit_M.mulVec y = one_bit_b)).image one_bit_Q.mulVec).card = 2 := by decide
15 
16 def incompatible_M : Matrix (Fin 3) (Fin 3) (ZMod 2) := ![![1, 1, 0], ![1, 0, 0], ![0, 1, 0]]
17 def incompatible_b : Fin 3 → ZMod 2 := ![0, 0, 1]
18 def incompatible_w : Fin 3 → ZMod 2 := ![1, 1, 1]
19 theorem incompatible_negative : ¬ ∃ y, incompatible_M.mulVec y = incompatible_b := by
20   exact row_witness_sound incompatible_M incompatible_b incompatible_w (by decide) (by decide)
21 
22 def redundant_M : Matrix (Fin 2) (Fin 3) (ZMod 2) := ![![1, 1, 0], ![0, 0, 0]]
23 def redundant_b : Fin 2 → ZMod 2 := ![0, 0]
24 theorem redundant_positive : ∃ y, redundant_M.mulVec y = redundant_b := by
25   exact ⟨![0, 0, 0], by decide⟩
26 theorem redundant_count : (Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
27     redundant_M.mulVec y = redundant_b)).card = 4 := by decide
28 def redundant_Q : Matrix (Fin 2) (Fin 3) (ZMod 2) := ![![0, 0, 1], ![0, 0, 1]]
29 theorem redundant_observations : ((Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
30     redundant_M.mulVec y = redundant_b)).image redundant_Q.mulVec).card = 2 := by decide
31 
32 def unique_M : Matrix (Fin 4) (Fin 3) (ZMod 2) := ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1], ![0, 0, 0]]
33 def unique_b : Fin 4 → ZMod 2 := ![0, 0, 0, 0]
34 theorem unique_positive : ∃ y, unique_M.mulVec y = unique_b := by
35   exact ⟨![0, 0, 0], by decide⟩
36 theorem unique_count : (Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
37     unique_M.mulVec y = unique_b)).card = 1 := by decide
38 def unique_Q : Matrix (Fin 1) (Fin 3) (ZMod 2) := ![![1, 1, 1]]
39 theorem unique_observations : ((Finset.univ.filter (fun y : Fin 3 → ZMod 2 =>
40     unique_M.mulVec y = unique_b)).image unique_Q.mulVec).card = 1 := by decide
41 
42 end ProofPath.Generated

Back to source controls