CommonQuotientExamples.lean

1 import MachineTheory.DiscrepancyClosure
2 import Mathlib.Tactic.NormNum
3 
4 /-!
5 # Exact examples and hypothesis boundaries for Core 2.4
6 
7 These examples instantiate the actual linear maps and word executor. They
8 separate invisible hidden dynamics, delayed observable return, one-initial-state
9 agreement, the reference-candidate premise and the absence of inverse recovery.
10 -/
11 namespace Komorebi.MachineTheory.CommonQuotient.Examples
12 
13 noncomputable section
14 
15 abbrev V2 := ℚ × ℚ
16 abbrev V3 := ℚ × (ℚ × ℚ)
17 
18 def first3 : V3 →ₗ[ℚ] ℚ := LinearMap.fst ℚ ℚ (ℚ × ℚ)
19 def second3 : V3 →ₗ[ℚ] ℚ := (LinearMap.fst ℚ ℚ ℚ).comp (LinearMap.snd ℚ ℚ (ℚ × ℚ))
20 def third3 : V3 →ₗ[ℚ] ℚ := (LinearMap.snd ℚ ℚ ℚ).comp (LinearMap.snd ℚ ℚ (ℚ × ℚ))
21 def keepTwo : V3 →ₗ[ℚ] V2 := first3.prod second3
22 
23 def visibleUpdate : V2 →ₗ[ℚ] V2 :=
24   ((LinearMap.fst ℚ ℚ ℚ) + (LinearMap.snd ℚ ℚ ℚ)).prod (LinearMap.snd ℚ ℚ ℚ)
25 
26 /-- The source's hidden third coordinate changes with the candidate. -/
27 def goodFamily (θ : Bool) (_ : Unit) : V3 →ₗ[ℚ] V3 :=
28   (first3 + second3).prod (second3.prod ((if θ then (2 : ℚ) else 3) • third3))
29 
30 /-- The real two-coordinate model, rather than an assumed quotient interface. -/
31 def goodModel : CommonModel goodFamily first3 where
32   Carrier := V2
33   addGroup := inferInstance
34   module := inferInstance
35   projection := keepTwo
36   onto := by
37     intro z
38     exact ⟨(z.1, (z.2, 0)), rfl⟩
39   update := fun _ => visibleUpdate
40   readout := LinearMap.fst ℚ ℚ ℚ
41   intertwines := by intro θ a; apply LinearMap.ext; intro v; rfl
42   reads := rfl
43 
44 /-- All initial vectors and all words agree, despite distinct full-state operators. -/
45 theorem good_agreement : ObservableAgreement goodFamily false first3 :=
46   commonModel_agreement goodFamily false first3 goodModel
47 
48 /-- Candidate changes at every operation preserve the protected visible result. -/
49 theorem good_switching (w : List (Bool × Unit)) (v : V3) :
50     first3 (switchedMap goodFamily w v) = first3 (wordMap (goodFamily false) (w.map Prod.snd) v) :=
51   switching_output goodFamily false first3 good_agreement w v
52 
53 /-- The candidate operators themselves have not been identified. -/
54 theorem good_candidates_differ : goodFamily true () ≠ goodFamily false () := by
55   intro h
56   have hh := congrArg third3 (LinearMap.congr_fun h (0, (0, 1)))
57   norm_num [goodFamily, first3, second3, third3] at hh
58 
59 /-- A protected output does not require reconstructing the hidden coordinate. -/
60 theorem good_projection_not_injective : ¬ Function.Injective keepTwo := by
61   intro h
62   have hv : ((0, (0, 0)) : V3) = ((0, (0, 1)) : V3) :=
63     h (a₁ := (0, (0, 0))) (a₂ := (0, (0, 1))) rfl
64   have hh := congrArg (fun v : V3 => v.2.2) hv
65   norm_num at hh
66 
67 /-- The canonical subspace is unchanged by choosing the other actual reference. -/
68 theorem good_reference_independent : discrepancy goodFamily false = discrepancy goodFamily true :=
69   discrepancy_reference_independent goodFamily false true
70 
71 /-- The constructed finite sequence, not an assumed limit, reaches the discrepancy space. -/
72 theorem good_finite_closure : stage goodFamily false (Module.finrank ℚ V3) = discrepancy goodFamily false :=
73   stage_finrank_eq goodFamily false
74 
75 /-- Immediate invisibility need not survive one subsequent reference action. -/
76 def first2 : V2 →ₗ[ℚ] ℚ := LinearMap.fst ℚ ℚ ℚ
77 def shift2 : V2 →ₗ[ℚ] V2 := (LinearMap.snd ℚ ℚ ℚ).prod (0 : V2 →ₗ[ℚ] ℚ)
78 def swap2 : V2 →ₗ[ℚ] V2 := (LinearMap.snd ℚ ℚ ℚ).prod (LinearMap.fst ℚ ℚ ℚ)
79 def returnFamily (θ : Bool) (_ : Unit) : V2 →ₗ[ℚ] V2 := if θ then swap2 else shift2
80 
81 /-- Every one-step discrepancy is invisible under the protected readout. -/
82 theorem immediate_invisible (θ : Bool) (a : Unit) :
83     first2.comp (returnFamily θ a - returnFamily false a) = 0 := by
84   cases θ <;> apply LinearMap.ext <;> intro v <;>
85     simp [returnFamily, shift2, swap2, first2]
86 
87 /-- But two steps reveal a difference. -/
88 theorem delayed_return :
89     first2 (wordMap (returnFamily true) [(), ()] (1, 0)) = 1 ∧
90     first2 (wordMap (returnFamily false) [(), ()] (1, 0)) = 0 := by
91   norm_num [wordMap, returnFamily, shift2, swap2, first2]
92 
93 /-- The universal agreement assertion fails in the immediate-invisibility example. -/
94 theorem no_agreement_from_immediate_invisibility : ¬ ObservableAgreement returnFamily false first2 := by
95   intro h
96   have hh := LinearMap.congr_fun (h true [(), ()]) (1, 0)
97   norm_num [wordMap, returnFamily, shift2, swap2, first2] at hh
98 
99 /-- Consequently the propagated space, unlike its unpropagated seed, is not invisible. -/
100 theorem propagated_visible : ¬ discrepancy returnFamily false ≤ LinearMap.ker first2 := by
101   intro h
102   exact no_agreement_from_immediate_invisibility
103     (agreement_of_discrepancy_invisible returnFamily false first2 h)
104 
105 /-- A concrete propagated difference produces unit protected output. -/
106 theorem propagated_difference_value :
107     first2 (returnFamily false () ((returnFamily true () - returnFamily false ()) (1, 0))) = 1 := by
108   norm_num [returnFamily, shift2, swap2, first2]
109 
110 /-- Two nilpotent candidate dynamics agree at one initial state, but not as operators. -/
111 def move12 : V3 →ₗ[ℚ] V3 := (0 : V3 →ₗ[ℚ] ℚ).prod (first3.prod (0 : V3 →ₗ[ℚ] ℚ))
112 def move23 : V3 →ₗ[ℚ] V3 := (0 : V3 →ₗ[ℚ] ℚ).prod ((0 : V3 →ₗ[ℚ] ℚ).prod second3)
113 def initialFamily (θ : Bool) (_ : Unit) : V3 →ₗ[ℚ] V3 := if θ then move23 else move12
114 def initialVector : V3 := (1, (0, 0))
115 
116 /-- Each fixed candidate has zero output on every word from this one initial vector. -/
117 theorem fixed_initial_output (θ : Bool) (w : List Unit) :
118     third3 (wordMap (initialFamily θ) w initialVector) = 0 := by
119   cases θ <;> cases w with
120   | nil => rfl
121   | cons a w =>
122     cases w with
123     | nil => rfl
124     | cons b w =>
125       change third3 (wordMap _ w (0 : V3)) = 0
126       rw [map_zero, map_zero]
127 
128 /-- Initial-state agreement genuinely holds for both fixed candidate systems. -/
129 theorem one_initial_agreement (θ : Bool) (w : List Unit) :
130     third3 (wordMap (initialFamily θ) w initialVector) =
131       third3 (wordMap (initialFamily false) w initialVector) := by
132   rw [fixed_initial_output, fixed_initial_output]
133 
134 /-- Switching first to move12 and then move23 reveals a protected unit. -/
135 theorem switched_initial_output :
136     third3 (switchedMap initialFamily [(false, ()), (true, ())] initialVector) = 1 := rfl
137 
138 /-- Action/candidate order matters: the reversed execution gives zero. -/
139 theorem switched_reverse_output :
140     third3 (switchedMap initialFamily [(true, ()), (false, ())] initialVector) = 0 := rfl
141 
142 /-- The all-initial-vector condition cannot be replaced by agreement at one vector. -/
143 theorem one_initial_is_not_enough : ¬ ObservableAgreement initialFamily false third3 := by
144   intro h
145   have hs := switching_output initialFamily false third3 h
146     [(false, ()), (true, ())] initialVector
147   rw [switched_initial_output, fixed_initial_output] at hs
148   norm_num at hs
149 
150 /-- A common model for supplied candidates says nothing about an unrelated reference family. -/
151 theorem unrelated_reference_fails :
152     (LinearMap.id : ℚ →ₗ[ℚ] ℚ).comp (wordMap (fun _ : Unit => LinearMap.id) [()]) ≠
153       (LinearMap.id : ℚ →ₗ[ℚ] ℚ).comp (wordMap (fun _ : Unit => 0) [()]) := by
154   intro h
155   have hh := LinearMap.congr_fun h 1
156   norm_num [wordMap] at hh
157 
158 /-- Equal candidate dynamics produce no discrepancy, including the empty action boundary. -/
159 theorem identical_candidates_zero {K V A Θ : Type*} [Field K] [AddCommGroup V] [Module K V]
160     (F : A → V →ₗ[K] V) (θ₀ : Θ) : discrepancy (fun _ : Θ => F) θ₀ = ⊥ := by
161   apply le_antisymm _ bot_le
162   apply discrepancy_le
163   · intro θ a v
164     simp only [sub_self, LinearMap.zero_apply, Submodule.zero_mem]
165   · intro a x hx
166     have hx0 : x = 0 := hx
167     rw [hx0, map_zero]
168     exact Submodule.zero_mem _
169 
170 end
171 end Komorebi.MachineTheory.CommonQuotient.Examples

Back to source controls