Documentation

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

Constants for the inversion rank and entropy bound #

Combining independent nonlinear output components, constant output summaries, and affine pairing yields coefficient (3+2c)/(2+c), where c=1-H₂(1/4). This is approximately 1.54311234736, strictly above three halves.

source
noncomputable def Algebraic.Aggregate.Geometry.Inversion.gateCoefficient :
ℝ

Leading gate coefficient from independent components and biased messages.

Equations
Instances For
    source
    noncomputable def Algebraic.Aggregate.Geometry.Inversion.constantPenalty :
    ℝ

    The finite additive loss contributed by a two-dimensional affine restriction.

    Equations
    Instances For
      source
      theorem Algebraic.Aggregate.Geometry.Inversion.three_halves_lt_gateCoefficient :
      3 / 2 < gateCoefficient

      Independent nonlinear outputs strictly improve the three-halves coefficient.

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

      The present rank and entropy combination gives a coefficient below two.

      source
      theorem Algebraic.Aggregate.Geometry.Inversion.constantPenalty_pos :
      0 < constantPenalty

      The exact finite penalty is positive.