Deterministic Search for a Fixed Expander Seed
Lax920634.SeedSearch · concepts/Lax920634/SeedSearch.lean · lax-920634
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Thirty permutations of a finite set are sufficient to make every set of at most half its size escape by at least a tenth through some permutation. A seed can therefore be found by checking finite tables in numerical order. This search is used at one fixed size, independent of the requested output order. Its cost is a constant in the construction of the infinite family.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Fin |
| 2 | import Mathlib.Data.Fintype.Powerset |
| 3 | import Mathlib.Data.List.FinRange |
| 4 | import Mathlib.Data.Nat.Find |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Deterministic Search for a Fixed Expander Seed |
| 9 | type: definition |
| 10 | --- |
| 11 | Thirty permutations of a finite set are sufficient to make every set of at |
| 12 | most half its size escape by at least a tenth through some permutation. |
| 13 | A seed can therefore be found by checking finite tables in numerical order. |
| 14 | This search is used at one fixed size, independent of the requested output |
| 15 | order. Its cost is a constant in the construction of the infinite family. |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | Candidate tables are numbered by their base- digits. The test is a |
| 20 | finite predicate about injectivity and cardinalities. The selected table |
| 21 | is the first successful candidate, with identity as a total default; |
| 22 | the correctness proof shows that the default is never needed. |
| 23 | The search is implemented by a finite list scan and uses no choice operation. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax920634.SeedSearch |
| 27 | |
| 28 | open Function |
| 29 | |
| 30 | /-- A table of thirty maps on a numbered finite vertex set. -/ |
| 31 | abbrev Table (n : ℕ) := Fin 30 → Fin n → Fin n |
| 32 | |
| 33 | /-- The number of vertices of `S` whose image lies outside `S`. -/ |
| 34 | def escape {n : ℕ} (f : Fin n → Fin n) (S : Finset (Fin n)) : ℕ := |
| 35 | (S.filter fun v => f v ∉ S).card |
| 36 | |
| 37 | /-- Each row is a permutation, and some row moves at least a tenth of each small set out. -/ |
| 38 | abbrev GoodTable {n : ℕ} (T : Table n) : Prop := |
| 39 | (∀ i, Bijective (T i)) ∧ |
| 40 | ∀ S : Finset (Fin n), 2 * S.card ≤ n → |
| 41 | ∃ i : Fin 30, S.card ≤ 10 * escape (T i) S |
| 42 | |
| 43 | /-- The candidate table represented by a base-`n` integer. -/ |
| 44 | def decode (n : ℕ) (code : Fin (n ^ (30 * n))) : Table n := |
| 45 | fun i v => finFunctionFinEquiv.symm code (finProdFinEquiv (i, v)) |
| 46 | |
| 47 | /-- All candidate codes in increasing numerical order. -/ |
| 48 | def candidates (n : ℕ) : List (Fin (n ^ (30 * n))) := List.finRange _ |
| 49 | |
| 50 | /-- The first expanding permutation table found by the finite deterministic scan. -/ |
| 51 | def selectedTable (n : ℕ) : Table n := |
| 52 | (((candidates n).find? fun code => decide (GoodTable (decode n code))).map |
| 53 | (decode n)).getD (fun _ v => v) |
| 54 | |
| 55 | /-- Find the inverse image by scanning a numbered finite vertex set. -/ |
| 56 | def inverse {n : ℕ} (f : Fin n → Fin n) (v : Fin n) : Fin n := |
| 57 | ((List.finRange n).find? fun u => decide (f u = v)).getD v |
| 58 | |
| 59 | /-- A fixed powering exponent sufficient for the lazy permutation seed. -/ |
| 60 | def poweringExponent : ℕ := 5760000 |
| 61 | |
| 62 | /-- The fixed degree of the powered seed. -/ |
| 63 | def seedDegree : ℕ := 120 ^ poweringExponent |
| 64 | |
| 65 | /-- The fixed number of seed vertices, the fourth power of its degree. -/ |
| 66 | def seedOrder : ℕ := seedDegree ^ 4 |
| 67 | |
| 68 | end Lax920634.SeedSearch |
| 69 |
Formalization notes
Candidate tables are numbered by their base- digits. The test is a finite predicate about injectivity and cardinalities. The selected table is the first successful candidate, with identity as a total default; the correctness proof shows that the default is never needed. The search is implemented by a finite list scan and uses no choice operation.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments