Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Local.Numbers

Exact logarithmic comparisons for conjunction tables #

The local entropy comparisons reduce to small integer inequalities, avoiding floating-point estimates in the circuit coefficient.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.binEntropy_quarter_eq :
Real.binEntropy (1 / 4) = 2 * Real.log 2 - 3 / 4 * Real.log 3

The natural-log entropy of a conjunction of two unbiased literals.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.three_quarters_log_lt_binEntropy_quarter :
3 / 4 * Real.log 2 < Real.binEntropy (1 / 4)

Three quarters of a bit is strictly below the two-literal seed cost.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.parallel_le_extension :
3 / 2 * Real.log 2 - Real.binEntropy (1 / 4) ≤ 3 / 4 * Real.log 2

A parallel edge's cost is at most the spanning-tree extension charge.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.half_le_chord :
1 / 2 * Real.log 2 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The remaining-edge charge is at least half a bit.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.extension_log_bound :
3 * Real.log 2 - 5 / 8 * Real.log 5 - Real.binEntropy (1 / 4) ≤ 3 / 4 * Real.log 2

The worst shared-variable extension costs at most three quarters of a bit.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.triangle_log_bound :
5 / 4 * Real.log 2 - 3 / 8 * Real.log 3 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The triangle's largest conditional entropy fits the remaining-edge charge.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.triangle_first_log_bound :
5 / 8 * Real.log 5 - Real.log 2 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The triangle table with five assignments in one parent fibre.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.triangle_second_log_bound :
5 / 8 * Real.log 5 - 1 / 4 * Real.log 2 - 3 / 8 * Real.log 3 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The triangle table splitting its five-point parent fibre into two and three.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.disjoint_first_log_bound :
3 / 2 * Real.log 3 - 7 / 4 * Real.log 2 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The four-variable table with both shared literals agreeing.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.disjoint_second_log_bound :
21 / 16 * Real.log 3 - 1 / 4 * Real.log 2 - 7 / 16 * Real.log 7 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The four-variable table with exactly one shared literal agreeing.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.disjoint_third_log_bound :
9 / 8 * Real.log 3 - 1 / 2 * Real.log 2 - 5 / 16 * Real.log 5 ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

The four-variable table with neither shared literal agreeing.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.binEntropy_eighth_le_chord :
Real.binEntropy (1 / 8) ≤ 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

Three forced literals save enough to be charged as a remaining graph edge.