Canonical encoding of finite Boolean assignments and tables

This module exposes computable exact-length codecs for Boolean functions on finite ordered domains, assignments on ordered finite coordinate sets, and their full Boolean truth tables.

theorem Complexity.BooleanDependency.OrderedAssignment.card {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Fintype.card (OrderedAssignment coordinates) = 2 ^ coordinates.card

There are exactly 2^|S| canonically ordered assignments to S.

@[simp]

theorem Complexity.BooleanDependency.length_encodeOrderedFunction {index : Type u_1} [Fintype index] [LinearOrder index] (function : index → Bool) : (encodeOrderedFunction function).length = Fintype.card index

Ordered finite-function encodings contain exactly one bit per input.

@[simp]

theorem Complexity.BooleanDependency.decodeOrderedFunction?_encodeOrderedFunction {index : Type u_1} [Fintype index] [LinearOrder index] (function : index → Bool) : decodeOrderedFunction? (encodeOrderedFunction function) = some function

Exact round trip for Boolean functions on finite ordered domains.

theorem Complexity.BooleanDependency.encodeOrderedFunction_injective {index : Type u_1} [Fintype index] [LinearOrder index] : Function.Injective encodeOrderedFunction

Canonical ordered finite-function encoding is injective.

@[simp]

theorem Complexity.BooleanDependency.decodeOrderedFunction?_eq_none_iff {index : Type u_1} [Fintype index] [LinearOrder index] (bits : List Bool) : decodeOrderedFunction? bits = none ↔ bits.length ≠ Fintype.card index

Ordered finite-function decoding fails exactly on malformed lengths.

@[simp]

theorem Complexity.BooleanDependency.length_encodeAssignment {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (assignment : ↥coordinates → Bool) : (encodeAssignment coordinates assignment).length = coordinates.card

Assignment encodings contain exactly one bit per selected coordinate.

@[simp]

theorem Complexity.BooleanDependency.decodeAssignment?_encodeAssignment {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (assignment : ↥coordinates → Bool) : decodeAssignment? coordinates (encodeAssignment coordinates assignment) = some assignment

Exact assignment-codec round trip.

theorem Complexity.BooleanDependency.encodeAssignment_injective {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Function.Injective (encodeAssignment coordinates)

Canonical assignment encoding is injective.

@[simp]

theorem Complexity.BooleanDependency.decodeAssignment?_eq_none_iff {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : decodeAssignment? coordinates bits = none ↔ bits.length ≠ coordinates.card

Assignment decoding fails exactly on strings of the wrong length.

@[simp]

theorem Complexity.BooleanDependency.length_encodeTable {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (table : (↥coordinates → Bool) → Bool) : (encodeTable coordinates table).length = 2 ^ coordinates.card

A full Boolean table has exactly 2^|S| serialized entries.

@[simp]

theorem Complexity.BooleanDependency.decodeTable?_encodeTable {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (table : (↥coordinates → Bool) → Bool) : decodeTable? coordinates (encodeTable coordinates table) = some table

Exact dependency-table-codec round trip.

theorem Complexity.BooleanDependency.encodeTable_injective {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) : Function.Injective (encodeTable coordinates)

Canonical dependency-table encoding is injective.

@[simp]

theorem Complexity.BooleanDependency.decodeTable?_eq_none_iff {coordinate : Type u_1} [LinearOrder coordinate] (coordinates : Finset coordinate) (bits : List Bool) : decodeTable? coordinates bits = none ↔ bits.length ≠ 2 ^ coordinates.card

Table decoding fails exactly on strings without one bit per assignment.