Quarter bias of conjunction messages

A conjunction summary that tests two distinct selected primary inputs is true on at most one quarter of the selected assignments. The proof overwrites the two forced coordinates to inject four copies of the accepting assignments into all assignments; repetitions and contradictory literals need no separate assumptions.

theorem Algebraic.Aggregate.Geometry.four_mul_card_le_of_forces_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : (ι → Bool) → Prop) [DecidablePred P] (i j : ι) (hne : i ≠ j) (a b : Bool) (hP : ∀ (x : ι → Bool), P x → x i = a ∧ x j = b) : 4 * Fintype.card { x : ι → Bool // P x } ≤ 2 ^ Fintype.card ι

Fixing two distinct Boolean coordinates leaves at most a quarter of all assignments.

theorem Algebraic.Aggregate.Geometry.conjunctionSummary_forces_pair {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (s t : Fin r) (i j : ↥U) (hs : wires s = Wire.input ↑i) (ht : wires t = Wire.input ↑j) (x : ↥U → Bool) (hx : conjunctionSummary polarity wires U (Wire.elim (Cutwidth.glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false) = true) : x i = polarity s ∧ x j = polarity t

Two selected literal slots force the corresponding assignment coordinates.

theorem Algebraic.Aggregate.Geometry.conjunctionSummary_quarter {r n g : ℕ} (polarity : Fin r → Bool) (wires : Fin r → Wire n g) (U : Finset (Fin n)) (s t : Fin r) (i j : ↥U) (hne : i ≠ j) (hs : wires s = Wire.input ↑i) (ht : wires t = Wire.input ↑j) : 4 * {x : ↥U → Bool | conjunctionSummary polarity wires U (Wire.elim (Cutwidth.glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false) = true}.card ≤ 2 ^ U.card

A selected conjunction with two distinct primary variables has quarter bias.

def Algebraic.Aggregate.Geometry.SelectedPair {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) : Prop

A conjunction line has two distinct primary variables selected by the cut.

Equations

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

@[instance_reducible]

instance Algebraic.Aggregate.Geometry.instDecidableSelectedPair {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) : Decidable (SelectedPair line U)

Equations

• Algebraic.Aggregate.Geometry.instDecidableSelectedPair line U = id inferInstance

theorem Algebraic.Aggregate.Geometry.multiPrimary_iff_exists_pair {n g : ℕ} (line : Line signature n g) : multiPrimary line = true ↔ Op.isConjunction line.op = true ∧ ∃ i ∈ primaryInputs line, ∃ j ∈ primaryInputs line, i ≠ j

Multiple-primary conjunctions supply two distinct designated primary variables.

theorem Algebraic.Aggregate.Geometry.SelectedPair.multiPrimary {n g : ℕ} {line : Line signature n g} {U : Finset (Fin n)} (h : SelectedPair line U) : Geometry.multiPrimary line = true

A selected pair belongs to an actual multiple-primary conjunction.

theorem Algebraic.Aggregate.Geometry.selectedPair_univ_iff {n g : ℕ} (line : Line signature n g) : SelectedPair line Finset.univ ↔ multiPrimary line = true

Selecting every input makes the pair condition exactly the geometric gate predicate.

theorem Algebraic.Aggregate.Geometry.lineSummary_quarter_of_selectedPair {n g : ℕ} (line : Line signature n g) (U : Finset (Fin n)) (h : SelectedPair line U) : 4 * {x : ↥U → Bool | lineSummary line U (Wire.elim (Cutwidth.glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false) = true}.card ≤ 2 ^ U.card

The actual line message has quarter bias whenever the selected-pair witness holds.

theorem Algebraic.Aggregate.Geometry.outputKey_quarter_of_selectedPair {n g : ℕ} (p : Program signature n g) (U : Finset (Fin n)) (out : Wire n g) (gate : Fin g) (h : SelectedPair (p.lines gate) U) : 4 * {x : ↥U → Bool | outputKey p U out (Cutwidth.glue U x fun (x : ↥Uᶜ) => false) gate.castSucc = true}.card ≤ Fintype.card (↥U → Bool)

The extra output-message coordinate does not change a gate's quarter bias.

theorem Algebraic.Aggregate.Geometry.multiCount_eq_card_filter {n g : ℕ} (p : Program signature n g) : multiCount p = {gate : Fin g | multiPrimary (p.lines gate) = true}.card

The recursive geometric gate count equals the number of qualifying actual lines.