ReconstructionBoundary.lean

1 import PaperX.ReconstructionExamples
2 import PaperX.UnipotentLogarithm
3 
4 /-! Checked limits of the quadratic logarithm and of zero-parameter sampling. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.ReconstructionBoundary
8 open PaperX.AffineMonodromy PaperX.ReconstructionExamples
9 open PaperX.WeilSpecialChain PaperX.SpecialMonodromy
10 open PaperX.NilpotentExponential PaperX.UnipotentLogarithm
11 open PaperX.MonodromyReconstruction
12 
13 def datum4 : PaperX.WeilData.Datum ν (Fin 4 → ℚ) := chain ℚ 4
14 
15 theorem quartic_nilpotence : datum4.N ^ 3 ≠ 0 ∧ datum4.N ^ 4 = 0 :=
16   ⟨shift_previous_power_nonzero 4 (by decide), shift_nilpotent 4⟩
17 
18 theorem quartic_exponential_coordinates (s : ℚ) (x : Fin 4 → ℚ) :
19     expN datum4.N s x =
20       ![x 0 + s * x 1 + (s ^ 2 / 2) * x 2 + (s ^ 3 / 6) * x 3,
21         x 1 + s * x 2 + (s ^ 2 / 2) * x 3, x 2 + s * x 3, x 3] := by
22   rw [expN_sum quartic_nilpotence.2]
23   funext j
24   fin_cases j <;>
25     simp [Finset.sum_range_succ, smul_pow, datum4, chain, chainDatum,
26       shift_pow_apply, Nat.factorial] <;> ring
27 
28 theorem quadratic_log_error :
29     log₂ (expN datum4.N 1) ![0, 0, 0, 1] 0 = -(1/3 : ℚ) := by
30   norm_num [log₂, pow_two, Module.End.mul_apply, LinearMap.sub_apply,
31     quartic_exponential_coordinates, Matrix.cons_val_two, Matrix.cons_val_three]
32 
33 theorem quadratic_log_fails_beyond_cube : log₂ (expN datum4.N 1) ≠ datum4.N := by
34   intro h
35   have he := congrArg (fun A : Module.End ℚ (Fin 4 → ℚ) => A ![0, 0, 0, 1] 0) h
36   rw [quadratic_log_error] at he
37   norm_num [datum4, chain, chainDatum, shift_apply] at he
38 
39 theorem monodromy_nonzero : datum3.N ≠ 0 := by
40   intro h
41   have hn := nonzero_monodromy.1
42   simp [h] at hn
43 
44 theorem zero_sample_collision :
45     expN datum3.N 0 = expN (0 : Module.End ℚ (Fin 3 → ℚ)) 0 ∧ datum3.N ≠ 0 := by
46   exact ⟨by simp, monodromy_nonzero⟩
47 
48 theorem zero_parameter_recovery_fails : recoverN 0 (expN datum3.N 0) ≠ datum3.N := by
49   simpa [recoverN] using monodromy_nonzero.symm
50 
51 theorem actual_translation_exponential : good3 u = expN datum3.N 1 := by
52   ext x
53   simp [good3, chosenCocycle, reconstruct_apply, unipotent,
54     translation_value.1, translation_action]
55 
56 theorem actual_monodromy_recovery : recoverN 1 (good3 u) = datum3.N := by
57   rw [actual_translation_exponential]
58   exact recoverN_expN nonzero_monodromy.2 (by norm_num)
59 
60 theorem actual_fixed_vectors (x : Fin 3 → ℚ) : good3 u x = x ↔ datum3.N x = 0 := by
61   rw [actual_translation_exponential]
62   exact expN_fixed_iff nonzero_monodromy.2 (by norm_num) x
63 
64 end PaperX.ReconstructionBoundary

Back to source controls