Conditional entropy for all outputs of a permutation

The full primary message is injective. Its majority event retains biased narrow and wide conjunction summaries while designated conjunction-output summaries are constant. Independent nonaffine output components supply the extra output charge.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.input_add_conditional_le_size_sub_outputConjunctionCount {n : ℕ} (c : Circuit Aggregate.Geometry.signature n n) (bijective : Function.Bijective (c.eval Aggregate.Geometry.interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction Aggregate.Geometry.interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (S : Finset (Fin c.size)) (eligible : S ⊆ Aggregate.Geometry.Shared.exactTwo c.program) (disjoint : (↑S).Pairwise fun (i j : Fin c.size) => Disjoint (Aggregate.Geometry.primaryInputs (c.program.lines i)) (Aggregate.Geometry.primaryInputs (c.program.lines j))) : ↑n + (messageLoss - pairSaving) * ↑S.card + pairSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + tripleSaving * ↑(Joint.retainedWide c.program Finset.univ).card ≤ ↑c.size - ↑(Aggregate.Geometry.outputConjunctionCount c)

On a permutation, the majority-conditioned primary message remains injective.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.three_mul_input_add_conditional_le_two_mul_size {n : ℕ} (c : Circuit Aggregate.Geometry.signature n n) (bijective : Function.Bijective (c.eval Aggregate.Geometry.interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction Aggregate.Geometry.interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (independent : Aggregate.Geometry.NonaffineComponents (c.eval Aggregate.Geometry.interpretation)) (P : Aggregate.Geometry.Shared.PrimaryPairing c.program) (disjoint : (↑P.remaining).Pairwise fun (i j : Fin c.size) => Disjoint (Aggregate.Geometry.primaryInputs (c.program.lines i)) (Aggregate.Geometry.primaryInputs (c.program.lines j))) : 3 * ↑n + (messageLoss - pairSaving) * (↑(Aggregate.Geometry.Shared.exactTwo c.program).card - 2 * ↑P.pairs.card) + pairSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + tripleSaving * ↑(Joint.retainedWide c.program Finset.univ).card ≤ 2 * ↑c.size

Output rank combines with all conditional narrow and wide savings.