Residual.lean

1 import Std
2 
3 /-!
4 Paper X, first checked block: residual partition and no crossing.
5 The reduction map is data. Positive-depth operations must preserve that map.
6 An infinite stream has a limit only under the explicit convergence hypothesis.
7 No arithmetic companion, occupancy, or Collatz assumption is imported.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.Residual
11 
12 variable {X R : Type}
13 
14 def Fiber (red : X → R) (r : R) := {x : X // red x = r}
15 
16 def pack (red : X → R) (x : X) : (r : R) × Fiber red r :=
17   ⟨red x, ⟨x, rfl⟩⟩
18 
19 def unpack (red : X → R) (p : (r : R) × Fiber red r) : X := p.2.1
20 
21 theorem unpack_pack (red : X → R) (x : X) : unpack red (pack red x) = x := rfl
22 
23 theorem pack_unpack (red : X → R) (p : (r : R) × Fiber red r) :
24     pack red (unpack red p) = p := by
25   rcases p with ⟨r, x, hx⟩
26   cases hx
27   rfl
28 
29 theorem residual_exhaustive (red : X → R) (x : X) : ∃ r, red x = r :=
30   ⟨red x, rfl⟩
31 
32 theorem residual_unique (red : X → R) (x : X) (r s : R)
33     (hr : red x = r) (hs : red x = s) : r = s := hr.symm.trans hs
34 
35 theorem fibers_disjoint (red : X → R) (r s : R) (hne : r ≠ s) :
36     ¬ ∃ x, red x = r ∧ red x = s := by
37   rintro ⟨x, hr, hs⟩
38   exact hne (residual_unique red x r s hr hs)
39 
40 /-- A finite sequence of allowed operations, including the empty sequence. -/
41 inductive Reach (step : X → X → Prop) : X → X → Prop
42   | refl (x : X) : Reach step x x
43   | next {x y z : X} : Reach step x y → step y z → Reach step x z
44 
45 theorem no_crossing_finite (red : X → R) (step : X → X → Prop)
46     (preserves : ∀ {x y}, step x y → red y = red x)
47     {x y : X} (h : Reach step x y) : red y = red x := by
48   induction h with
49   | refl => rfl
50   | next _ hs ih => exact (preserves hs).trans ih
51 
52 theorem zeroth_order_obstruction (red : X → R) (step : X → X → Prop)
53     (preserves : ∀ {x y}, step x y → red y = red x)
54     {x y : X} (different : red x ≠ red y) : ¬ Reach step x y := by
55   intro h
56   exact different (no_crossing_finite red step preserves h).symm
57 
58 theorem stream_invariant (red : X → R) (step : X → X → Prop)
59     (preserves : ∀ {x y}, step x y → red y = red x)
60     (stream : Nat → X) (follows : ∀ n, step (stream n) (stream (n+1))) :
61     ∀ n, red (stream n) = red (stream 0) := by
62   intro n
63   induction n with
64   | zero => rfl
65   | succ n ih => exact (preserves (follows n)).trans ih
66 
67 /-- Finite-precision convergence; the type of observations may depend on depth. -/
68 def PrecisionConverges {Y : Type} {Level : Nat → Type}
69     (observe : (d : Nat) → Y → Level d) (stream : Nat → Y) (limit : Y) : Prop :=
70   ∀ d, ∃ N, ∀ n, N ≤ n → observe d (stream n) = observe d limit
71 
72 theorem no_crossing_limit {Y : Type} {Level : Nat → Type}
73     (observe : (d : Nat) → Y → Level d) (stream : Nat → Y) (limit : Y)
74     (sameRoot : ∀ n, observe 0 (stream n) = observe 0 (stream 0))
75     (converges : PrecisionConverges observe stream limit) :
76     observe 0 limit = observe 0 (stream 0) := by
77   obtain ⟨N, hN⟩ := converges 0
78   exact (hN N (Nat.le_refl N)).symm.trans (sameRoot N)
79 
80 theorem positive_depth_mod (p x h : Nat) : (x + p*h) % p = x % p := by
81   simp [Nat.add_mod]
82 
83 /-- Root preservation alone does not imply convergence: alternating 0 and 3. -/
84 def oscillation (n : Nat) : Nat := if n % 2 = 0 then 0 else 3
85 
86 theorem oscillation_same_root (n : Nat) : oscillation n % 3 = 0 := by
87   unfold oscillation
88   split <;> decide
89 
90 /-- At precision 9, the root-preserving stream is not even eventually constant. -/
91 theorem oscillation_not_eventually_constant_mod9 :
92     ¬ ∃ r N : Nat, ∀ n, N ≤ n → oscillation n % 9 = r := by
93   rintro ⟨r, N, h⟩
94   have he := h (2*N) (by omega)
95   have ho := h (2*N+1) (by omega)
96   have even : (2*N) % 2 = 0 := by omega
97   simp [oscillation, even] at he
98   simp [oscillation] at ho
99   omega
100 
101 end PaperX.Residual

Back to source controls