Finite Boolean dependency tables

A function depending on a finite coordinate set can be represented by its canonical table on assignments to that set. This module exposes exact reconstruction, the 2^|S| table-entry count, finiteness of the function's range, and the corresponding range-cardinality bound. It also splits total assignments bijectively across a coordinate set and its complement and proves that uniform restriction is exactly uniform. Ordered finite coordinate sets also receive computable exact-length assignment and truth-table codecs.

@[simp]

theorem Complexity.BooleanDependency.mergeAssignments_split {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (input : coordinate → Bool) : mergeAssignments coordinates (restrict coordinates input, restrict coordinatesᶜ input) = input

Splitting and then merging a total assignment recovers it exactly.

@[simp]

theorem Complexity.BooleanDependency.restrict_mergeAssignments_left {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (selected : ↥coordinates → Bool) (outside : ↥coordinatesᶜ → Bool) : restrict coordinates (mergeAssignments coordinates (selected, outside)) = selected

Restricting a merged assignment to its selected coordinates recovers the selected component.

@[simp]

theorem Complexity.BooleanDependency.restrict_mergeAssignments_right {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (selected : ↥coordinates → Bool) (outside : ↥coordinatesᶜ → Bool) : restrict coordinatesᶜ (mergeAssignments coordinates (selected, outside)) = outside

Restricting a merged assignment to the complement recovers the complement component.

theorem Complexity.BooleanDependency.uniformProbability_restrict {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (event : (↥coordinates → Bool) → Prop) [DecidablePred event] : uniformProbability {input : coordinate → Bool | event (restrict coordinates input)} = uniformProbability (Finset.filter event Finset.univ)

Restricting a uniformly random total Boolean assignment to any finite coordinate subset produces the exact uniform distribution on subset assignments.

@[simp]

theorem Complexity.BooleanDependency.extendByFalse_restrict_apply {coordinate : Type u_1} [DecidableEq coordinate] (coordinates : Finset coordinate) (input : coordinate → Bool) (index : coordinate) (hindex : index ∈ coordinates) : extendByFalse coordinates (restrict coordinates input) index = input index

Extending a restricted assignment recovers every selected coordinate.

@[simp]

theorem Complexity.BooleanDependency.table_restrict {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) (input : coordinate → Bool) : table coordinates function (restrict coordinates input) = function input

If a function depends only on the selected coordinates, its canonical table reconstructs its value on every total input.

theorem Complexity.BooleanDependency.card_assignments {coordinate : Type u_1} (coordinates : Finset coordinate) : Nat.card (↥coordinates → Bool) = 2 ^ coordinates.card

A table on |S| Boolean coordinates has exactly 2^|S| entries.

theorem Complexity.BooleanDependency.finite_range_of_dependsOn {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) : (Set.range function).Finite

A function depending on finitely many Boolean coordinates has finite range.

theorem Complexity.BooleanDependency.card_range_le_pow_card_of_dependsOn {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) : Nat.card ↑(Set.range function) ≤ 2 ^ coordinates.card

A function depending on S has at most 2^|S| distinct values.