BoundaryExamples.lean

1 import PaperXI.GeneralChain
2 import PaperXI.ChainSharpness
3 import PaperXI.ScalarCovariance
4 import PaperXI.FourierCovariance
5 import PaperXI.HolonomyResidual
6 
7 set_option autoImplicit false
8 namespace PaperXI.BoundaryExamples
9 open PaperXI.MonodromyChain
10 
11 theorem empty_chain : (shift (K := ℚ) (W := ℚ) (m := 0) (fun _ => 1)) ^ 0 = 0 :=
12   nilpotent_bound _
13 
14 theorem singleton_chain : (shift (K := ℚ) (W := ℚ) (m := 1) (fun _ => 1)) ^ 1 = 0 :=
15   nilpotent_bound _
16 
17 theorem length_three_square_nonzero :
18     (shift (K := ℚ) (W := ℚ) (m := 3) (fun _ => 1)) ^ 2 ≠ 0 :=
19   identity_shift_power_ne_zero (by decide)
20 
21 theorem length_three_cube_zero :
22     (shift (K := ℚ) (W := ℚ) (m := 3) (fun _ => 1)) ^ 3 = 0 := nilpotent_bound _
23 
24 theorem inverse_two_mod_five : (2 : ZMod 5)⁻¹ = 3 := by
25   exact ZMod.inv_eq_of_mul_eq_one 5 2 3 (by decide)
26 theorem inverse_label_differs : (2 : ZMod 5)⁻¹ ≠ 2 := by
27   rw [inverse_two_mod_five]
28   decide
29 
30 end PaperXI.BoundaryExamples

Back to source controls