Constants for the Gold-map gate bound

With c = 1 - H₂(1/4), the restriction–rank and entropy inequalities give the leading coefficient (7 + 4c)/(4 + 2c), approximately 1.771556, and the additive penalty (3 + 4c)/(4 + 2c), approximately 0.857781. The coefficient lies strictly between 7/4 and 2.

noncomputable def Algebraic.Aggregate.Geometry.Gold.gateCoefficient : ℝ

Leading gate coefficient for the Gold map in odd dimension.

Equations

• Algebraic.Aggregate.Geometry.Gold.gateCoefficient = (7 + 4 * Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving) / (4 + 2 * Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving)

noncomputable def Algebraic.Aggregate.Geometry.Gold.constantPenalty : ℝ

The finite additive loss in the Gold-map gate bound.

Equations

• Algebraic.Aggregate.Geometry.Gold.constantPenalty = (3 + 4 * Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving) / (4 + 2 * Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving)

theorem Algebraic.Aggregate.Geometry.Gold.seven_quarters_lt_gateCoefficient : 7 / 4 < gateCoefficient

The Gold coefficient exceeds seven quarters.

theorem Algebraic.Aggregate.Geometry.Gold.gateCoefficient_lt_two : gateCoefficient < 2

The Gold coefficient is below two.

theorem Algebraic.Aggregate.Geometry.Gold.constantPenalty_pos : 0 < constantPenalty

The finite penalty is positive.