Theme/Transfer.lean — FrcCore

1import FrcCore.Theme.Reach23/-!4# The logic theme — the transfer digraph: walks of every length give a periodic walk565-reductio's Theorem periodic-dbe (5:E6), the one-dimensional periodic de Bruijn–Erdős theorem, at the level of its7transfer digraph (21 October 2026): a finite digraph on `[0, n)` in which walks of every finite length exist has a8vertex that begins walks of every length, every such vertex has a successor of the same kind, and the greedy walk9inside that sub-digraph (the least good successor at each step) is eventually periodic with period at most `n`10(5:E5's pigeonhole, `repeat_below`). A proper colouring of `k` consecutive blocks of a periodic graph is a walk of11length `k − 1` in its transfer digraph, so the periodic walk is a periodic proper colouring; that passage is the12body's modelling and rests there. No Mathlib, no axioms: the stabilisation of the decreasing sets of good vertices13is proved by counting, and the periodic walk is built by bounded search.14-/1516namespace FRC.Transfer1718open FRC.Logic FRC.Reach1920/-- `walks edge n v k`: in the digraph on `[0, n)` with edge relation `edge`, the vertex `v` begins a walk of `k`21edges. -/22def walks (edge : Nat → Nat → Bool) (n : Nat) (v : Nat) : Nat → Bool23  | 0 => true24  | k + 1 => anyBelow (fun w => edge v w && walks edge n w k) n2526variable {edge : Nat → Nat → Bool} {n : Nat}2728theorem walks_succ_iff (v k : Nat) :29    walks edge n v (k + 1) = true ↔ ∃ w, w < n ∧ edge v w = true ∧ walks edge n w k = true :=30  Iff.trans (anyBelow_true_iff _ n)31    ⟨fun ⟨w, hw, h⟩ => ⟨w, hw, band_l h, band_r h⟩, fun ⟨w, hw, h1, h2⟩ => ⟨w, hw, by rw [h1, h2]; rfl⟩⟩3233/-- A walk of `k + 1` edges contains one of `k`. -/34theorem walks_of_succ (v : Nat) : ∀ k, walks edge n v (k + 1) = true → walks edge n v k = true35  | 0, _ => rfl36  | k + 1, h => by37    match (walks_succ_iff v (k + 1)).mp h with38    | ⟨w, hw, he, hk⟩ => exact (walks_succ_iff v k).mpr ⟨w, hw, he, walks_of_succ w k hk⟩3940theorem walks_mono (v : Nat) : ∀ j k, j ≤ k → walks edge n v k = true → walks edge n v j = true41  | j, k, hjk, h => by42    match Nat.eq_or_lt_of_le hjk with43    | Or.inl e => exact e ▸ h44    | Or.inr hlt =>45      match k, hlt with46      | k' + 1, hlt' => exact walks_mono v j k' (Nat.le_of_lt_succ hlt') (walks_of_succ v k' h)4748/-! ### The sets of good vertices decrease and stabilise -/4950/-- The number of vertices below `n` that begin a walk of `k` edges. -/51def goodCount (edge : Nat → Nat → Bool) (n k : Nat) : Nat := count (fun v => walks edge n v k) n5253theorem count_le_of_imp (f g : Nat → Bool) : ∀ m, (∀ x, x < m → f x = true → g x = true) → count f m ≤ count g m54  | 0, _ => Nat.le_refl 055  | m + 1, h => by56    show count f m + cond (f m) 1 0 ≤ count g m + cond (g m) 1 057    have ih := count_le_of_imp f g m (fun x hx => h x (Nat.lt_succ_of_lt hx))58    exact match hf : f m with59      | false => Nat.le_trans (Nat.add_le_add_right ih 0) (Nat.add_le_add_left (Nat.zero_le _) _)60      | true => by rw [h m (Nat.lt_succ_self m) hf]; exact Nat.add_le_add_right ih 16162theorem count_le (f : Nat → Bool) : ∀ m, count f m ≤ m63  | 0 => Nat.le_refl 064  | m + 1 => by65    show count f m + cond (f m) 1 0 ≤ m + 166    exact match f m with67      | true => Nat.add_le_add_right (count_le f m) 168      | false => Nat.le_succ_of_le (count_le f m)6970/-- Equal counts of nested predicates: the smaller one holds wherever the larger does. -/71theorem eq_of_count_eq (f g : Nat → Bool) : ∀ m, (∀ x, x < m → f x = true → g x = true) → count f m = count g m →72    ∀ x, x < m → g x = true → f x = true73  | 0, _, _, x, hx, _ => absurd hx (Nat.not_lt_zero x)74  | m + 1, h, e, x, hx, hg => by75    have h' : ∀ x, x < m → f x = true → g x = true := fun x hx => h x (Nat.lt_succ_of_lt hx)76    have ih := count_le_of_imp f g m h'77    have e' : count f m + cond (f m) 1 0 = count g m + cond (g m) 1 0 := e78    match Nat.lt_or_ge x m with79    | Or.inl hxm =>80      -- the last position agrees or f m = false ≤ g m; either way the counts below m are equal81      have em : count f m = count g m := by82        match hf : f m with83        | true =>84          rw [hf, h m (Nat.lt_succ_self m) hf] at e'85          exact Nat.add_right_cancel e'86        | false =>87          rw [hf] at e'88          exact match hgm : g m with89            | false => by rw [hgm] at e'; exact Nat.add_right_cancel e'90            | true => by91                rw [hgm] at e'92                exact absurd e' (Nat.ne_of_lt (Nat.lt_of_le_of_lt (Nat.add_le_add_right ih 0) (Nat.lt_succ_self _)))93      exact eq_of_count_eq f g m h' em x hxm hg94    | Or.inr hxm =>95      have ex : x = m := Nat.le_antisymm (Nat.le_of_lt_succ hx) hxm96      subst ex97      exact match hf : f x with98        | true => rfl99        | false => by100            rw [hf, hg] at e'101            exact absurd e' (Nat.ne_of_lt (Nat.lt_of_le_of_lt (Nat.add_le_add_right ih 0) (Nat.lt_succ_self _)))102103/-- The good sets decrease: `goodCount (k+1) ≤ goodCount k`. -/104theorem goodCount_succ_le (k : Nat) : goodCount edge n (k + 1) ≤ goodCount edge n k :=105  count_le_of_imp _ _ n (fun v _ h => walks_of_succ v k h)106107theorem goodCount_le_of_le : ∀ j k, j ≤ k → goodCount edge n k ≤ goodCount edge n j108  | j, k, hjk => count_le_of_imp _ _ n (fun v _ h => walks_mono v j k hjk h)109110/-- When the good set stops shrinking it is stationary: `goodCount k₀ = goodCount (k₀+1)` gives111`walks v k₀ → walks v k` for every `k`. -/112theorem stationary (k₀ : Nat) (e : goodCount edge n k₀ = goodCount edge n (k₀ + 1)) :113    ∀ k, ∀ v, v < n → walks edge n v k₀ = true → walks edge n v k = true := by114  -- step: the (k₀+1)-good are exactly the k₀-good; then (k₀+2)-good = successors into k₀-good ∩ … by induction115  have back : ∀ v, v < n → walks edge n v k₀ = true → walks edge n v (k₀ + 1) = true :=116    eq_of_count_eq (fun v => walks edge n v (k₀ + 1)) (fun v => walks edge n v k₀) n117      (fun v _ h => walks_of_succ v k₀ h) e.symm118  have up : ∀ m, ∀ v, v < n → walks edge n v k₀ = true → walks edge n v (k₀ + m) = true := by119    intro m120    induction m with121    | zero => exact fun v _ h => h122    | succ m ih =>123      intro v hv h124      match (walks_succ_iff v k₀).mp (back v hv h) with125      | ⟨w, hw, he, hk⟩ => exact (walks_succ_iff v (k₀ + m)).mpr ⟨w, hw, he, ih w hw hk⟩126  intro k v hv h127  match Nat.lt_or_ge k k₀ with128  | Or.inl hlt => exact walks_mono v k k₀ (Nat.le_of_lt hlt) h129  | Or.inr hge =>130    have : k = k₀ + (k - k₀) := (FRC.Nat.add_sub_of_le hge).symm131    rw [this]; exact up (k - k₀) v hv h132133/-- Among `k = 0, …, n` the decreasing counts, all at most `n`, repeat: some `k₀ ≤ n` is stationary. -/134theorem exists_stationary : ∃ k₀, k₀ ≤ n ∧ goodCount edge n k₀ = goodCount edge n (k₀ + 1) := by135  -- otherwise the counts drop strictly at every step below n + 1, so goodCount (n+1) + (n+1) ≤ goodCount 0 ≤ n136  have drop : ∀ m, (∀ k, k < m → goodCount edge n k ≠ goodCount edge n (k + 1)) →137      goodCount edge n m + m ≤ goodCount edge n 0 := by138    intro m139    induction m with140    | zero => exact fun _ => Nat.le_refl _141    | succ m ih =>142      intro h143      have ih' := ih (fun k hk => h k (Nat.lt_succ_of_lt hk))144      have hlt : goodCount edge n (m + 1) < goodCount edge n m :=145        Nat.lt_of_le_of_ne (goodCount_succ_le m) (fun e => h m (Nat.lt_succ_self m) e.symm)146      show goodCount edge n (m + 1) + (m + 1) ≤ goodCount edge n 0147      have h3 : goodCount edge n (m + 1) + (m + 1) ≤ goodCount edge n m + m := by148        rw [← Nat.add_assoc, Nat.add_right_comm]149        exact Nat.add_le_add_right (Nat.succ_le_of_lt hlt) m150      exact Nat.le_trans h3 ih'151  have dec : Decidable (∃ k, k < n + 1 ∧ goodCount edge n k = goodCount edge n (k + 1)) :=152    FRC.Shell.decExistsLT (fun k => goodCount edge n k = goodCount edge n (k + 1)) (n + 1)153  match dec with154  | isTrue ⟨k, hk, e⟩ => exact ⟨k, Nat.le_of_lt_succ hk, e⟩155  | isFalse hne =>156    exfalso157    have hall : ∀ k, k < n + 1 → goodCount edge n k ≠ goodCount edge n (k + 1) :=158      fun k hk e => hne ⟨k, hk, e⟩159    have h1 := drop (n + 1) hall160    have h2 : goodCount edge n 0 ≤ n := count_le _ n161    exact Nat.lt_irrefl (n + 1) (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_add_left (n + 1) _) h1) (Nat.lt_succ_of_le h2))162163/-! ### A vertex good for every length, and a good successor -/164165/-- `allGood v`: `v` begins walks of every length. -/166def AllGood (edge : Nat → Nat → Bool) (n v : Nat) : Prop := ∀ k, walks edge n v k = true167168/-- 5:E6 (Theorem periodic-dbe, the sub-digraph is nonempty) — if walks of every length exist, some vertex begins169walks of every length: the good sets decrease and stabilise, and a vertex of the stationary set is good for ever. -/170theorem exists_allGood (h : ∀ k, ∃ v, v < n ∧ walks edge n v k = true) : ∃ v, v < n ∧ AllGood edge n v :=171  match exists_stationary (edge := edge) (n := n) with172  | ⟨k₀, _, e⟩ => match h k₀ with173    | ⟨v, hv, hk⟩ => ⟨v, hv, fun k => stationary k₀ e k v hv hk⟩174175/-- 5:E6 (Theorem periodic-dbe, out-degree one in the sub-digraph) — a vertex good for every length has a successor176good for every length. -/177theorem allGood_successor {v : Nat} (_hv : v < n) (hg : AllGood edge n v) :178    ∃ w, w < n ∧ edge v w = true ∧ AllGood edge n w :=179  match exists_stationary (edge := edge) (n := n) with180  | ⟨k₀, _, e⟩ => match (walks_succ_iff v k₀).mp (hg (k₀ + 1)) with181    | ⟨w, hw, he, hk⟩ => ⟨w, hw, he, fun k => stationary k₀ e k w hw hk⟩182183/-! ### The greedy walk in the sub-digraph and its period -/184185/-- The stationary length, by bounded search (`exists_stationary` gives it below `n + 1`). -/186def stationaryIndex (edge : Nat → Nat → Bool) (n : Nat) : Nat :=187  match leastBelow (fun k => decide (goodCount edge n k = goodCount edge n (k + 1))) (n + 1) with188  | some k => k189  | none => 0190191theorem stationaryIndex_spec : goodCount edge n (stationaryIndex edge n) = goodCount edge n (stationaryIndex edge n + 1) :=192  match exists_stationary (edge := edge) (n := n) with193  | ⟨k₀, hk₀, e⟩ => by194    unfold stationaryIndex195    match hl : leastBelow (fun k => decide (goodCount edge n k = goodCount edge n (k + 1))) (n + 1) with196    | some k => exact of_decide_eq_true (leastBelow_spec _ (n + 1) k hl).2.1197    | none =>198      exfalso199      match leastBelow_some (fun k => decide (goodCount edge n k = goodCount edge n (k + 1))) (n + 1) k₀200          (Nat.lt_succ_of_le hk₀) (decide_eq_true e) with201      | ⟨y, hy⟩ => rw [hl] at hy; exact nomatch hy202203/-- `good v`: `v` is good at the stationary length, hence for every length. -/204def good (edge : Nat → Nat → Bool) (n : Nat) (v : Nat) : Bool := walks edge n v (stationaryIndex edge n)205206theorem allGood_of_good {v : Nat} (hv : v < n) (h : good edge n v = true) : AllGood edge n v :=207  fun k => stationary (stationaryIndex edge n) stationaryIndex_spec k v hv h208209/-- The greedy step: the least good successor of `v`, or `v` itself when there is none (never, on good vertices). -/210def next (edge : Nat → Nat → Bool) (n : Nat) (v : Nat) : Nat :=211  match leastBelow (fun w => edge v w && good edge n w) n with212  | some w => w213  | none => v214215theorem next_spec {v : Nat} (hv : v < n) (hg : good edge n v = true) :216    next edge n v < n ∧ edge v (next edge n v) = true ∧ good edge n (next edge n v) = true := by217  match allGood_successor hv (allGood_of_good hv hg) with218  | ⟨w, hw, he, hwg⟩ =>219    have hP : (edge v w && good edge n w) = true := by220      have hgw : good edge n w = true := hwg (stationaryIndex edge n)221      rw [he, hgw]; rfl222    unfold next223    match hl : leastBelow (fun w => edge v w && good edge n w) n with224    | some u =>225      have s := leastBelow_spec _ n u hl226      exact ⟨s.1, band_l s.2.1, band_r s.2.1⟩227    | none =>228      exfalso229      match leastBelow_some (fun w => edge v w && good edge n w) n w hw hP with230      | ⟨y, hy⟩ => rw [hl] at hy; exact nomatch hy231232theorem next_lt {v : Nat} (hv : v < n) (hg : good edge n v = true) : next edge n v < n := (next_spec hv hg).1233234/-- The greedy walk from a good vertex stays good. -/235theorem iter_good {v : Nat} (hv : v < n) (hg : good edge n v = true) :236    ∀ k, iter (next edge n) v k < n ∧ good edge n (iter (next edge n) v k) = true237  | 0 => ⟨hv, hg⟩238  | k + 1 =>239    have ih := iter_good hv hg k240    have s := next_spec ih.1 ih.2241    ⟨s.1, s.2.2⟩242243/-- The greedy step on good vertices and the identity elsewhere, so that it maps `[0, n)` into itself. -/244def nextGood (edge : Nat → Nat → Bool) (n : Nat) (y : Nat) : Nat := cond (good edge n y) (next edge n y) y245246theorem nextGood_lt {y : Nat} (hy : y < n) : nextGood edge n y < n := by247  unfold nextGood248  cases hgy : good edge n y249  · exact hy250  · exact next_lt hy hgy251252theorem iterGood {v : Nat} (hv : v < n) (hg : good edge n v = true) :253    ∀ j, good edge n (iter (nextGood edge n) v j) = true ∧ iter (nextGood edge n) v j < n254  | 0 => ⟨hg, hv⟩255  | j + 1 => by256    have ih := iterGood hv hg j257    show good edge n (nextGood edge n (iter (nextGood edge n) v j)) = true ∧ nextGood edge n (iter (nextGood edge n) v j) < n258    have e : nextGood edge n (iter (nextGood edge n) v j) = next edge n (iter (nextGood edge n) v j) := by259      show cond (good edge n (iter (nextGood edge n) v j)) (next edge n (iter (nextGood edge n) v j))260          (iter (nextGood edge n) v j) = next edge n (iter (nextGood edge n) v j)261      rw [ih.1]; rfl262    rw [e]263    exact ⟨(next_spec ih.2 ih.1).2.2, (next_spec ih.2 ih.1).1⟩264265theorem iterGood_edge {v : Nat} (hv : v < n) (hg : good edge n v = true) (k : Nat) :266    edge (iter (nextGood edge n) v k) (iter (nextGood edge n) v (k + 1)) = true := by267  have gk := iterGood hv hg k268  show edge (iter (nextGood edge n) v k) (nextGood edge n (iter (nextGood edge n) v k)) = true269  have e : nextGood edge n (iter (nextGood edge n) v k) = next edge n (iter (nextGood edge n) v k) := by270    show cond (good edge n (iter (nextGood edge n) v k)) (next edge n (iter (nextGood edge n) v k))271        (iter (nextGood edge n) v k) = next edge n (iter (nextGood edge n) v k)272    rw [gk.1]; rfl273  rw [e]274  exact (next_spec gk.2 gk.1).2.1275276/-- 5:E6 (Theorem periodic-dbe, the periodic walk) — if the digraph on `[0, n)` has walks of every length, it has an277infinite walk `w` that is periodic with period `m`, `1 ≤ m ≤ n`: every step is an edge and `w (i + m) = w i`. The278walk is the greedy walk in the sub-digraph of vertices good for every length, read from its first return. -/279theorem periodic_walk (h : ∀ k, ∃ v, v < n ∧ walks edge n v k = true) :280    ∃ w : Nat → Nat, ∃ m, 0 < m ∧ m ≤ n ∧ (∀ i, w i < n) ∧ (∀ i, edge (w i) (w (i + 1)) = true) ∧ ∀ i, w (i + m) = w i :=281  match exists_allGood h with282  | ⟨v, hv, hg⟩ =>283    have hgood : good edge n v = true := hg _284    have hstep : ∀ y, y < n → nextGood edge n y < n := fun y hy => nextGood_lt hy285    match eventually_periodic (nextGood edge n) n hstep v hv with286    | ⟨i₀, p, hp, hpn, hper⟩ =>287      ⟨fun i => iter (nextGood edge n) v (i₀ + i), p, hp, hpn,288       fun i => iter_lt _ hstep hv _,289       fun i => by290         show edge (iter (nextGood edge n) v (i₀ + i)) (iter (nextGood edge n) v (i₀ + (i + 1))) = true291         rw [← Nat.add_assoc]292         exact iterGood_edge hv hgood (i₀ + i),293       fun i => by294         show iter (nextGood edge n) v (i₀ + (i + p)) = iter (nextGood edge n) v (i₀ + i)295         rw [← Nat.add_assoc]; exact hper i⟩296297end FRC.Transfer298299