CompletionObstructions.lean

1 import PaperX.CompletionExamples
2 
3 /-! A finite occupied representation node can die at the next precision, even
4 while other branches of the same forest survive. The computations below are
5 kernel checked over Z/4 and Z/8, not universal arithmetic occupancy assertions. -/
6 set_option autoImplicit false
7 namespace PaperX.CompletionObstructions
8 open scoped Matrix
9 open PaperX.RepresentationLimits PaperX.CompletionExamples
10 
11 instance fourLarge : Fact (1 < 4) := ⟨by decide⟩
12 instance eightLarge : Fact (1 < 8) := ⟨by decide⟩
13 
14 def node4 : Matrix (Fin 2) (Fin 2) (ZMod 4) := !![1,2;2,3]
15 def red8 : ZMod 8 →+* ZMod 4 := ZMod.castHom (by decide) (ZMod 4)
16 
17 theorem node4_involution : node4 * node4 = 1 := by decide +kernel
18 
19 theorem node4_polynomial : node4.charpoly = Polynomial.X^2 - 1 := by
20   rw [Matrix.charpoly_fin_two]
21   have ht : node4.trace = 0 := by decide +kernel
22   have hd : node4.det = -1 := by decide +kernel
23   rw [ht, hd]
24   simp [sub_eq_add_neg]
25 
26 def nodeRepresentation : MatrixRep (ZMod 4) C2 (Fin 2) where
27   toFun g := if g = 1 then 1 else node4
28   map_one' := by decide +kernel
29   map_mul' := by decide +kernel
30 
31 theorem node_generator : nodeRepresentation generator = node4 := by decide +kernel
32 
33 /-- The obstruction is trace and determinant at the next dyadic precision. -/
34 theorem lifted_trace_forces_wrong_det : ∀ a b c d : ZMod 8,
35     red8 a = 1 → red8 b = 2 → red8 c = 2 → red8 d = 3 →
36     a + d = 0 → a*d-b*c ≠ -1 := by
37   decide +kernel
38 
39 theorem no_matrix_lift (B : Matrix (Fin 2) (Fin 2) (ZMod 8))
40     (hB : B.map red8 = node4) : B.charpoly ≠ Polynomial.X^2 - 1 := by
41   intro hp
42   have ht : B.trace = 0 := by
43     have H := congrArg (fun p : Polynomial (ZMod 8) => p.coeff 1) hp
44     simpa [Matrix.charpoly_fin_two, Polynomial.coeff_one] using H
45   have hd : B.det = -1 := by
46     have H := congrArg (fun p : Polynomial (ZMod 8) => p.coeff 0) hp
47     simpa [Matrix.charpoly_fin_two, Polynomial.coeff_one] using H
48   have hij := fun i j => congrArg (fun A : Matrix (Fin 2) (Fin 2) (ZMod 4) => A i j) hB
49   apply lifted_trace_forces_wrong_det (B 0 0) (B 0 1) (B 1 0) (B 1 1)
50     (hij 0 0) (hij 0 1) (hij 1 0) (hij 1 1)
51   · simpa [Matrix.trace, Fin.sum_univ_succ] using ht
52   · simpa [Matrix.det_fin_two] using hd
53 
54 /-- This is an actual representation node without a next-level child having the
55 same selected polynomial, not just an unrelated scalar root example. -/
56 theorem no_representation_lift : ¬ ∃ ρ : MatrixRep (ZMod 8) C2 (Fin 2),
57     changeCoefficients red8 ρ = nodeRepresentation ∧
58     (ρ generator).charpoly = Polynomial.X^2-1 := by
59   rintro ⟨ρ,hr,hp⟩
60   have hB : (ρ generator).map red8 = node4 := by
61     exact (congrArg (fun τ => τ generator) hr).trans node_generator
62   exact no_matrix_lift (ρ generator) hB hp
63 
64 end PaperX.CompletionObstructions

Back to source controls