Disjoint pairs of conjunction gates sharing primary inputs

Pairs refer to actual program indices. Both endpoints have exactly two distinct primary inputs, and different pairs have disjoint gate endpoints.

def Algebraic.Aggregate.Geometry.Shared.exactTwo {n g : ℕ} (p : Program signature n g) : Finset (Fin g)

Actual conjunction gates with exactly two distinct direct primary inputs.

Equations

• One or more equations did not get rendered due to their size.

structure Algebraic.Aggregate.Geometry.Shared.PrimaryPairing {n g : ℕ} (p : Program signature n g) : Type

Gate-disjoint ordered pairs sharing a primary input.

• pairs : Finset (Fin g × Fin g)

  The selected pairs of actual gate indices.

• eligible (e : Fin g × Fin g) : e ∈ self.pairs → e.1 ∈ exactTwo p ∧ e.2 ∈ exactTwo p

  Each endpoint is an actual exact-two conjunction gate.

• distinct (e : Fin g × Fin g) : e ∈ self.pairs → e.1 ≠ e.2

  A pair contains two different gates.

• overlap (e : Fin g × Fin g) : e ∈ self.pairs → ∃ j ∈ primaryInputs (p.lines e.1), j ∈ primaryInputs (p.lines e.2)

  The two gates have a common primary variable.

• disjoint : (↑self.pairs).Pairwise fun (e f : Fin g × Fin g) => Disjoint {e.1, e.2} {f.1, f.2}

  No gate occurs in two selected pairs.

def Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.used {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) : Finset (Fin g)

Gate indices belonging to a selected pair.

Equations

• P.used = P.pairs.biUnion fun (e : Fin g × Fin g) => {e.1, e.2}

def Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.remaining {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) : Finset (Fin g)

Exact-two conjunction gates not selected in any pair.

Equations

• P.remaining = Algebraic.Aggregate.Geometry.Shared.exactTwo p \ P.used