-
An Introduction to Lax
-
def
Lax242665.Primesp. 1Prime numbers
A natural number greater than 1 is prime if it is divisible only by 1 and by itself.
1 import Mathlib.Data.Nat.Notation 2 … module docstring, 8 lines 11 12 namespace Lax242665.Primes 13 14 /-- `n` is prime: it is greater than 1, and every divisor `d` of `n` is 15 `1` or `n` itself. -/ 16 def Prime (n : ℕ) : Prop := 17 1 < n ∧ ∀ d : ℕ, d ∣ n → d = 1 ∨ d = n 18 19 end Lax242665.Primes 20 -
thm✓
Lax242665.InfinitelyManyPrimesp. 1There are infinitely many primes
For every natural number there is a prime number .
1 import Lax242665.Primes 2 … module docstring, 7 lines 10 11 namespace Lax242665.InfinitelyManyPrimes 12 13 /-- Beyond every natural number `n` lies a prime `p`. -/ 14 axiom exists_prime_gt : ∀ n : ℕ, ∃ p : ℕ, Primes.Prime p ∧ n < p 15 16 end Lax242665.InfinitelyManyPrimes 17 -
def
Lax48.TwinWidthp. 2Twin-width
A partition sequence of a finite simple graph G is a sequence of partitions of its vertex set that starts at the partition into singletons, merges two parts into one at every step, and ends at the partition with a single part. Two parts of a same partition are homogeneous if either every pair of vertices across them is adjacent or none is; two non-homogeneous parts are red-adjacent. The red degree of a part is the number of other parts of its partition that are red-adjacent to it.
The twin-width of G is the least d such that G has a partition sequence in which every part of every partition has red degree at most d.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 import Mathlib.Data.Set.Card 3 import Mathlib.Data.Nat.Lattice 4 … module docstring, 25 lines 30 31 namespace Lax48.TwinWidth 32 33 /-- Two vertex sets are homogeneous in `G`: either every pair of vertices 34 across them is adjacent, or none is. -/ 35 def Homogeneous {V : Type} (G : SimpleGraph V) (A B : Finset V) : Prop := 36 (∀ a ∈ A, ∀ b ∈ B, G.Adj a b) ∨ (∀ a ∈ A, ∀ b ∈ B, ¬ G.Adj a b) 37 38 /-- The red degree of a part `A` in a family of parts `P`: the number of 39 other parts of `P` that are not homogeneous with `A`. -/ 40 noncomputable def redDegree {V : Type} (G : SimpleGraph V) 41 (P : Finset (Finset V)) (A : Finset V) : ℕ := 42 {B | B ∈ P ∧ B ≠ A ∧ ¬ Homogeneous G A B}.ncard 43 44 /-- The partition of a finite vertex type into singletons. -/ 45 def singletonPartition (V : Type) [Fintype V] [DecidableEq V] : 46 Finset (Finset V) := 47 Finset.univ.image fun v : V => ({v} : Finset V) 48 49 /-- A partition sequence of `G` in which every part has red degree at most 50 `d`: starting from the singleton partition, each step merges two parts into 51 one, until a single part remains. -/ 52 structure PartitionSequence {V : Type} [Fintype V] [DecidableEq V] 53 (G : SimpleGraph V) (d : ℕ) where 54 /-- The number of merge steps. -/ 55 stepCount : ℕ 56 /-- The partition after each number of merge steps. -/ 57 partition : ℕ → Finset (Finset V) 58 /-- The sequence starts at the singleton partition. -/ 59 starts : partition 0 = singletonPartition V 60 /-- The sequence ends with a single part. -/ 61 ends : (partition stepCount).card ≤ 1 62 /-- Each step merges two distinct parts into one and keeps all other 63 parts. -/ 64 step_merges : 65 ∀ i, i < stepCount → ∃ A ∈ partition i, ∃ B ∈ partition i, A ≠ B ∧ 66 partition (i + 1) = insert (A ∪ B) (((partition i).erase A).erase B) 67 /-- Every part of every partition in the sequence has red degree at most 68 `d`. -/ 69 redDegree_le : 70 ∀ i, i ≤ stepCount → ∀ ⦃A⦄, A ∈ partition i → 71 redDegree G (partition i) A ≤ d 72 73 /-- `G` has a partition sequence in which every part has red degree at most 74 `d`. -/ 75 def HasTwinWidthAtMost {V : Type} [Fintype V] [DecidableEq V] 76 (G : SimpleGraph V) (d : ℕ) : Prop := 77 Nonempty (PartitionSequence G d) 78 79 /-- The twin-width of a finite simple graph: the least `d` such that the 80 graph has a partition sequence in which every part has red degree at most 81 `d`. -/ 82 noncomputable def twinWidth {V : Type} [Fintype V] [DecidableEq V] 83 (G : SimpleGraph V) : ℕ := 84 sInf {d | HasTwinWidthAtMost G d} 85 86 end Lax48.TwinWidth 87 -
def
Lax12.NowhereDenseClassesp. 2Nowhere dense graph classes
A graph H is a depth-r minor of a graph G if H can be obtained from G by deleting vertices and edges and contracting pairwise disjoint connected subgraphs of radius at most r. A graph class is nowhere dense if for every depth r there is a t such that no member has the complete graph on t vertices as a depth-r minor.
The source lecture notes give these as Definitions 2.3 and 2.6 of Chapter 1 (2019/20 edition), writing H ⪯r G for the depth-r minor relation. Nowhere denseness is stated there as ωr(C) < ∞ for every r, with the excluded-clique form used here spelled out immediately after as an equivalent.
1 import Lax12.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 3 … module docstring, 29 lines 33 34 namespace Lax12.NowhereDenseClasses 35 36 open Lax12.GraphClasses 37 38 /-- A model of `H` as a depth-`r` minor of `G`: pairwise disjoint branch 39 sets, each spanned by walks of length at most `r` from a center vertex 40 (hence connected of radius at most `r`), with an edge of `G` between the 41 branch sets of any two adjacent vertices of `H`. -/ 42 structure ShallowMinorModel {V W : Type*} (r : ℕ) (H : SimpleGraph W) 43 (G : SimpleGraph V) where 44 /-- The branch set of each vertex of `H`. -/ 45 branch : W → Set V 46 /-- The center of each branch set. -/ 47 center : W → V 48 /-- Centers lie in their branch sets (so branch sets are nonempty). -/ 49 center_mem : ∀ u, center u ∈ branch u 50 /-- Distinct branch sets are disjoint. -/ 51 disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v) 52 /-- Every vertex of a branch set is reached from the center by a walk 53 of length at most `r` inside the branch set. -/ 54 radius_le : ∀ u, ∀ x ∈ branch u, ∃ w : G.Walk (center u) x, 55 w.length ≤ r ∧ ∀ y ∈ w.support, y ∈ branch u 56 /-- Adjacent vertices of `H` have adjacent branch sets. -/ 57 adj : ∀ u v, H.Adj u v → ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y 58 59 /-- `H` is a minor of `G` at depth `r`. -/ 60 def HasShallowMinor {V W : Type*} (G : SimpleGraph V) (r : ℕ) 61 (H : SimpleGraph W) : Prop := 62 Nonempty (ShallowMinorModel r H G) 63 64 /-- A graph class is nowhere dense if for every depth `r` some complete 65 graph is not a depth-`r` minor of any member. -/ 66 def NowhereDense (C : GraphClass) : Prop := 67 ∀ r : ℕ, ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 68 ¬ HasShallowMinor G r (⊤ : SimpleGraph (Fin t)) 69 70 end Lax12.NowhereDenseClasses 71 -
def
Lax67.Ramp. 2The word RAM
A word RAM is a random access machine whose writable memory consists of cells holding natural numbers below . The word length is a parameter; one finite program serves all word lengths. Input is a read-only finite array supplied at initialization, also accessible as a sequential tape. Output is an append-only tape. Working memory starts at zero and output starts empty.
The input interface has four operations. consumes the next entry of the sequential tape into cell , halting if the tape is empty. branches on tape emptiness without consuming input. writes the original input length into cell . reads the original input at the index in cell into cell , returning zero outside the input. Indexed access never consumes the sequential tape, and sequential reads never change the original input. Zero is ordinary data, not an end marker. Each operation costs one instruction. No length header or other framing is added to the supplied list.
Arithmetic results, input values and lengths, output values, and data-memory addresses are reduced modulo . Subtraction is truncated at zero, and division is integer division with . Input indices are words too. Program labels and the program counter are natural numbers and are not reduced modulo .
1 import Mathlib.Data.List.Basic 2 … module docstring, 110 lines 113 114 namespace Lax67.Ram 115 116 /-- An instruction. Every number naming a cell is read, except that 117 the first one names the destination for instructions that write a cell, 118 and the cell holding the destination address for `store`. `set` carries 119 a literal value; `jump`, `jzero`, and `jeof` carry program labels, 120 which are not data-memory addresses. -/ 121 inductive Instr 122 /-- Set cell `a` to the literal `n`. -/ 123 | set (a n : ℕ) 124 /-- Set cell `a` to the contents of the cell whose address cell `b` 125 holds. -/ 126 | load (a b : ℕ) 127 /-- Set the cell whose address cell `a` holds to the contents of cell 128 `b`. -/ 129 | store (a b : ℕ) 130 /-- Set cell `a` to the sum of cells `b` and `c`, wrapping around 131 modulo `2 ^ w`. -/ 132 | add (a b c : ℕ) 133 /-- Set cell `a` to the difference of cells `b` and `c`, truncated at 134 zero rather than wrapping around. -/ 135 | sub (a b c : ℕ) 136 /-- Set cell `a` to the product of cells `b` and `c`, wrapping around 137 modulo `2 ^ w`. -/ 138 | mul (a b c : ℕ) 139 /-- Set cell `a` to the quotient of cells `b` and `c`, rounding 140 towards zero; division by zero yields zero. -/ 141 | div (a b c : ℕ) 142 /-- Set cell `a` to the bitwise conjunction of cells `b` and `c`. -/ 143 | and (a b c : ℕ) 144 /-- Set cell `a` to cell `b` shifted left by the number of bits cell 145 `c` holds, wrapping around modulo `2 ^ w`; a shift by `w` or more 146 yields zero. -/ 147 | shiftl (a b c : ℕ) 148 /-- Set cell `a` to the bitwise complement `2 ^ w - 1 - m[b]` of cell 149 `b` within the word length. -/ 150 | not (a b : ℕ) 151 /-- Continue at instruction `l`. -/ 152 | jump (l : ℕ) 153 /-- Continue at instruction `l` if cell `a` is zero. -/ 154 | jzero (a l : ℕ) 155 /-- Continue at instruction `l` exactly when the remaining input tape 156 is empty. This test does not consume input. -/ 157 | jeof (l : ℕ) 158 /-- Write the original input length, reduced to a word, into cell `a`. -/ 159 | inputLength (a : ℕ) 160 /-- Read original input at the word index in cell `b` into cell `a`, 161 returning zero outside the input. Read the index before writing `a`, 162 even when the two cell addresses coincide. Do not consume input. -/ 163 | inputLoad (a b : ℕ) 164 /-- Halt. -/ 165 | halt 166 /-- Read the next number of the input tape into cell `a`, or halt if 167 the tape is exhausted. -/ 168 | read (a : ℕ) 169 /-- Append the contents of cell `a` to the output tape. -/ 170 | write (a : ℕ) 171 172 /-- A program: a finite sequence of instructions, numbered from `0`. -/ 173 abbrev Program : Type := List Instr 174 175 /-- A machine state: the program counter, the contents of every memory 176 cell, the immutable original input array, the remaining sequential input 177 tape, and the output tape written so far. -/ 178 structure State where 179 /-- The number of the instruction to be executed next. -/ 180 pc : ℕ 181 /-- The contents of the memory cells; only the cells with number below 182 `2 ^ w` are ever addressed. -/ 183 mem : ℕ → ℕ 184 /-- The original read-only input, unchanged by every instruction. -/ 185 input : List ℕ 186 /-- The numbers still to be read from the input tape. -/ 187 inp : List ℕ 188 /-- The numbers written to the output tape so far. -/ 189 out : List ℕ 190 191 /-- The memory `m` with cell `a` set to `v`, at word length `w`: the 192 address and the value written are both taken modulo `2 ^ w`. -/ 193 def setCell (w : ℕ) (m : ℕ → ℕ) (a v : ℕ) : ℕ → ℕ := 194 fun b => if b = a % 2 ^ w then v % 2 ^ w else m b 195 196 /-- The effect of one instruction on the state at word length `w`, or 197 `none` if it halts the machine, which a `halt` instruction and a read 198 from an exhausted input tape do. Data values, input indices, and 199 data-memory addresses are reduced modulo `2 ^ w`; program labels and 200 the counter are not. -/ 201 def Instr.effect (w : ℕ) : Instr → State → Option State 202 | set a n, s => some { s with pc := s.pc + 1, mem := setCell w s.mem a n } 203 | load a b, s => 204 some 205 { s with 206 pc := s.pc + 1 207 mem := setCell w s.mem a (s.mem (s.mem (b % 2 ^ w) % 2 ^ w)) } 208 | store a b, s => 209 some 210 { s with 211 pc := s.pc + 1 212 mem := setCell w s.mem (s.mem (a % 2 ^ w)) (s.mem (b % 2 ^ w)) } 213 | add a b c, s => 214 some 215 { s with 216 pc := s.pc + 1 217 mem := setCell w s.mem a (s.mem (b % 2 ^ w) + s.mem (c % 2 ^ w)) } 218 | sub a b c, s => 219 some 220 { s with 221 pc := s.pc + 1 222 mem := setCell w s.mem a (s.mem (b % 2 ^ w) - s.mem (c % 2 ^ w)) } 223 | mul a b c, s => 224 some 225 { s with 226 pc := s.pc + 1 227 mem := setCell w s.mem a (s.mem (b % 2 ^ w) * s.mem (c % 2 ^ w)) } 228 | div a b c, s => 229 some 230 { s with 231 pc := s.pc + 1 232 mem := setCell w s.mem a (s.mem (b % 2 ^ w) / s.mem (c % 2 ^ w)) } 233 | and a b c, s => 234 some 235 { s with 236 pc := s.pc + 1 237 mem := setCell w s.mem a (Nat.land (s.mem (b % 2 ^ w)) (s.mem (c % 2 ^ w))) } 238 | shiftl a b c, s => 239 some 240 { s with 241 pc := s.pc + 1 242 mem := setCell w s.mem a (s.mem (b % 2 ^ w) * 2 ^ s.mem (c % 2 ^ w)) } 243 | not a b, s => 244 some 245 { s with 246 pc := s.pc + 1 247 mem := setCell w s.mem a (2 ^ w - 1 - s.mem (b % 2 ^ w)) } 248 | jump l, s => some { s with pc := l } 249 | jzero a l, s => some { s with pc := if s.mem (a % 2 ^ w) = 0 then l else s.pc + 1 } 250 | jeof l, s => some { s with pc := if s.inp.isEmpty then l else s.pc + 1 } 251 | inputLength a, s => 252 some { s with pc := s.pc + 1, mem := setCell w s.mem a s.input.length } 253 | inputLoad a b, s => 254 some { s with 255 pc := s.pc + 1 256 mem := setCell w s.mem a (s.input[s.mem (b % 2 ^ w) % 2 ^ w]?.getD 0) } 257 | halt, _ => none 258 | read a, s => 259 s.inp.head?.map fun v => 260 { s with pc := s.pc + 1, mem := setCell w s.mem a v, inp := s.inp.tail } 261 | write a, s => 262 some { s with pc := s.pc + 1, out := s.out ++ [s.mem (a % 2 ^ w) % 2 ^ w] } 263 264 /-- One step of the machine at word length `w`: fetch the instruction 265 the program counter points at and execute it. The result is `none` if 266 the machine has halted, which also happens when the program counter has 267 run past the program. -/ 268 def step (w : ℕ) (p : Program) (s : State) : Option State := 269 p[s.pc]?.bind fun i => i.effect w s 270 271 /-- The state after `t` successful transitions at word length `w`, or 272 `none` if one of those transitions terminates. This auxiliary count does 273 not include a fetched terminal instruction; `RunsTo` charges that too. -/ 274 def run (w : ℕ) (p : Program) : ℕ → State → Option State 275 | 0, s => some s 276 | t + 1, s => (step w p s).bind (run w p t) 277 278 /-- The initial state on input `x`: program counter zero, all memory 279 cells zero, the original input array and its sequential tape both `x`, 280 and the output tape empty. -/ 281 def initState (x : List ℕ) : State where 282 pc := 0 283 mem := fun _ => 0 284 input := x 285 inp := x 286 out := [] 287 288 /-- Cost of termination at `s`, when `step w p s = none`: a fetched 289 terminal instruction costs one, while an out-of-range program counter 290 costs zero because there is no instruction to execute. -/ 291 def terminalCost (p : Program) (s : State) : ℕ := 292 if s.pc < p.length then 1 else 0 293 294 /-- Started on input `x` at word length `w`, the machine executes 295 exactly `t` instructions and then halts, having written the word `y` to 296 its output tape. -/ 297 def RunsTo (w : ℕ) (p : Program) (x y : List ℕ) (t : ℕ) : Prop := 298 ∃ (k : ℕ) (s : State), run w p k (initState x) = some s ∧ 299 step w p s = none ∧ s.out = y ∧ t = k + terminalCost p s 300 301 end Lax67.Ram 302 -
no assumptions
Euclid's argument: the smallest prime factor of cannot be at most , because then would divide and hence divide .
-
lem✓
Lax242665.OddPrimesp. 2Every prime other than 2 is odd
Every prime number is odd.
1 import Mathlib.Algebra.Ring.Parity 2 import Lax242665.Primes 3 … module docstring, 7 lines 11 12 namespace Lax242665.OddPrimes 13 14 /-- A prime `p` other than `2` is odd. -/ 15 axiom odd_of_prime : ∀ p : ℕ, Primes.Prime p → p ≠ 2 → Odd p 16 17 end Lax242665.OddPrimes 18 -
no assumptions
An even prime is divisible by , so is or the prime itself.
-
lem×
Lax242665.BertrandPostulatep. 3Bertrand's postulate
For every natural number there is a prime number with .
1 import Lax242665.Primes 2 … module docstring, 8 lines 11 12 namespace Lax242665.BertrandPostulate 13 14 /-- For every `n ≥ 1` there is a prime `p` with `n < p ≤ 2n`. -/ 15 axiom exists_prime_between : 16 ∀ n : ℕ, 1 ≤ n → ∃ p : ℕ, Primes.Prime p ∧ n < p ∧ p ≤ 2 * n 17 18 end Lax242665.BertrandPostulate 19 -
thm×
Lax242665.OddPrimeBetweenp. 3An odd prime between n and 2n
For every natural number there is an odd prime number with .
1 import Mathlib.Algebra.Ring.Parity 2 import Lax242665.Primes 3 … module docstring, 8 lines 12 13 namespace Lax242665.OddPrimeBetween 14 15 /-- For every `n ≥ 2` there is an odd prime `p` with `n < p ≤ 2n`. -/ 16 axiom exists_odd_prime_between : 17 ∀ n : ℕ, 2 ≤ n → ∃ p : ℕ, Primes.Prime p ∧ Odd p ∧ n < p ∧ p ≤ 2 * n 18 19 end Lax242665.OddPrimeBetween 20 -
Bertrand's postulate gives a prime with . Since , this prime is not , hence odd.