Finite truth-table proofs for conditional conjunction costs

All cases are checked by kernel reduction and exact logarithmic inequalities.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.LocalCases.seed_cost (a b : Bool) : (tableCost (pairBit 0 1 a b) fun (x : Fin 2 → Bool) => ()) = Real.binEntropy (1 / 4)

The seed table has exactly the quarter binary entropy.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.LocalCases.extension_cost (a b c d : Bool) : tableCost (pairBit 0 1 a b) (pairBit 0 2 c d) ≤ 3 / 4 * Real.log 2

The shared-endpoint table costs at most three quarters of a bit.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.LocalCases.parallel_cost (a b c d : Bool) : tableCost (pairBit 0 1 a b) (pairBit 0 1 c d) ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The parallel-support table obeys the remaining-edge charge.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.LocalCases.triangle_cost (a b c d e f : Bool) : (tableCost (pairBit 0 1 a b) fun (x : Fin 3 → Bool) => (pairBit 0 2 c d x, pairBit 1 2 e f x)) ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

All signed triangle tables obey the remaining-edge charge.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.LocalCases.disjoint_cost (a b c d e f : Bool) : (tableCost (pairBit 0 1 a b) fun (x : Fin 4 → Bool) => (pairBit 0 2 c d x, pairBit 1 3 e f x)) ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

All signed four-vertex tables obey the remaining-edge charge.