Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Pair.Internal

Exact pair weights and their transport to dominated Boolean features #

Compatible primary conjunctions use weights (5/8, 1/8, 1/8, 1/8); incompatible ones use (1/2, 1/4, 1/4, 0). Both weights increase when a true feature is turned false. Thus arbitrary additional gate predicates preserve the bound.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.weight (disjoint : Bool) (y : Bool × Bool) :
ℝ

Pair weights for compatible literals and for mutually exclusive conjunctions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.weight_nonneg (disjoint : Bool) (y : Bool × Bool) :
    0 ≤ weight disjoint y
    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.weight_mass (disjoint : Bool) :
    ∑ y : Bool × Bool, weight disjoint y = 1
    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.weight_le (disjoint a b c d : Bool) (first : a = true → c = true) (second : b = true → d = true) :
    weight disjoint (c, d) ≤ weight disjoint (a, b)
    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.disjoint_cost_le :
    3 / 2 * Real.log 2 ≤ pairEntropyCost
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.parallel (a b c d : Bool) :
    WeightBound (fun (x : Fin 2 → Bool) => (pairBit 0 1 a b x, pairBit 0 1 c d x)) pairEntropyCost

    Exact two-coordinate certificate, including equal and incompatible signed supports.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.shared (a b c d : Bool) :
      WeightBound (fun (x : Fin 3 → Bool) => (pairBit 0 1 a b x, pairBit 0 2 c d x)) pairEntropyCost

      Exact three-coordinate certificate for a pair sharing its first coordinate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal.dominatedSharedLeft {V : Type u_1} [Fintype V] [DecidableEq V] (e f : SignedEdge V) (left : e.left = f.left) (first second : (V → Bool) → Bool) (hfirst : ∀ (x : V → Bool), first x = true → e.eval x = true) (hsecond : ∀ (x : V → Bool), second x = true → f.eval x = true) :
        WeightBound (fun (x : V → Bool) => (first x, second x)) pairEntropyCost

        Lift the local pair certificates and permit arbitrary additional Boolean predicates.

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