Exact constants for majority-fiber and entropy combinations

The separate-coordinate and joint-message inequalities are combined so that their two-variable saving is half the wide-conjunction saving. The additional majority-fiber inequality has weight wideSaving / (2 * log₂(3/2)).

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.messageLoss : ℝ

Logarithmic charge in the majority-fiber message inequality.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.messageLoss = Real.logb 2 (3 / 2)

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight : ℝ

Weight of the majority-fiber inequality.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight = Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving / (2 * Algebraic.Cutwidth.Aggregate.Geometry.Fiber.messageLoss)

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.separateWeight : ℝ

Weight of the separate-coordinate entropy inequality.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.jointWeight : ℝ

Weight of the joint-message entropy inequality.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarNumerator : ℝ

Numerator of the scalar gate coefficient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarDenominator : ℝ

Denominator of the scalar gate coefficient.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarDenominator = 1 + Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving + Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.gateCoefficient : ℝ

Exact scalar coefficient supplied by the fiber and entropy combination.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.gateCoefficient = Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarNumerator / Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarDenominator

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionNumerator : ℝ

Numerator when independent nonlinear output components are also counted.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionDenominator : ℝ

Denominator when independent nonlinear output components are also counted.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionDenominator = 2 + Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving + 2 * Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionCoefficient : ℝ

Exact coefficient combining component rank, majority fibers, and entropy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionPenalty : ℝ

Finite loss from the two-dimensional affine restriction.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionPenalty = 4 * Algebraic.Cutwidth.Aggregate.Geometry.Shared.wideSaving / Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionDenominator

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.messageLoss_eq_logb_three_sub_one : messageLoss = Real.logb 2 3 - 1

The same logarithmic charge in the form supplied by majority-input counting.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.messageLoss_pos : 0 < messageLoss

The majority-fiber logarithmic charge is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight_pos : 0 < fiberWeight

The majority-fiber inequality has positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.fiberWeight_mul_messageLoss : fiberWeight * messageLoss = Shared.wideSaving / 2

The weighted majority-fiber charge is half the wide-conjunction saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.bitSaving_lt_half_wideSaving : Entropy.bitSaving < Shared.wideSaving / 2

The one-eighth saving exceeds twice the separate two-variable saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.half_wideSaving_lt_gateSaving : Shared.wideSaving / 2 < Joint.gateSaving

Half the one-eighth saving is less than the joint two-variable saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.savingGap_pos : 0 < Joint.gateSaving - Entropy.bitSaving

The denominator of the entropy interpolation is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.separateWeight_pos : 0 < separateWeight

The separate-coordinate entropy inequality has positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.jointWeight_pos : 0 < jointWeight

The joint-message entropy inequality has positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.separateWeight_add_jointWeight : separateWeight + jointWeight = 1

The entropy interpolation is a convex combination.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.weighted_saving : separateWeight * Entropy.bitSaving + jointWeight * Joint.gateSaving = Shared.wideSaving / 2

The interpolated two-variable saving is half the wide-conjunction saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.savingGap_eq_two_mul_overlapPenalty : Joint.gateSaving - Entropy.bitSaving = 2 * Joint.overlapPenalty

The joint saving gap is exactly twice the overlap penalty.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.jointWeight_mul_overlapPenalty : jointWeight * Joint.overlapPenalty = (Shared.wideSaving / 2 - Entropy.bitSaving) / 2

The overlap charge after entropy interpolation.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.scalarDenominator_pos : 0 < scalarDenominator

The scalar denominator is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionDenominator_pos : 0 < inversionDenominator

The component-rank denominator is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.one_lt_gateCoefficient : 1 < gateCoefficient

The scalar coefficient exceeds one.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.three_halves_lt_inversionCoefficient : 3 / 2 < inversionCoefficient

The coefficient with independent output components exceeds three halves.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.inversionPenalty_pos : 0 < inversionPenalty

The finite component-rank penalty is positive.