GeneralRecoveryBoundary.lean

1 import PaperX.GeneralLogarithmExamples
2 
3 /-! The original-action sample condition remains essential. An exponential
4 factor can be absorbed into the supplied original group action, giving the
5 same reconstructed representation with different monodromy data. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.GeneralRecoveryBoundary
9 open PaperX.WeilData PaperX.MonodromyReconstruction
10 
11 variable {K G : Type*} [Field K] [CharZero K] [Group G] {ν : G →* Kˣ}
12 variable {V : Type*} [AddCommGroup V] [Module K V]
13 
14 /-- Absorb the whole reconstructed action into r and set monodromy to zero. -/
15 def absorbed (D : Datum ν V) (t : TwistedCocycle ν) : Datum ν V where
16   r := reconstruct D t
17   N := 0
18   nilpotent := ⟨1, by simp⟩
19   relation g x := by simp
20 
21 theorem absorbed_reconstruct (D : Datum ν V) (t : TwistedCocycle ν) :
22     reconstruct (absorbed D t) t = reconstruct D t := by
23   ext g x
24   simp [absorbed, reconstruct_apply, unipotent, PaperX.NilpotentExponential.expN]
25 
26 theorem absorbed_monodromy (D : Datum ν V) (t : TwistedCocycle ν) :
27     (absorbed D t).N = 0 := rfl
28 
29 open PaperX.AffineMonodromy PaperX.ReconstructionExamples
30 open PaperX.GeneralLogarithmExamples PaperX.LogarithmicRecovery
31 open PaperX.SpecialMonodromy
32 
33 theorem long_chain_monodromy_nonzero : (chain ℚ 6).N ≠ 0 := by
34   intro h
35   have hn := (sixth_order_example).1
36   simp [h] at hn
37 
38 /-- Equal reconstructed representations and a nonzero cocycle sample do not
39 by themselves determine the original monodromy datum. -/
40 theorem identical_reconstruction_different_monodromy :
41     reconstruct (absorbed (chain ℚ 6) chosenCocycle) chosenCocycle = chainAction 6 ∧
42       (absorbed (chain ℚ 6) chosenCocycle).N ≠ (chain ℚ 6).N ∧
43       chosenCocycle.value u ≠ 0 := by
44   exact ⟨absorbed_reconstruct _ _, long_chain_monodromy_nonzero.symm,
45     by norm_num [chosenCocycle, translation_value.1]⟩
46 
47 /-- The absorbed datum fails exactly the original-action hypothesis used in
48 the general extraction theorem. -/
49 theorem absorbed_original_sample_nontrivial :
50     (absorbed (chain ℚ 6) chosenCocycle).r u ≠ 1 := by
51   intro h
52   have hs : chainAction 6 u = 1 := h
53   have hr := recover_arbitrary_chain 6
54   rw [hs] at hr
55   have hz : (chain ℚ 6).N = 0 := by
56     simpa [recoverN, PaperX.FiniteLogarithm.log_one] using hr.symm
57   exact long_chain_monodromy_nonzero hz
58 
59 /-- The complete logarithm still cannot recover an arbitrary supplied N
60 unless the known original action is trivial at the sample. -/
61 theorem recovery_without_original_sample_fails :
62     recoverN 1 (reconstruct (absorbed (chain ℚ 6) chosenCocycle) chosenCocycle u) ≠
63       (absorbed (chain ℚ 6) chosenCocycle).N := by
64   intro hbad
65   have he := congrArg (fun ρ : Representation ℚ (Affine ℚ) (Fin 6 → ℚ) =>
66     recoverN 1 (ρ u)) (absorbed_reconstruct (chain ℚ 6) chosenCocycle)
67   have hrec : recoverN 1
68       (reconstruct (absorbed (chain ℚ 6) chosenCocycle) chosenCocycle u) =
69         (chain ℚ 6).N := he.trans (recover_arbitrary_chain 6)
70   exact long_chain_monodromy_nonzero (hrec.symm.trans hbad)
71 
72 
73 end PaperX.GeneralRecoveryBoundary

Back to source controls