Checked twin-contraction reconstruction
Lax235315.TwinReconstruction · concepts/Lax235315/TwinReconstruction.lean · lax-235315
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A reconstruction starts with an order on a small remaining ground set and undoes checked contraction rounds. In each round it inserts removed ground vertices next to twins over the retained set-side representatives. Every old set-side vertex has a retained representative whose neighborhood differs on at most k active ground vertices.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | import Mathlib.Data.Set.Card |
| 3 | import Mathlib.Data.Set.SymmDiff |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Checked twin-contraction reconstruction |
| 8 | type: definition |
| 9 | --- |
| 10 | A reconstruction starts with an order on a small remaining ground set and |
| 11 | undoes checked contraction rounds. In each round it inserts removed ground |
| 12 | vertices next to twins over the retained set-side representatives. Every |
| 13 | old set-side vertex has a retained representative whose neighborhood differs |
| 14 | on at most k active ground vertices. |
| 15 | |
| 16 | # Formalization notes |
| 17 | |
| 18 | The two sides are subsets of the same canonical vertex type, as in the |
| 19 | graph-neighborhood bipartite representation. A round records concrete lists, |
| 20 | actual adjacent twin insertions, and the checked symmetric-difference bound. |
| 21 | It does not assume any crossing-number conclusion. |
| 22 | The run relation describes deterministic reconstruction certificates. A |
| 23 | separate implementation proof must show that the machine produces one. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax235315.TwinReconstruction |
| 27 | open scoped symmDiff |
| 28 | |
| 29 | /-- Insert x immediately after the first occurrence of a, if a is present. -/ |
| 30 | def insertAfter {n : ℕ} (a x : Fin n) : List (Fin n) → List (Fin n) |
| 31 | | [] => [] |
| 32 | | b :: rest => if b = a then b :: x :: rest else b :: insertAfter a x rest |
| 33 | |
| 34 | /-- A list contains each member of A exactly once and contains no other vertex. -/ |
| 35 | def Enumerates {n : ℕ} (A : Set (Fin n)) (l : List (Fin n)) : Prop := |
| 36 | l.Nodup ∧ ∀ v : Fin n, v ∈ l ↔ v ∈ A |
| 37 | |
| 38 | /-- A sequence of insertions of fresh vertices next to twins over B. -/ |
| 39 | inductive TwinExpansion {n : ℕ} (G : SimpleGraph (Fin n)) (B : Set (Fin n)) : |
| 40 | List (Fin n) → List (Fin n) → Prop |
| 41 | /-- No insertion is needed to expand a list to itself. -/ |
| 42 | | refl (l : List (Fin n)) : TwinExpansion G B l l |
| 43 | /-- Restore a fresh vertex immediately after a present twin. -/ |
| 44 | | insert {small current : List (Fin n)} {a x : Fin n} |
| 45 | (previous : TwinExpansion G B small current) |
| 46 | (present : a ∈ current) (fresh : x ∉ current) |
| 47 | (twins : ∀ b ∈ B, (G.Adj b a ↔ G.Adj b x)) : |
| 48 | TwinExpansion G B small (insertAfter a x current) |
| 49 | |
| 50 | /-- The data checked when one contraction round is reconstructed. -/ |
| 51 | structure Reduction {n : ℕ} (G : SimpleGraph (Fin n)) (k : ℕ) |
| 52 | (A B A' B' : Set (Fin n)) (small big : List (Fin n)) where |
| 53 | /-- The contracted list enumerates the retained ground vertices. -/ |
| 54 | small_enumerates : Enumerates A' small |
| 55 | /-- The reconstructed list enumerates the preceding ground vertices. -/ |
| 56 | big_enumerates : Enumerates A big |
| 57 | /-- Reconstruction uses only genuine twin insertions over B'. -/ |
| 58 | expands : TwinExpansion G B' small big |
| 59 | /-- The representative assigned to each set-side vertex. -/ |
| 60 | representative : Fin n → Fin n |
| 61 | /-- Representatives of active vertices belong to the retained side. -/ |
| 62 | representative_mem : ∀ b ∈ B, representative b ∈ B' |
| 63 | /-- The checked distance to each representative on the active ground set. -/ |
| 64 | near : ∀ b ∈ B, |
| 65 | ((G.neighborSet b ∩ A) ∆ (G.neighborSet (representative b) ∩ A)).ncard ≤ k |
| 66 | |
| 67 | /-- A complete reconstruction, indexed by the number of undone rounds. -/ |
| 68 | inductive Run {n : ℕ} (G : SimpleGraph (Fin n)) (k q : ℕ) : |
| 69 | ℕ → Set (Fin n) → Set (Fin n) → List (Fin n) → Prop |
| 70 | /-- Start with any order on a ground set of at most q vertices. -/ |
| 71 | | base {A B : Set (Fin n)} {l : List (Fin n)} |
| 72 | (enumerates : Enumerates A l) (small : A.ncard ≤ q) : |
| 73 | Run G k q 0 A B l |
| 74 | /-- Undo one checked contraction and continue the recorded reconstruction. -/ |
| 75 | | step {rounds : ℕ} {A B A' B' : Set (Fin n)} |
| 76 | {small big : List (Fin n)} |
| 77 | (reduction : Reduction G k A B A' B' small big) |
| 78 | (tail : Run G k q rounds A' B' small) : |
| 79 | Run G k q (rounds + 1) A B big |
| 80 | |
| 81 | end Lax235315.TwinReconstruction |
| 82 |
Formalization notes
The two sides are subsets of the same canonical vertex type, as in the graph-neighborhood bipartite representation. A round records concrete lists, actual adjacent twin insertions, and the checked symmetric-difference bound. It does not assume any crossing-number conclusion. The run relation describes deterministic reconstruction certificates. A separate implementation proof must show that the machine produces one.
Builds on
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments