GeneralLogarithmExamples.lean

1 import PaperX.GeneralReconstructionRecovery
2 import PaperX.ReconstructionBoundary
3 
4 /-! Actual affine representations with arbitrarily long monodromy chains.
5 The quartic example lies outside the predecessor's cubic recovery class. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.GeneralLogarithmExamples
9 open PaperX.WeilData PaperX.WeilSpecialChain PaperX.SpecialMonodromy
10 open PaperX.AffineMonodromy PaperX.ReconstructionExamples
11 open PaperX.NilpotentExponential PaperX.MonodromyReconstruction
12 open PaperX.LogarithmicRecovery
13 
14 def chainAction (n : ℕ) : Representation ℚ G (Fin n → ℚ) :=
15   reconstruct (chain ℚ n) chosenCocycle
16 
17 theorem chain_translation_action (n : ℕ) : (chain ℚ n).r u = 1 := by
18   ext x j
19   simp [chain, chainDatum, chainRep, diagonalF, norm, u, translation,
20     SemidirectProduct.rightHom]
21 
22 theorem chain_sample (n : ℕ) : chainAction n u = expN (chain ℚ n).N 1 := by
23   apply LinearMap.ext
24   intro x
25   change expN (chain ℚ n).N (chosenCocycle.value u) ((chain ℚ n).r u x) = _
26   rw [chain_translation_action]
27   rfl
28 
29 /-- This invokes the general extraction theorem for every chain length. -/
30 theorem recover_arbitrary_chain (n : ℕ) : recoverN 1 (chainAction n u) = (chain ℚ n).N := by
31   rw [chain_sample]
32   exact recoverN_expN (chain ℚ n).nilpotent (by norm_num)
33 
34 theorem arbitrary_chain_fixed_vectors (n : ℕ) (x : Fin n → ℚ) :
35     chainAction n u x = x ↔ (chain ℚ n).N x = 0 := by
36   rw [chain_sample]
37   exact expN_fixed_iff (chain ℚ n).nilpotent (by norm_num) x
38 
39 theorem sixth_order_example :
40     (chain ℚ 6).N ^ 5 ≠ 0 ∧ (chain ℚ 6).N ^ 6 = 0 ∧
41       recoverN 1 (chainAction 6 u) = (chain ℚ 6).N :=
42   ⟨shift_previous_power_nonzero 6 (by decide), shift_nilpotent 6,
43     recover_arbitrary_chain 6⟩
44 
45 /-- The former quartic counterexample is now recovered by the full logarithm. -/
46 theorem quartic_recovered_but_quadratic_fails :
47     recoverN 1 (expN PaperX.ReconstructionBoundary.datum4.N 1) =
48       PaperX.ReconstructionBoundary.datum4.N ∧
49     PaperX.UnipotentLogarithm.log₂ (expN PaperX.ReconstructionBoundary.datum4.N 1) ≠
50       PaperX.ReconstructionBoundary.datum4.N := by
51   exact ⟨recoverN_expN PaperX.ReconstructionBoundary.datum4.nilpotent (by norm_num),
52     PaperX.ReconstructionBoundary.quadratic_log_fails_beyond_cube⟩
53 
54 theorem recover_arbitrary_chain_parameter (n : ℕ) (s : ℚ) (hs : s ≠ 0) :
55     recoverN s (expN (chain ℚ n).N s) = (chain ℚ n).N :=
56   recoverN_expN (chain ℚ n).nilpotent hs
57 
58 /-- The parameter restriction remains essential even with the complete logarithm. -/
59 theorem general_zero_parameter_recovery_fails :
60     recoverN 0 (expN datum3.N 0) ≠ datum3.N := by
61   simpa [recoverN] using PaperX.ReconstructionBoundary.monodromy_nonzero.symm
62 
63 /-- Any reconstructed-action intertwiner between two arbitrary chain lengths
64 recovers both the original affine action and monodromy. -/
65 theorem arbitrary_chain_intertwiner (n m : ℕ) (f : (Fin n → ℚ) →ₗ[ℚ] (Fin m → ℚ)) :
66     (∀ g x, f (chainAction n g x) = chainAction m g (f x)) ↔
67       (∀ g x, f ((chain ℚ n).r g x) = (chain ℚ m).r g (f x)) ∧
68         (chain ℚ m).N ∘ₗ f = f ∘ₗ (chain ℚ n).N := by
69   exact PaperX.GeneralReconstructionRecovery.reconstruct_intertwiner_iff
70     chosenCocycle u (chain_translation_action n) (chain_translation_action m)
71     (by norm_num [chosenCocycle, translation_value.1]) f
72 
73 end PaperX.GeneralLogarithmExamples

Back to source controls