Documentation

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

Constants for shared-control restrictions and wide conjunction messages #

The affine saving at intersecting exact-two gates combines with the stronger one-eighth bias of wide conjunctions. Its coefficient strictly exceeds the previous joint-graph coefficient.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideEntropy :
ℝ

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

Equations
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving :
    ℝ

    Information saved by a conjunction involving at least three primary variables.

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

      The whole-basis coefficient obtained from shared primary controls.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Shared.receiverRetention (n k : ℕ) :
        ℝ

        Fraction of designated triples retained after a logarithmic receiving side.

        Equations
        Instances For
          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.receiverRetention_nonneg {n k : ℕ} (range : k + 4 ≤ n) :
          0 ≤ receiverRetention n k

          A sending side with at least three coordinates has nonnegative triple retention.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideEntropy_eq :
          wideEntropy = 3 - 7 / 8 * (Real.log 7 / Real.log 2)

          The one-eighth entropy has an exact expression using the logarithm of seven.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving_pos :
          0 < wideSaving

          A wide conjunction saves a positive number of bits.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.gateSaving_lt_wideSaving :
          Joint.gateSaving < wideSaving

          The one-eighth bias saves strictly more than the joint two-variable gate charge.

          source
          theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving_lt_two_mul_gateSaving :
          wideSaving < 2 * Joint.gateSaving

          Twice the two-variable gate saving dominates the one-eighth saving.

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

          Shared-control preprocessing strictly improves the preceding joint coefficient.

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

          The resulting gate coefficient is strictly above one.