Examples.lean

1 import KomorebiLSM.Polynomial
2 import KomorebiLSM.LinearRefinement
3 import KomorebiLSM.MemoryBounds
4 import Mathlib.Tactic.NormNum
5 
6 /-! Exact examples and hypothesis-boundary counterexamples.
7 All assertions are ordinary kernel-checked proofs, not native execution.
8 -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.Examples
11 
12 abbrev V := ℚ × ℚ
13 
14 def retainFirst : V →ₗ[ℚ] V where
15   toFun x := (x.1, 0)
16   map_add' := by intro x y; ext <;> simp
17   map_smul' := by intro a x; ext <;> simp
18 
19 def swap : V →ₗ[ℚ] V where
20   toFun x := (x.2, x.1)
21   map_add' := by intro x y; rfl
22   map_smul' := by intro a x; rfl
23 
24 theorem retain_idempotent (x : V) : retainFirst (retainFirst x) = retainFirst x := rfl
25 
26 theorem preserved_signal_need_not_close :
27     ¬ FiberConstant retainFirst (fun x => retainFirst (swap x)) := by
28   intro h
29   have hbad := congrArg Prod.fst (h (0,0) (0,1) rfl)
30   norm_num [retainFirst, swap] at hbad
31 
32 theorem full_two_steps_return : retainFirst (swap (swap (1,0))) = (1,0) := rfl
33 
34 theorem separately_compressed_steps_lose_return :
35     retainFirst (swap (retainFirst (swap (retainFirst (1,0))))) = (0,0) := rfl
36 
37 theorem return_defect_is_nonzero : closureDefect retainFirst swap ≠ 0 := by
38   intro h
39   have hx := congrArg (fun f : V →ₗ[ℚ] V => (f (0,1)).1) h
40   norm_num [closureDefect, unresolved, retainFirst, swap] at hx
41 
42 /-- An arbitrary ambient redundant vector need not be fixed by consistency projection. -/
43 def redundantArchive : Realization ℚ V where
44   analysis x := (x,x)
45   synthesis c := c.1
46   reconstruct _ := rfl
47 
48 theorem redundant_not_all_consistent : ¬ redundantArchive.Consistent (0,1) := by
49   rintro ⟨x, hx⟩
50   have h0 := congrArg Prod.fst hx
51   have h1 := congrArg Prod.snd hx
52   simp only [redundantArchive] at h0 h1
53   norm_num [h0] at h1
54 
55 theorem redundant_projection_changes_vector :
56     redundantArchive.projector (0,1) = (0,0) := rfl
57 
58 theorem strict_refinement_has_no_initializer :
59     ¬ ∃ J : ℚ → V, ∀ x : V, J x.1 = x := by
60   apply no_factor_of_witness (fun x : V => x.1) (fun x : V => x) (0,0) (0,1) rfl
61   intro h
62   have hh := congrArg Prod.snd h
63   norm_num at hh
64 
65 theorem independent_squares_are_not_the_square_of_sum :
66     ((1:ℚ)+1)^2 ≠ (1:ℚ)^2 + 1^2 := by norm_num
67 
68 theorem cross_packet_term (x y : ℚ) : (x+y)^2 = x^2 + 2*x*y + y^2 := by ring
69 
70 /-- The exact two-coordinate system in the frozen manuscript. -/
71 def signalStep : V →ₗ[ℚ] V where
72   toFun x := ((1/2)*x.1+x.2, (1/4)*x.1+(1/3)*x.2)
73   map_add' := by intro x y; ext <;> simp <;> ring
74   map_smul' := by intro a x; ext <;> simp <;> ring
75 
76 theorem manuscript_first_step : signalStep (1,0) = (1/2,1/4) := by
77   norm_num [signalStep]
78 
79 theorem manuscript_second_step : signalStep (signalStep (1,0)) = (1/2,5/24) := by
80   norm_num [signalStep]
81 
82 theorem manuscript_third_observation : (signalStep (signalStep (signalStep (1,0)))).1 = 11/24 := by
83   norm_num [signalStep]
84 
85 theorem manuscript_omitted_return :
86     (retainFirst (signalStep (signalStep (1,0)))).1 -
87       (retainFirst (signalStep (retainFirst (signalStep (1,0))))).1 = 1/4 := by
88   norm_num [retainFirst, signalStep]
89 
90 end Komorebi.LSM.Examples

Back to source controls