Majority fibers of permutation circuit messages

Disjoint exact-two conjunctions simultaneously have their majority summaries on a large set of inputs. These false coordinates and the constant true conjunction output summaries can both be omitted from the injective full-primary message.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.input_add_majority_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 * ↑S.card ≤ ↑c.size - ↑(Aggregate.Geometry.outputConjunctionCount c)

Disjoint majority summaries and constant output summaries save separate message bits.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.input_add_remaining_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) (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))) : ↑n + messageLoss * ↑P.remaining.card ≤ ↑c.size - ↑(Aggregate.Geometry.outputConjunctionCount c)

Unpaired exact-two gates give the majority-fiber inequality for a primary pairing.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.three_mul_input_add_majority_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 * (↑(Aggregate.Geometry.Shared.exactTwo c.program).card - 2 * ↑P.pairs.card) ≤ 2 * ↑c.size

Independent nonaffine outputs combine with unpaired majority summaries.