Information savings at permutation outputs

The full-primary messages determine a permutation's input. Conjunction output messages are constant, while multiple-primary conjunction messages have quarter bias. Removing the former and applying weighted counting gives both savings.

theorem Algebraic.Aggregate.Geometry.lineSummary_eq_true_of_primaryInputs_eq_empty {n g : ℕ} (line : Line signature n g) (conjunction : Op.isConjunction line.op = true) (empty : primaryInputs line = ∅) (x : Fin n → Bool) : lineSummary line Finset.univ (Wire.elim x fun (x : Fin g) => false) = true

A conjunction with no primary slot has the constant true primary message.

theorem Algebraic.Aggregate.Geometry.key_quarter_of_multiPrimary {n g : ℕ} (p : Program signature n g) (gate : Fin g) (marked : multiPrimary (p.lines gate) = true) : 4 * {x : Fin n → Bool | key p Finset.univ x gate = true}.card ≤ Fintype.card (Fin n → Bool)

A full-primary conjunction message testing two variables has quarter bias.

theorem Algebraic.Aggregate.Geometry.key_injective_of_permutation {n : ℕ} (c : Circuit signature n n) (bijective : Function.Bijective (c.eval interpretation)) (nonprojection : ∀ (i j : Fin n), c.outputFunction interpretation i ≠ fun (x : Fin n → Bool) => x j) : Function.Injective (key c.program Finset.univ)

The gate messages of a nonprojection permutation determine its complete input.

theorem Algebraic.Aggregate.Geometry.input_le_size_sub_outputConjunctionCount_sub_bias {n : ℕ} (c : Circuit signature n n) (bijective : Function.Bijective (c.eval interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) : ↑n ≤ ↑c.size - ↑(outputConjunctionCount c) - ↑(multiCount c.program) * Cutwidth.Aggregate.Geometry.Entropy.bitSaving

Constant conjunction outputs and biased internal summaries both save message bits.