Reconstruction over finite alphabets
Lax100001.Alphabet · concepts/Lax100001/Alphabet.lean · lax-100001
Natural Language Statement
Theorem
A binary reconstruction rule gives a rule for every finite alphabet. The lifted rule first asks one singleton query per letter and then runs the binary rule on every pair projection. The proof bounds its cost by the sum of the actual binary run lengths. A uniform bound for binary inputs through a given length gives the stated finite-alphabet bound at that length.
Concept map
Preparing this local graph with the browser’s fonts…
Evidence
In the paper
- page 18 of this submission's paper
Lean source
| 1 | /- |
| 2 | Copyright (c) 2026 Anonymous. All rights reserved. |
| 3 | Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | Authors: ChatGPT (OpenAI), Claude (Anthropic) |
| 5 | -/ |
| 6 | import Lax100001.Counting |
| 7 | import Mathlib.Data.Fintype.Card |
| 8 | |
| 9 | /-! |
| 10 | --- |
| 11 | title: Reconstruction over finite alphabets |
| 12 | type: theorem |
| 13 | --- |
| 14 | A binary reconstruction rule gives a rule for every finite alphabet. The lifted rule first |
| 15 | asks one singleton query per letter and then runs the binary rule on every pair projection. |
| 16 | The proof bounds its cost by the sum of the actual binary run lengths. A uniform bound for |
| 17 | binary inputs through a given length gives the stated finite-alphabet bound at that length. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax100001.Alphabet |
| 21 | |
| 22 | open Counting |
| 23 | |
| 24 | variable {α : Type} [DecidableEq α] |
| 25 | |
| 26 | /-- Keep the letters `a` and `b`, and write them as binary letters. -/ |
| 27 | def pairProjection (a b : α) (w : Word α) : Word := |
| 28 | w.filterMap fun x => if x = a then some false else if x = b then some true else none |
| 29 | |
| 30 | /-- Replace the binary letters by `a` and `b`. -/ |
| 31 | def encode (a b : α) (p : Word) : Word α := |
| 32 | p.map fun c => if c then b else a |
| 33 | |
| 34 | /-- Enumerate one orientation of every pair of positions in a list. -/ |
| 35 | def pairs : List α → List (α × α) |
| 36 | | [] => [] |
| 37 | | a :: l => l.map (a, ·) ++ pairs l |
| 38 | |
| 39 | end Lax100001.Alphabet |
| 40 | |
| 41 | namespace Lax100001.Alphabet |
| 42 | |
| 43 | open Counting |
| 44 | |
| 45 | /-- Binary rules lift to finite alphabets through singleton counts and binary projections. |
| 46 | The cost is the sum of the binary run lengths and one query per letter. -/ |
| 47 | axiom finite_alphabet_reduction (α : Type) [Fintype α] [DecidableEq α] |
| 48 | (r : Rule) (H : Word → List Exchange) (hr : ∀ v, IsRun r v (H v)) |
| 49 | (allowed : Word → Prop) (lifted : Word α → Prop) |
| 50 | (hqueries : ∀ v, ∀ e ∈ H v, allowed e.query) |
| 51 | (hsingle : ∀ a, lifted [a]) |
| 52 | (hencode : ∀ a b, a ≠ b → ∀ q, allowed q → lifted (encode a b q)) : |
| 53 | ∃ rule : Rule α, ∀ w : Word α, ∃ history : List (Exchange α), |
| 54 | IsRun rule w history ∧ (∀ e ∈ history, lifted e.query) ∧ |
| 55 | history.length = Fintype.card α + |
| 56 | ((pairs (Finset.univ.toList : List α)).map |
| 57 | (fun p => (H (pairProjection p.1 p.2 w)).length)).sum |
| 58 | |
| 59 | /-- A whole-length monotone binary bound gives a finite-alphabet bound. -/ |
| 60 | axiom finite_alphabet_bound (α : Type) [Fintype α] [DecidableEq α] |
| 61 | (r : Rule) (H : Word → List Exchange) (hr : ∀ v, IsRun r v (H v)) |
| 62 | (allowed : Word → Prop) (lifted : Word α → Prop) |
| 63 | (hqueries : ∀ v, ∀ e ∈ H v, allowed e.query) |
| 64 | (hsingle : ∀ a, lifted [a]) |
| 65 | (hencode : ∀ a b, a ≠ b → ∀ q, allowed q → lifted (encode a b q)) |
| 66 | (Q : ℕ → ℕ) (hQ : Monotone Q) (hcost : ∀ v, (H v).length ≤ Q v.length) : |
| 67 | ∃ rule : Rule α, ∀ w : Word α, ∃ history : List (Exchange α), |
| 68 | IsRun rule w history ∧ (∀ e ∈ history, lifted e.query) ∧ |
| 69 | history.length ≤ Fintype.card α + (Fintype.card α).choose 2 * Q w.length |
| 70 | |
| 71 | end Lax100001.Alphabet |
| 72 | |
| 73 | namespace Lax100001.Alphabet |
| 74 | |
| 75 | open Counting |
| 76 | |
| 77 | /-- A uniform binary bound through length `n` bounds every lifted run through length `n`. -/ |
| 78 | axiom finite_alphabet_envelope (α : Type) [Fintype α] [DecidableEq α] |
| 79 | (r : Rule) (H : Word → List Exchange) (hr : ∀ v, IsRun r v (H v)) |
| 80 | (allowed : Word → Prop) (lifted : Word α → Prop) |
| 81 | (hqueries : ∀ v, ∀ e ∈ H v, allowed e.query) |
| 82 | (hsingle : ∀ a, lifted [a]) |
| 83 | (hencode : ∀ a b, a ≠ b → ∀ q, allowed q → lifted (encode a b q)) |
| 84 | (n q : ℕ) (hcost : ∀ v, v.length ≤ n → (H v).length ≤ q) : |
| 85 | ∃ rule : Rule α, ∀ w : Word α, w.length ≤ n → ∃ history : List (Exchange α), |
| 86 | IsRun rule w history ∧ (∀ e ∈ history, lifted e.query) ∧ |
| 87 | history.length ≤ Fintype.card α + (Fintype.card α).choose 2 * q |
| 88 | |
| 89 | end Lax100001.Alphabet |
| 90 |