JointReconstructionExamples.lean

1 import MachineTheory.JointReconstruction
2 import Mathlib.LinearAlgebra.Prod
3 import Mathlib.Algebra.Field.ZMod
4 import Mathlib.Algebra.CharP.Two
5 import Mathlib.Tactic.NormNum
6 
7 /-! # Exact binary joint reconstruction and its limits
8 
9 The source's two-dimensional state is `(b,s)` over `ZMod 2`. Sharing the
10 records `(b+s,s)` recovers both coordinates, including the calibration bit.
11 The separate three-dimensional example adds a distinct nuisance coordinate
12 `n`. This extra coordinate is invisible to both records, while `b` is still
13 recoverable. No communication or recipient execution cost is inferred.
14 -/
15 namespace Komorebi.MachineTheory.JointReconstructionExamples
16 noncomputable section
17 
18 abbrev F₂ := ZMod 2
19 abbrev State₂ := F₂ × F₂
20 
21 def physical₂ : State₂ →ₗ[F₂] F₂ := LinearMap.fst F₂ F₂ F₂
22 def calibration₂ : State₂ →ₗ[F₂] F₂ := LinearMap.snd F₂ F₂ F₂
23 def display₂ : State₂ →ₗ[F₂] F₂ := physical₂ + calibration₂
24 def joint₂ : State₂ →ₗ[F₂] State₂ := display₂.prod calibration₂
25 def decodeTarget : State₂ →ₗ[F₂] F₂ := physical₂ + calibration₂
26 def decodeState : State₂ →ₗ[F₂] State₂ := decodeTarget.prod calibration₂
27 
28 /-- The source's explicit inverse recovers the entire two-coordinate state. -/
29 theorem exact_binary_inverse : decodeState.comp joint₂ = LinearMap.id := by
30   apply LinearMap.ext
31   intro x
32   apply Prod.ext
33   · simp [decodeState, decodeTarget, joint₂, display₂, physical₂, calibration₂,
34       CharTwo.add_cancel_right]
35   · simp [decodeState, joint₂, calibration₂]
36 
37 theorem exact_binary_target : physical₂ = decodeTarget.comp joint₂ := by
38   apply LinearMap.ext
39   intro x
40   simp [decodeTarget, joint₂, display₂, physical₂, calibration₂,
41     CharTwo.add_cancel_right]
42 
43 theorem exact_binary_injective : Function.Injective joint₂ := by
44   intro x y h
45   have he := congrArg decodeState h
46   change (decodeState.comp joint₂) x = (decodeState.comp joint₂) y at he
47   simpa only [exact_binary_inverse, LinearMap.id_apply] using he
48 
49 /-- Agent A's accessible display cannot recover the target, even by a nonlinear function. -/
50 theorem display_alone_impossible :
51     ¬ ∃ D : F₂ → F₂, ∀ x, D (display₂ x) = physical₂ x := by
52   rintro ⟨D, hD⟩
53   have h0 := hD (0,0)
54   have h1 := hD (1,1)
55   norm_num [display₂, physical₂, calibration₂] at h0 h1
56   exact zero_ne_one (h0.symm.trans h1)
57 
58 /-- Agent B's accessible calibration also cannot recover the physical target. -/
59 theorem calibration_alone_impossible :
60     ¬ ∃ D : F₂ → F₂, ∀ x, D (calibration₂ x) = physical₂ x := by
61   rintro ⟨D, hD⟩
62   have h0 := hD (0,0)
63   have h1 := hD (1,0)
64   norm_num [physical₂, calibration₂] at h0 h1
65   exact zero_ne_one (h0.symm.trans h1)
66 
67 /-- The two kernels intersect trivially although each single record loses a direction. -/
68 theorem binary_kernel_intersection :
69     LinearMap.ker joint₂ = LinearMap.ker display₂ ⊓ LinearMap.ker calibration₂ ∧
70     LinearMap.ker joint₂ = ⊥ := by
71   constructor
72   · exact LinearMap.ker_prod display₂ calibration₂
73   · exact LinearMap.ker_eq_bot.mpr exact_binary_injective
74 
75 theorem lost_direction_is_removed :
76     (1,1) ∈ LinearMap.ker display₂ ∧ (1,1) ∉ LinearMap.ker joint₂ := by
77   norm_num [LinearMap.mem_ker, display₂, joint₂, physical₂, calibration₂]
78   decide
79 
80 abbrev State₃ := F₂ × (F₂ × F₂)
81 def physical₃ : State₃ →ₗ[F₂] F₂ := LinearMap.fst F₂ F₂ (F₂ × F₂)
82 def calibration₃ : State₃ →ₗ[F₂] F₂ :=
83   (LinearMap.fst F₂ F₂ F₂).comp (LinearMap.snd F₂ F₂ (F₂ × F₂))
84 def nuisance₃ : State₃ →ₗ[F₂] F₂ :=
85   (LinearMap.snd F₂ F₂ F₂).comp (LinearMap.snd F₂ F₂ (F₂ × F₂))
86 def display₃ : State₃ →ₗ[F₂] F₂ := physical₃ + calibration₃
87 def joint₃ : State₃ →ₗ[F₂] State₂ := display₃.prod calibration₃
88 
89 theorem extra_nuisance_target_reconstructed : physical₃ = decodeTarget.comp joint₃ := by
90   apply LinearMap.ext
91   intro x
92   simp [decodeTarget, joint₃, display₃, physical₃, calibration₃, physical₂,
93     calibration₂, CharTwo.add_cancel_right]
94 
95 theorem extra_nuisance_not_injective : ¬ Function.Injective joint₃ := by
96   intro h
97   have he := h (show joint₃ (0,0,0) = joint₃ (0,0,1) by
98     simp [joint₃, display₃, physical₃, calibration₃])
99   have hn := congrArg (fun x : State₃ => x.2.2) he
100   exact zero_ne_one hn
101 
102 /-- The general criterion certifies this target despite the unresolved extra dimension. -/
103 theorem extra_nuisance_kernel_condition :
104     LinearMap.ker joint₃ ≤ LinearMap.ker physical₃ :=
105   JointReconstruction.ker_le_of_decoder (K := F₂) joint₃ physical₃ decodeTarget
106     extra_nuisance_target_reconstructed
107 
108 theorem extra_nuisance_no_full_linear_decoder :
109     ¬ ∃ D : State₂ →ₗ[F₂] State₃, LinearMap.id = D.comp joint₃ := by
110   intro h
111   exact extra_nuisance_not_injective
112     ((JointReconstruction.full_state_iff_injective (K := F₂) joint₃).mp h)
113 
114 /-- Unlike the source's calibration bit, this additional nuisance remains unrecoverable. -/
115 theorem extra_nuisance_not_reconstructed :
116     ¬ ∃ D : State₂ → F₂, ∀ x, D (joint₃ x) = nuisance₃ x := by
117   rintro ⟨D, hD⟩
118   have h0 := hD (0,0,0)
119   have h1 := hD (0,0,1)
120   norm_num [joint₃, display₃, physical₃, calibration₃, nuisance₃] at h0 h1
121   exact zero_ne_one (h0.symm.trans h1)
122 
123 /-- A record with proper range still permits a total linear decoder. -/
124 def embeddedRecord : F₂ →ₗ[F₂] State₂ := (LinearMap.id : F₂ →ₗ[F₂] F₂).prod 0
125 def extension₀ : State₂ →ₗ[F₂] F₂ := physical₂
126 def extension₁ : State₂ →ₗ[F₂] F₂ := physical₂ + calibration₂
127 
128 theorem proper_range_extensions :
129     extension₀.comp embeddedRecord = LinearMap.id ∧
130     extension₁.comp embeddedRecord = LinearMap.id := by
131   constructor <;> apply LinearMap.ext <;> intro x <;>
132     simp [extension₀, extension₁, embeddedRecord, physical₂, calibration₂]
133 
134 theorem proper_range_not_surjective : ¬ Function.Surjective embeddedRecord := by
135   intro h
136   obtain ⟨x, hx⟩ := h (0,1)
137   have he := congrArg Prod.snd hx
138   norm_num [embeddedRecord] at he
139 
140 /-- Values outside the record range are unconstrained by the reconstruction identity. -/
141 theorem extensions_differ_outside_range : extension₀ ≠ extension₁ := by
142   intro h
143   have he := LinearMap.congr_fun h (0,1)
144   norm_num [extension₀, extension₁, physical₂, calibration₂] at he
145 
146 end
147 end Komorebi.MachineTheory.JointReconstructionExamples

Back to source controls