DyadicIsometryControls.lean

1 module
2 public import DyadicFourIsometry
3 public import Mathlib.NumberTheory.Padics.RingHoms
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace KomorebiPaperIX.DyadicIsometryControls
10 
11 open DyadicFourIsometry
12 
13 /-- A concrete value confirms the normalization and its sign. -/
14 theorem address_zero_at_one : isometry 0 (by decide) (1 : ℤ_[2]) = -1 := by
15   have hr : DyadicPacketRational.packet 0 1 = (-1 : ℚ) := by
16     norm_num [DyadicPacketRational.packet, Congruential.unnormalized,
17       DyadicFourLeastPeriods.originalBonus, DyadicFourPrefix.bonus,
18       DyadicFourPrefix.coeff_0_1]
19   apply Subtype.ext
20   have h := isometry_nat 0 (by decide) 1
21   simpa [hr] using h
22 
23 /-- The next exact value detects that the isometry is not additive. -/
24 theorem address_zero_at_two : isometry 0 (by decide) (2 : ℤ_[2]) = 34 := by
25   have hr : DyadicPacketRational.packet 0 2 = (34 : ℚ) := by
26     norm_num [DyadicPacketRational.packet, Congruential.unnormalized,
27       DyadicFourLeastPeriods.originalBonus, DyadicFourPrefix.bonus,
28       DyadicFourPrefix.coeff_0_2]
29   apply Subtype.ext
30   have h := isometry_nat 0 (by decide) 2
31   change ((isometry 0 (by decide) (2 : ℤ_[2])) : ℚ_[2]) = (34 : ℚ_[2])
32   simpa [hr] using h
33 
34 /-- A metric isometry does not thereby become an additive or ring homomorphism. -/
35 theorem address_zero_not_additive :
36     ¬ ∀ x y : ℤ_[2], isometry 0 (by decide) (x + y) =
37       isometry 0 (by decide) x + isometry 0 (by decide) y := by
38   intro h
39   have hh := h 1 1
40   norm_num [address_zero_at_one, address_zero_at_two] at hh
41 
42 /-- The inverse recovers the nontrivial second rational sample. -/
43 theorem address_zero_inverse_at_thirty_four :
44     (isometry 0 (by decide)).symm (34 : ℤ_[2]) = 2 := by
45   rw [← address_zero_at_two]
46   exact (isometry 0 (by decide)).symm_apply_apply 2
47 
48 /-- The unnormalized address-zero packet stays in the odd residue class. -/
49 theorem original_address_zero_ne_zero (x : ℤ_[2]) :
50     originalExtension 0 (by decide) x ≠ 0 := by
51   intro hx
52   have h := congrArg (PadicInt.toZMod : ℤ_[2] →+* ZMod 2) hx
53   have ht : PadicInt.toZMod (2 : ℤ_[2]) = (0 : ZMod 2) := by
54     change PadicInt.toZMod ((2 : ℕ) : ℤ_[2]) = 0
55     rw [map_natCast]
56     exact ZMod.natCast_self 2
57   norm_num [originalExtension, DyadicFourLeastPeriods.originalBonus,
58     DyadicFourPrefix.bonus, ht] at h
59 
60 /-- The original affine image is not the whole dyadic integer ring. -/
61 theorem original_address_zero_not_surjective :
62     ¬ Function.Surjective (originalExtension 0 (by decide)) := by
63   intro h
64   obtain ⟨x, hx⟩ := h 0
65   exact original_address_zero_ne_zero x hx
66 
67 end KomorebiPaperIX.DyadicIsometryControls

Back to source controls