Affine behavior of actual signed circuit lines

Affine operations preserve affine inputs. If all internal predecessors are constant, at most one direct primary variable suffices to make any line affine. A falsified literal makes a conjunction line constant.

theorem Algebraic.Aggregate.Geometry.affineOn_xorSum {n : ℕ} {S : AffineFlat n} {r : ℕ} (fs : Fin r → (Fin n → Bool) → Bool) (h : ∀ (i : Fin r), AffineOn S (fs i)) : AffineOn S fun (x : Fin n → Bool) => xorSum fun (i : Fin r) => fs i x

Parity of any finite family of affine Boolean functions is affine.

theorem Algebraic.Aggregate.Geometry.affineOn_affineOp {n : ℕ} {S : AffineFlat n} {r : ℕ} (bias : Bool) (coefficient : Fin r → Bool) (fs : Fin r → (Fin n → Bool) → Bool) (h : ∀ (i : Fin r), AffineOn S (fs i)) : AffineOn S fun (x : Fin n → Bool) => interpretation (Op.affine r bias coefficient) fun (i : Fin (signature.Arity (Op.affine r bias coefficient))) => fs i x

An actual affine gate preserves affine input functions at every fan-in.

theorem Algebraic.Aggregate.Geometry.affineOn_of_depends_coordinate {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (i : Fin n) (depends : ∀ x ∈ S.carrier, ∀ y ∈ S.carrier, x i = y i → f x = f y) : AffineOn S f

Depending on one primary coordinate makes a Boolean function affine on the flat.

theorem Algebraic.Aggregate.Geometry.affineOn_of_depends_small {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} (U : Finset (Fin n)) (small : U.card ≤ 1) (depends : ∀ x ∈ S.carrier, ∀ y ∈ S.carrier, (∀ i ∈ U, x i = y i) → f x = f y) : AffineOn S f

Dependence on at most one coordinate suffices, including the empty support case.

def Algebraic.Aggregate.Geometry.lineFunction {n g : ℕ} (p : Program signature n g) (line : Line signature n g) : (Fin n → Bool) → Bool

The function computed by appending this actual line to the program.

Equations

• Algebraic.Aggregate.Geometry.lineFunction p line x = line.eval Algebraic.Aggregate.Geometry.interpretation x (p.eval Algebraic.Aggregate.Geometry.interpretation x)

theorem Algebraic.Aggregate.Geometry.affineOn_wire {n g : ℕ} {S : AffineFlat n} (p : Program signature n g) (affine : ∀ (i : Fin g), AffineOn S (p.gateFunction interpretation i)) (wire : Wire n g) : AffineOn S (p.wireFunction interpretation wire)

Affine gate outputs and original input coordinates cover every actual wire.

theorem Algebraic.Aggregate.Geometry.constantOn_line_of_slots {n g : ℕ} {S : AffineFlat n} (p : Program signature n g) (line : Line signature n g) (constant : ∀ (slot : Fin (signature.Arity line.op)), ConstantOn S (p.wireFunction interpretation (line.wires slot))) : ConstantOn S (lineFunction p line)

A line whose input slots are all constant has constant output.

theorem Algebraic.Aggregate.Geometry.affineOn_line_of_small_primary {n g : ℕ} {S : AffineFlat n} (p : Program signature n g) (line : Line signature n g) (small : (primaryInputs line).card ≤ 1) (constant : ∀ (slot : Fin (signature.Arity line.op)) (i : Fin g), line.wires slot = Wire.gate i → ConstantOn S (p.gateFunction interpretation i)) : AffineOn S (lineFunction p line)

Once internal predecessors are constant, one primary variable suffices for affineness.

theorem Algebraic.Aggregate.Geometry.constantOn_conjunction {n g : ℕ} {S : AffineFlat n} (p : Program signature n g) {r : ℕ} (polarity : Fin r → Bool) (negated : Bool) (wires : Fin r → Wire n g) (slot : Fin r) (value : ∀ x ∈ S.carrier, p.wireFunction interpretation (wires slot) x = !polarity slot) : ConstantOn S (lineFunction p { op := Op.conjunction r polarity negated, wires := wires })

A controlling input value forces the signed conjunction's output.