Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Joint.Parameters

Constants for joint conjunction messages #

Revealing a graph of two-variable conjunctions charges a seed edge its binary entropy, a further tree edge three quarters of a bit, and every remaining edge three halves of a bit minus the seed entropy. The resulting joint information bound improves the coefficient from the separate-coordinate entropy argument.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.quarterEntropy :
ℝ

Entropy in bits of a conjunction of two independent unbiased literals.

Equations
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.overlapPenalty :
    ℝ

    The variable charge in the joint conjunction-message bound.

    Equations
    Instances For
      source
      noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.gateSaving :
      ℝ

      The gate saving after accounting for shared primary variables.

      Equations
      Instances For
        source
        noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.gateCoefficient :
        ℝ

        The coefficient supplied by joint message counting and affine restrictions.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.quarterEntropy_eq :
          quarterEntropy = 2 - 3 / 4 * (Real.log 3 / Real.log 2)

          An exact logarithmic expression for the two-literal entropy.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.three_quarters_lt_quarterEntropy :
          3 / 4 < quarterEntropy

          The seed entropy exceeds three quarters of a bit, since 27 < 32.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.quarterEntropy_lt_one :
          quarterEntropy < 1

          A conjunction carries strictly less than one bit.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.overlapPenalty_pos :
          0 < overlapPenalty

          The graph variable charge is positive.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.overlapPenalty_lt_quarter :
          overlapPenalty < 1 / 4

          The graph variable charge is less than one quarter.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.gateSaving_pos :
          0 < gateSaving

          The joint gate saving is positive.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.gateCoefficient_eq :
          gateCoefficient = (1 - overlapPenalty + 2 * gateSaving) / (1 + gateSaving)

          The coefficient in the form arising from the two finite inequalities.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.old_gateCoefficient_lt :
          Geometry.gateCoefficient < gateCoefficient

          Joint counting strictly improves the previous separate-coordinate coefficient.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.one_lt_gateCoefficient :
          1 < gateCoefficient

          The joint coefficient is strictly above one.