Exact constants for entropy conditioned on majority fibers

On a product of three-point pair fibers, two and three distinct prescribed coordinates have probabilities at most 4/9 and 8/27. Their binary entropy savings determine positive interpolation weights for the scalar and inversion bounds. All comparisons below use exact logarithms and integer inequalities.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving : ℝ

Saving of a two-coordinate conjunction under the majority-product law.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving = 1 - Real.binEntropy (4 / 9) / Real.log 2

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving : ℝ

Saving of a three-coordinate conjunction under the majority-product law.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving = 1 - Real.binEntropy (8 / 27) / Real.log 2

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberDenominator : ℝ

Denominator in the weight of the conditional-majority inequality.

Equations

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

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

Weight of the conditional-majority inequality.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.wideWeight : ℝ

Weight of the shared-control affine inequality.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.effectiveSaving : ℝ

Narrow-gate saving supplied by the marginal/joint entropy interpolation.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.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.Conditional.jointWeight : ℝ

Weight of the joint-message entropy inequality.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.jointWeight = 1 - Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.separateWeight

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

Numerator of the conditional-majority scalar coefficient.

Equations

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

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

Denominator of the conditional-majority scalar coefficient.

Equations

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

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

Exact scalar coefficient of the conditional-majority combination.

Equations

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

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

Numerator when independent nonaffine output components are counted.

Equations

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

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

Denominator when independent nonaffine output components are counted.

Equations

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

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

Exact inversion coefficient of the conditional-majority combination.

Equations

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

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

Loss when simultaneous affine inversion outputs live on at most four points.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving_eq : pairSaving = 17 / 9 - 2 * (Real.log 3 / Real.log 2) + 5 / 9 * (Real.log 5 / Real.log 2)

Exact logarithmic form of the conditional two-coordinate saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving_eq : tripleSaving = 17 / 9 - 3 * (Real.log 3 / Real.log 2) + 19 / 27 * (Real.log 19 / Real.log 2)

Exact logarithmic form of the conditional three-coordinate saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving_pos : 0 < pairSaving

The conditional pair is not unbiased, so its saving is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving_pos : 0 < tripleSaving

The conditional triple is not unbiased, so its saving is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving_nonneg : 0 ≤ pairSaving

The conditional pair saving is nonnegative.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving_nonneg : 0 ≤ tripleSaving

The conditional triple saving is nonnegative.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving_lt : pairSaving < 1 / 64

A rational upper bound proved by an exact integer-power comparison.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.tripleSaving_lt : tripleSaving < 1 / 8

A rational upper bound proved by an exact integer-power comparison.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.messageLoss_bounds : 7 / 12 < messageLoss ∧ messageLoss < 3 / 5

Exact rational bounds on the majority message loss.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.pairSaving_lt_messageLoss : pairSaving < messageLoss

The conditional pair charge leaves a positive majority-fiber saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.wideSaving_bounds : 9 / 20 < Shared.wideSaving ∧ Shared.wideSaving < 1 / 2

Exact rational bounds on the unconditional wide-conjunction saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberDenominator_bounds : 1 < fiberDenominator ∧ fiberDenominator < 6 / 5

The conditional-fiber denominator lies in a positive rational interval.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberDenominator_pos : 0 < fiberDenominator

The conditional-fiber denominator is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberWeight_bounds : 3 / 8 < fiberWeight ∧ fiberWeight < 1 / 2

The conditional-fiber weight lies in a useful exact rational interval.

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

The conditional-fiber inequality has positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.effectiveSaving_bounds : 1 / 5 < effectiveSaving ∧ effectiveSaving < 3 / 10

The effective saving is between one fifth and three tenths.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.effectiveSaving_between : Entropy.bitSaving < effectiveSaving ∧ effectiveSaving < Joint.gateSaving

The effective saving lies strictly between the two available entropy charges.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.wideWeight_pos : 0 < wideWeight

The shared-control affine inequality has positive weight.

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

The separate-coordinate entropy inequality has positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.jointWeight_eq : jointWeight = (effectiveSaving - Entropy.bitSaving) / (Joint.gateSaving - Entropy.bitSaving)

The joint entropy weight in a symmetric quotient form.

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

The joint-message entropy inequality has positive weight.

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

The unconditional entropy inequalities are combined convexly.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.weighted_saving : separateWeight * Entropy.bitSaving + jointWeight * Joint.gateSaving = effectiveSaving

The unconditional narrow-gate charge is exactly the effective saving.

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

The interpolated overlap charge in terms of the effective saving.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberWeight_mul_denominator : fiberWeight * fiberDenominator = Shared.wideSaving

The defining conditional-fiber denominator cancels against its weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.wideWeight_eq : wideWeight = Shared.wideSaving + fiberWeight * tripleSaving

Conditional wide-gate information supplements the original wide-gate charge.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.effectiveSaving_add_pairSaving : effectiveSaving + fiberWeight * pairSaving = wideWeight / 2

Unconditional and conditional narrow-gate charges match the affine weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.effectiveSaving_add_messageLoss : effectiveSaving + fiberWeight * messageLoss = wideWeight

The combined narrow-gate charge is the shared-control affine weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.fiberWeight_mul_pairLoss : fiberWeight * (2 * (messageLoss - pairSaving)) = wideWeight

The matching loss in the conditional majority inequality cancels the affine gain.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.scalarDenominator_eq : scalarDenominator = 1 + fiberWeight + wideWeight

The scalar denominator is the sum of the three positive inequality weights.

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

The scalar denominator is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.scalarNumerator_eq : scalarNumerator = 1 - jointWeight * Joint.overlapPenalty + fiberWeight + 2 * wideWeight

The scalar numerator in the form obtained by adding the finite inequalities.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.inversionDenominator_eq : inversionDenominator = 2 + 2 * fiberWeight + wideWeight

The inversion denominator is the sum of the rank-adjusted inequality weights.

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

The inversion denominator is positive.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.inversionNumerator_eq : inversionNumerator = 3 - jointWeight * Joint.overlapPenalty + 3 * fiberWeight + 2 * wideWeight

The inversion numerator in the form obtained by adding the finite inequalities.

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

The conditional-majority scalar coefficient exceeds one.

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

The conditional-majority inversion coefficient exceeds three halves.

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

The finite inversion penalty is positive.