BitstringEncoding.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

24 declarations, 0 contain sorry, 0 declared as axioms

Bitstring encodings

This section provides a typeclass-inferrable version of Mathlib's Computability.Encoding, specialized to the alphabet Bool.

Making it a class makes it easier to quickly ask if a function is computable in polynomial time, without having to explicitly pass around the encoding (See IsPolyTime).

We set up instances for common types like Bool, ℕ, ℤ, ℚ, and instance derivations for Prod and List types, so that we obtain instances for many common types appearing in algorithms and complexity theory.

While different references may choose different encodings, generally our encodings should be polytime-transcodable with any other reasonable binary encoding for a given type. Thus, while it may not be obvious without further examination which of several essentially equivalent encodings of a type is being used, we can at least be sure that for functions between types with BitstringEncoding instances, formalizations of questions of polynomial-time computability will capture the intended meaning.

Imports (2)

Imported by 2 files

class BitstringEncoding A canonical encoding of a type as bitstrings (List Bool) line 52 source
Source documentation
A canonical encoding of a type as bitstrings (List Bool).
This is a class version of Mathlib's Computability.Encoding, specialized to the alphabet Bool.

no axioms what this means
```
class BitstringEncoding α extends Computability.Encoding α Bool

namespace BitstringEncoding

variable {α β : Type*}

/-- The encoding function of the canonical `BitstringEncoding` of `α`. -/
```
def BitstringEncoding.bitEncode The encoding function of the canonical BitstringEncoding of α line 59 source
Source documentation
The encoding function of the canonical BitstringEncoding of α.

no axioms what this means
Statement uses: BitstringEncoding, List, Bool
Proof uses: Computability.Encoding.encode, BitstringEncoding.toEncoding
```
def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a
```
Mentions: BitstringEncoding
def BitstringEncoding.bitDecode The decoding function of the canonical BitstringEncoding of α line 62 source
Source documentation
The decoding function of the canonical BitstringEncoding of α.

no axioms what this means
Statement uses: BitstringEncoding, List, Bool, Option
Proof uses: Computability.Encoding.decode, BitstringEncoding.toEncoding
```
def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l
…
```
Mentions: BitstringEncoding
theorem BitstringEncoding.bitDecode_bitEncode Decoding is a left inverse of encoding line 66 source
Source documentation
Decoding is a left inverse of encoding.

no axioms what this means
Statement uses: BitstringEncoding, Eq, Option, BitstringEncoding.bitDecode, BitstringEncoding.bitEncode, Option.some
Proof uses: Computability.Encoding.decode_encode, Bool, BitstringEncoding.toEncoding
```
theorem bitDecode_bitEncode [BitstringEncoding α] (a : α) : bitDecode (bitEncode a) = some a :=
…
```
Mentions: BitstringEncoding, BitstringEncoding.bitDecode, BitstringEncoding.bitEncode
theorem BitstringEncoding.bitEncode_injective line 69 source
standard axioms: propext what this means
Statement uses: BitstringEncoding, Function.Injective, List, Bool, BitstringEncoding.bitEncode
Proof uses: Computability.Encoding.encode_injective, BitstringEncoding.toEncoding
def BitstringEncoding.ofLeftInverse Transport a BitstringEncoding along an injection f with partial inverse g line 75 source
Source documentation
Transport a BitstringEncoding along an injection f with partial inverse g.

standard axioms: Quot.sound, propext what this means
Statement uses: BitstringEncoding, Option, Eq, Option.some
Proof uses: BitstringEncoding.mk, Computability.Encoding.mk, Bool, BitstringEncoding.bitEncode, List, Option.bind, BitstringEncoding.bitDecode
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def ofLeftInverse [BitstringEncoding β] (f : α → β) (g : β → Option α)
    (h : ∀ x, g (f x) = some x) : BitstringEncoding α where
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 85) line 85 source
Source documentation
ℕ is encoded by its (little-endian) binary representation, as in Computability.encodeNat.
```
instance : BitstringEncoding ℕ where
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 91) line 91 source
Source documentation
Bool is encoded as a singleton bitstring.
```
instance : BitstringEncoding Bool where
…
```
Mentions: BitstringEncoding
def BitstringEncoding.delimit Make a bitstring self-delimiting: each payload bit b becomes the two bits [true, b], and the block is terminated by false line 107 source
Source documentation
Make a bitstring self-delimiting: each payload bit b becomes the two bits [true, b], and the block is terminated by false.

no axioms what this means
Statement uses: List, Bool
2 instances, coercions and auxiliary constants left out.
```
def delimit : List Bool → List Bool
  | [] => [false]
  | b :: l => true :: b :: delimit l

/-- Parse one self-delimiting block from the front of the input, returning the payload
and the remaining input. -/
```
def BitstringEncoding.undelimit Parse one self-delimiting block from the front of the input, returning the payload and the remaining input line 113 source
Source documentation
Parse one self-delimiting block from the front of the input, returning the payload and the remaining input.

standard axioms: propext what this means
Statement uses: List, Bool, Option, Prod
2 instances, coercions and auxiliary constants left out.
```
def undelimit : List Bool → Option (List Bool × List Bool)
  | false :: rest => some ([], rest)
  | true :: b :: input => (undelimit input).map fun p => (b :: p.1, p.2)
  | _ => none

@[simp]
```
theorem BitstringEncoding.undelimit_delimit line 119 source
standard axioms: propext what this means
Statement uses: List, Bool, Eq, Option, Prod, BitstringEncoding.undelimit, HAppend.hAppend, BitstringEncoding.delimit, Option.some, Prod.mk
Proof uses: List.rec, Eq.refl, List.nil, of_eq_true, List.cons, Eq.trans, True, congrFun', congrArg, Bool.true, Option.map, Prod.fst, Prod.snd, BitstringEncoding.undelimit.eq_2, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem BitstringEncoding.length_delimit line 126 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, Bool, Eq, Nat, List.length, BitstringEncoding.delimit, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: List.rec, Eq.refl, List.nil, Eq.mpr, List.cons, id, Eq.trans, congrFun', congrArg, Decidable.byContradiction, Not
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.

def BitstringEncoding.undelimitBlocksAux Parse a sequence of self-delimiting blocks, using fuel to bound the number of blocks line 135 source

Source documentation

Parse a sequence of self-delimiting blocks, using fuel to bound the number of blocks.

This is the auxiliary, fuel-carrying implementation of undelimitBlocks; since every block is nonempty, input.length is always enough fuel.

standard axioms: propext what this means

Statement uses: Nat, List, Bool, Option

2 instances, coercions and auxiliary constants left out.

def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
  | _, [] => some []
  | 0, _ :: _ => none
  | fuel + 1, input =>
    -- `p.1` is the parsed block and `p.2` the remaining input; using projections rather than a
    -- pattern-matching lambda keeps the body free of matchers.
    (undelimit input).bind fun p => (undelimitBlocksAux fuel p.2).map (p.1 :: ·)

/-- Parse a sequence of self-delimiting blocks off the front of the input.

Since every block is nonempty, `input.length` bounds the number of blocks, so it always
suffices as fuel for `undelimitBlocksAux`. -/

Mentions: BitstringEncoding.undelimit

def BitstringEncoding.undelimitBlocks Parse a sequence of self-delimiting blocks off the front of the input line 147 source
Source documentation
Parse a sequence of self-delimiting blocks off the front of the input.
Since every block is nonempty, input.length bounds the number of blocks, so it always suffices as fuel for undelimitBlocksAux.

standard axioms: propext what this means
Statement uses: List, Bool, Option
Proof uses: BitstringEncoding.undelimitBlocksAux, List.length
```
def undelimitBlocks (input : List Bool) : Option (List (List Bool)) :=
…
```
theorem BitstringEncoding.length_le_length_flatten_delimit line 150 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, Bool, LE.le, Nat, List.length, List.flatten, List.map, BitstringEncoding.delimit
Proof uses: List.rec, of_eq_true, OfNat.ofNat, List.nil, Eq.trans, True, congrArg, List.map_nil, Eq.mpr, List.cons, HAdd.hAdd, HMul.hMul, id, Eq, HAppend.hAppend, List.map_cons, List.length_append, congrFun', BitstringEncoding.length_delimit, Decidable.byContradiction and 1 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem BitstringEncoding.undelimitBlocksAux_flatten_delimit line 159 source
theorem BitstringEncoding.undelimitBlocks_flatten_delimit line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Bool, Eq, Option, BitstringEncoding.undelimitBlocks, List.flatten, List.map, BitstringEncoding.delimit, Option.some
Proof uses: List.length, BitstringEncoding.length_le_length_flatten_delimit
1 instances, coercions and auxiliary constants left out.
theorem BitstringEncoding.mapM_bitDecode_map_bitEncode line 172 source
standard axioms: Quot.sound, propext what this means
Statement uses: BitstringEncoding, List, Eq, Option, List.mapM, Bool, BitstringEncoding.bitDecode, List.map, BitstringEncoding.bitEncode, Option.some
Proof uses: List.rec, Eq.refl, List.nil, of_eq_true, List.cons, Eq.trans, True, congrFun', congrArg, Bind.bind, Pure.pure, List.map_cons, List.mapM_cons, congr, BitstringEncoding.bitDecode_bitEncode, funext, eq_self
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance BitstringEncoding.(instance at line 182) line 182 source
Source documentation
A pair is encoded as a self-delimiting block for the first component followed by the encoding of the second.
```
instance [BitstringEncoding α] [BitstringEncoding β] : BitstringEncoding (α × β) where
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 194) line 194 source
Source documentation
A list is encoded as the concatenation of self-delimiting blocks for its elements.
```
instance [BitstringEncoding α] : BitstringEncoding (List α) where
…
```
Mentions: BitstringEncoding
def BitstringEncoding.ofSubtype A subtype inherits the encoding of the ambient type; decoding additionally checks the defining predicate line 204 source
Source documentation
A subtype inherits the encoding of the ambient type; decoding additionally checks the defining predicate.

standard axioms: Quot.sound, propext what this means
Statement uses: BitstringEncoding, DecidablePred, Subtype
Proof uses: BitstringEncoding.mk, Computability.Encoding.mk, Bool, BitstringEncoding.bitEncode, List, Option.bind, BitstringEncoding.bitDecode, dite, Option, Option.some, Subtype.mk, Not, Option.none
2 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def ofSubtype {p : α → Prop} [BitstringEncoding α] [DecidablePred p] :
    BitstringEncoding (Subtype p) where
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 211) line 211 source
Source documentation
ℕ+ is encoded as the subtype {n : ℕ // 0 < n} it is defined to be.
```
instance : BitstringEncoding ℕ+ :=
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 215) line 215 source
Source documentation
ℤ is encoded via the pair (n.toNat, (-n).toNat) (one component is always 0).
```
instance : BitstringEncoding ℤ :=
…
```
Mentions: BitstringEncoding
instance BitstringEncoding.(instance at line 220) line 220 source
Source documentation
ℚ is encoded as its (reduced) numerator-denominator pair.
```
instance : BitstringEncoding ℚ :=
…
```
Mentions: BitstringEncoding