Documentation

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

Constants in the pairing and entropy bound #

The gate coefficient is (1+2c)/(1+c), where c is the saving in bits from a quarter-biased Boolean message. The survival probability accounts for giving k+1 of the n primary inputs to the receiving party.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.pairRetention (n k : ℕ) :
ℝ

Exact survival fraction for two designated primary variables.

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

    The asymptotic gate coefficient from affine pairing and biased messages.

    Equations
    Instances For
      source
      theorem Algebraic.Cutwidth.Aggregate.Geometry.one_lt_gateCoefficient :
      1 < gateCoefficient

      Pairing and entropy yield a coefficient strictly above one.

      source
      theorem Algebraic.Cutwidth.Aggregate.Geometry.gateCoefficient_lt_two :
      gateCoefficient < 2

      The present combination has coefficient strictly below two.

      source
      theorem Algebraic.Cutwidth.Aggregate.Geometry.pairRetention_nonneg {n k : ℕ} (range : k + 2 ≤ n) :
      0 ≤ pairRetention n k

      In the valid finite range the pair survival factor is nonnegative.