Documentation

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

Exact conditional tables on at most four Boolean variables #

Every local graph configuration is one of a seed, an extension, a parallel edge, a triangle, or a path on four vertices. Finite enumeration checks the signed Boolean tables; exact logarithmic inequalities certify their coding costs.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairSeed (a b : Bool) :
WeightBound (pairBit 0 1 a b) (Real.binEntropy (1 / 4))

A signed two-variable conjunction costs exactly the quarter binary entropy.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairExtension (a b c d : Bool) :
    ConditionalWeightBound (pairBit 0 1 a b) (pairBit 0 2 c d) (3 / 4 * Real.log 2)

    One previously used endpoint gives a three-quarter-bit conditional cost.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairParallel (a b c d : Bool) :
      ConditionalWeightBound (pairBit 0 1 a b) (pairBit 0 1 c d) (3 / 2 * Real.log 2 - Real.binEntropy (1 / 4))

      A repeated support obeys the remaining-edge charge.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairTriangle (a b c d e f : Bool) :
        ConditionalWeightBound (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))

        A triangle obeys the remaining-edge charge for every choice of literal signs.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairDisjoint (a b c d e f : Bool) :
          ConditionalWeightBound (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))

          Two neighbors on four vertices obey the remaining-edge charge.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For