TraceExamples.lean

1 import PaperX.TraceRecovery
2 import PaperX.FiniteCharacters
3 import Mathlib.Data.ZMod.Basic
4 import Mathlib.LinearAlgebra.Matrix.Notation
5 import Mathlib.Tactic.Linarith
6 import Mathlib.Tactic.FinCases
7 import Mathlib.Tactic.NormNum
8 
9 /-! Explicit finite-image representation example and exact failure cases.
10 No numerical table is claimed to come from an unspecified arithmetic carrier. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperX.TraceExamples
14 
15 open scoped BigOperators Matrix
16 open PaperX.FiniteSeparation PaperX.TraceRecovery
17 
18 abbrev G := Multiplicative (ZMod 2 × ZMod 2)
19 
20 def chi (i : Fin 3) (g : G) : ℚ :=
21   if i = 0 then 1 else if i = 1 then
22     if g.toAdd.1 = 0 then 1 else -1
23   else if g.toAdd.2 = 0 then 1 else -1
24 
25 theorem chi_one : ∀ i, chi i 1 = 1 := by decide +kernel
26 
27 theorem chi_mul : ∀ i g h, chi i (g * h) = chi i g * chi i h := by decide +kernel
28 
29 def chiHom (i : Fin 3) : G →* ℚ where
30   toFun := chi i
31   map_one' := chi_one i
32   map_mul' := chi_mul i
33 
34 /-- Actual one-dimensional representations of the four-element group. -/
35 def rep (i : Fin 3) : Representation ℚ G (Fin 1 → ℚ) :=
36   ((algebraMap ℚ (Module.End ℚ (Fin 1 → ℚ))).toMonoidHom).comp (chiHom i)
37 
38 theorem rep_character (i : Fin 3) : (rep i).character = chi i := by
39   funext g
40   simp [Representation.character, rep, chiHom, Algebra.algebraMap_eq_smul_one,
41     LinearMap.trace_one]
42 
43 def samples : Fin 3 → G := ![Multiplicative.ofAdd (0,0),
44   Multiplicative.ofAdd (1,0), Multiplicative.ofAdd (0,1)]
45 
46 def separator : Matrix (Fin 3) (Fin 3) ℚ := !![1,1,1; 1,-1,1; 1,1,-1]
47 
48 theorem actual_trace_matrix : sampleMatrix (fun i => (rep i).character) samples = separator := by
49   simp_rw [rep_character]
50   decide +kernel
51 
52 theorem distinct_samples : Function.Injective samples := by decide +kernel
53 
54 theorem determinant_four : separator.det = 4 := by
55   rw [Matrix.det_fin_three]; decide +kernel
56 
57 theorem determinant_nonzero : separator.det ≠ 0 := by rw [determinant_four]; norm_num
58 
59 theorem actual_characters_independent :
60     LinearIndependent ℚ (fun i => (rep i).character) := by
61   apply independent_of_separator _ samples
62   rw [actual_trace_matrix]
63   exact determinant_nonzero
64 
65 def multiplicities : Fin 3 → ℕ := ![2,0,1]
66 def capacities : Fin 3 → ℕ := ![3,2,2]
67 def observed : Fin 3 → ℚ := ![3,3,1]
68 
69 theorem observed_trace : separator *ᵥ (fun i => (multiplicities i : ℚ)) = observed := by
70   decide +kernel
71 
72 theorem exact_recovery : recover separator observed = fun i => (multiplicities i : ℚ) := by
73   rw [← observed_trace, recover_trace separator determinant_nonzero]
74 
75 theorem multiplicities_admissible : Admissible capacities multiplicities := by unfold Admissible; decide +kernel
76 
77 theorem only_natural_solution (m : Fin 3 → ℕ)
78     (h : separator *ᵥ (fun i => (m i : ℚ)) = observed) : m = multiplicities := by
79   exact natural_multiplicity_unique separator determinant_nonzero m multiplicities
80     (h.trans observed_trace.symm)
81 
82 /-- One equation has a unique rational solution but no natural multiplicity solution. -/
83 def fractionalTrace : Fin 3 → ℚ := ![1/2,1/2,1/2]
84 
85 theorem fractional_solution : recover separator fractionalTrace = ![1/2,0,0] := by
86   have h : separator *ᵥ ![(1/2 : ℚ),0,0] = fractionalTrace := by decide +kernel
87   rw [← h, recover_trace separator determinant_nonzero]
88 
89 theorem fractional_not_natural : ¬ ∃ m : Fin 3 → ℕ,
90     separator *ᵥ (fun i => (m i : ℚ)) = fractionalTrace := by
91   rintro ⟨m, hm⟩
92   have he := congrArg (recover separator) hm
93   rw [recover_trace separator determinant_nonzero, fractional_solution] at he
94   have h0 := congrFun he 0
95   norm_num at h0
96   have h1 : (2 : ℚ) * (m 0 : ℚ) = 1 := by linarith
97   have h2 : 2 * m 0 = 1 := by exact_mod_cast h1
98   omega
99 
100 /-- Integer recovery alone does not check the stated carrier capacities. -/
101 def excessive : Fin 3 → ℕ := ![4,0,1]
102 
103 theorem excessive_not_admissible : ¬ Admissible capacities excessive := by unfold Admissible; decide +kernel
104 
105 theorem no_admissible_excessive_trace : ¬ ∃ m : Fin 3 → ℕ,
106     Admissible capacities m ∧
107     separator *ᵥ (fun i => (m i : ℚ)) = separator *ᵥ (fun i => (excessive i : ℚ)) := by
108   rintro ⟨m, hm, ht⟩
109   have h := natural_multiplicity_unique separator determinant_nonzero m excessive ht
110   exact excessive_not_admissible (h ▸ hm)
111 
112 /-- Field extension preserves rank, but residue reduction need not. -/
113 theorem separator_mod2_singular :
114     ( (!![1,1,1; 1,-1,1; 1,1,-1] : Matrix (Fin 3) (Fin 3) (ZMod 2))).det = 0 := by
115   rw [Matrix.det_fin_three]; decide +kernel
116 
117 /-- Natural multiplicities cannot be recovered from traces in characteristic two. -/
118 theorem natural_trace_collision_mod2 :
119     (1 : Matrix (Fin 1) (Fin 1) (ZMod 2)) *ᵥ (fun _ => (0 : ZMod 2)) =
120     (1 : Matrix (Fin 1) (Fin 1) (ZMod 2)) *ᵥ (fun _ => (2 : ZMod 2)) := by
121   decide +kernel
122 
123 end PaperX.TraceExamples

Back to source controls