Balanced conjunction outputs have no primary slots

A balanced Boolean function forced into one primary half-cube must be a literal. Consequently a nonliteral balanced conjunction output reads only internal wires, and its full-primary one-way message is constant.

noncomputable def Algebraic.Aggregate.Geometry.outputGateSet {n m : ℕ} (c : Circuit signature n m) : Finset (Fin c.size)

Actual gate wires selected among the circuit's outputs.

Equations

• Algebraic.Aggregate.Geometry.outputGateSet c = {gate : Fin c.size | ∃ (i : Fin m), c.outputs i = Cslib.Circuits.Wire.gate gate}

noncomputable def Algebraic.Aggregate.Geometry.outputConjunctions {n m : ℕ} (c : Circuit signature n m) : Finset (Fin c.size)

Conjunction gates whose wires are designated circuit outputs.

Equations

• Algebraic.Aggregate.Geometry.outputConjunctions c = {gate ∈ Algebraic.Aggregate.Geometry.outputGateSet c | Algebraic.Aggregate.Geometry.Op.isConjunction (c.program.lines gate).op = true}

noncomputable def Algebraic.Aggregate.Geometry.outputConjunctionCount {n m : ℕ} (c : Circuit signature n m) : ℕ

The number of distinct conjunction output gates.

Equations

• Algebraic.Aggregate.Geometry.outputConjunctionCount c = (Algebraic.Aggregate.Geometry.outputConjunctions c).card

theorem Algebraic.Aggregate.Geometry.exists_injective_outputGates {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) : ∃ (gate : Fin n → Fin c.size), Function.Injective gate ∧ ∀ (i : Fin n), c.outputs i = Wire.gate (gate i)

Nonprojection output wires of a permutation are distinct actual gates.

theorem Algebraic.Aggregate.Geometry.card_outputGateSet {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) : (outputGateSet c).card = n

A nonprojection permutation has exactly one distinct designated gate per output.

theorem Algebraic.Aggregate.Geometry.input_add_conjunctionCount_le_size_add_outputConjunctionCount {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) : n + conjunctionCount c.program ≤ c.size + outputConjunctionCount c

Distinct output gates and conjunction gates overlap exactly at conjunction outputs.

theorem Algebraic.Aggregate.Geometry.eq_literal_of_balanced_forced {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) (a b : Bool) (balanced : 2 * Fintype.card { x : Fin n → Bool // f x = b } = 2 ^ n) (forced : ∀ (x : Fin n → Bool), f x = b → x i = a) : f = fun (x : Fin n → Bool) => a ^^ b ^^ x i

A balanced bit forced into a primary half-cube is a primary literal.

theorem Algebraic.Aggregate.Geometry.conjunction_line_forces_primary {n g : ℕ} (p : Program signature n g) (line : Line signature n g) (conjunction : Op.isConjunction line.op = true) (i : Fin n) (primary : i ∈ primaryInputs line) : ∃ (a : Bool) (b : Bool), ∀ (x : Fin n → Bool), lineFunction p line x = b → x i = a

A primary literal is forced by the nondefault value of a conjunction line.

theorem Algebraic.Aggregate.Geometry.primaryInputs_eq_empty_of_output_conjunction {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) (gate : Fin c.size) (output : gate ∈ outputConjunctions c) : primaryInputs (c.program.lines gate) = ∅

Balanced nonliteral conjunction output gates cannot read a primary input directly.