RepairExamples.lean

1 import KomorebiSpace.RepairProjection
2 import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Constructed and non-canonical examples
8 
9 The split model satisfies all correction hypotheses with rate zero and retains
10 an arbitrary nonzero semantic coordinate. A second model shows that preservation
11 of a nontrivial observable does not by itself make exact repairs unique.
12 -/
13 universe u v w
14 noncomputable section
15 namespace KomorebiSpace
16 namespace RepairExamples
17 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
18 variable (S : Type v) (R : Type w)
19 variable [NormedAddCommGroup S] [NormedSpace 𝕜 S]
20 variable [NormedAddCommGroup R] [NormedSpace 𝕜 R]
21 
22 def splitScheme : RepairDynamics.Scheme
23     (ContinuousLinearMap.snd 𝕜 S R) (ContinuousLinearMap.fst 𝕜 S R) where
24   correction := ContinuousLinearMap.inr 𝕜 S R
25   rate := 0
26   rate_nonneg := le_rfl
27   rate_lt_one := zero_lt_one
28   preserve _ := rfl
29   contract x := by simp
30 
31 /-- The actual iteration, not just its existential conclusion, repairs in one step. -/
32 theorem split_step (x : S × R) :
33     RepairDynamics.step (ContinuousLinearMap.snd 𝕜 S R)
34       (ContinuousLinearMap.inr 𝕜 S R) x = (x.1, 0) := by
35   ext <;> simp [RepairDynamics.step]
36 
37 variable [CompleteSpace S] [CompleteSpace R]
38 
39 /-- The constructed analytic projection agrees with the explicit split projection. -/
40 theorem split_projection (x : S × R) :
41     (splitScheme (𝕜 := 𝕜) S R).projection x = (x.1, 0) := by
42   apply Prod.ext
43   · exact (splitScheme (𝕜 := 𝕜) S R).limit_semantics x
44   · exact (splitScheme (𝕜 := 𝕜) S R).limit_exact x
45 
46 /-- Nonzero semantic information survives exactification in the model. -/
47 theorem split_nonzero (s : S) (hs : s ≠ 0) (r : R) :
48     (splitScheme (𝕜 := 𝕜) S R).projection (s,r) ≠ 0 := by
49   rw [split_projection]
50   intro h
51   exact hs (congrArg Prod.fst h)
52 
53 /-- Exactness and one nontrivial protected coordinate need not determine the result. -/
54 theorem semantics_alone_not_unique :
55     ∃ a b : ℝ × (ℝ × ℝ), a ≠ b ∧
56       a.2.2 = 0 ∧ b.2.2 = 0 ∧ a.1 = b.1 ∧ a.1 = 1 := by
57   refine ⟨(1,(0,0)), (1,(1,0)), ?_, rfl, rfl, rfl, rfl⟩
58   intro h
59   have h01 : (0 : ℝ) = 1 := congrArg (fun x : ℝ × (ℝ × ℝ) => x.2.1) h
60   exact zero_ne_one h01
61 
62 end RepairExamples
63 end KomorebiSpace
64 end

Back to source controls