Positive and read-once Boolean formulas from tight binary-cost circuits

A one-output De Morgan circuit c : Circuit Boolean.signature n 1 on n ≥ 1 variables that depends on all n inputs must use at least n - 1 binary (AND/OR) gates (Circuit.card_inputSupport_le_cost_binaryCost). When n ≥ 1 and this bound is tight (c.program.cost binaryCost ≤ n - 1, i.e. c.program.cost binaryCost + 1 ≤ n), no gate in the backward cone of the output can share wires or use a Boolean constant, so the circuit unfolds without duplication into a constant-free negation-normal-form formula (LitFormula) of leaf size n in which each of the n variables appears at a single leaf (Circuit.exists_litFormula_of_cost_binaryCost_le).

If moreover every coordinate i : Fin n is positively essential—meaning some pair of inputs differing only at i flips the output from false to true when coordinate i is flipped from false to true—then every leaf must have positive polarity, yielding a positive (monotone) read-once formula F : PosFormula n of leaf size n and gate size n - 1 computing the same function (Circuit.exists_posFormula_of_cost_binaryCost_le) [Ilango2020FOCS, Section III.B; ECCC TR20-183, Section 3, Claim 13, p. 24].

Main definitions

• Cslib.Circuits.Boolean.LitFormula: constant-free negation-normal-form Boolean formulas built from literals lit i pol using binary and and or.
• Cslib.Circuits.Boolean.PosFormula: constant-free positive (monotone) Boolean formulas built from variables var i using binary and and or.
• Cslib.Circuits.Boolean.PosFormula.IsReadOnce: no variable appears at more than one leaf.
• Cslib.Circuits.Boolean.PosFormula.IsSubformula: the structural subformula relation.
• Cslib.Circuits.Boolean.PosFormula.flipSensitive: input coordinates in leafSupport whose flip from w₀ to true changes the formula value from false to true.
• Cslib.Circuits.Boolean.PosFormula.orFin: right-nested disjunction of m > 0 positive formulas.

Main results

• Cslib.Circuits.Program.exists_litFormula_of_card_biUnion_wireSupport_ge: a frontier of wires achieving the binary-cost support bound unfolds into constant-free NNF formulas whose leaf sizes sum to frontier.card + p.cost binaryCost.
• Cslib.Circuits.Circuit.exists_litFormula_of_cost_binaryCost_le: a one-output De Morgan circuit with full support and c.program.cost binaryCost + 1 ≤ n unfolds into a LitFormula of leaf size n.
• Cslib.Circuits.Circuit.exists_posFormula_of_cost_binaryCost_le: when every coordinate is positively essential and c.program.cost binaryCost + 1 ≤ n, the circuit is computed by a read-once PosFormula of leaf size n and size n - 1.
• Cslib.Circuits.Boolean.PosFormula.card_flipSensitive_le_numOr_add_one: a read-once positive formula has at most numOr + 1 flip-sensitive coordinates at any baseline input.
• Cslib.Circuits.Boolean.PosFormula.eval_eq_of_isSubformula_of_eval_eq: in a read-once positive formula, two inputs that agree outside a subformula's support and give the subformula the same value give the whole formula the same value.

References

• R. Ilango, Constant Depth Formula and Partial Function Versions of MCSP are Hard
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Constant-free positive (monotone) Boolean formulas

inductive Cslib.Circuits.Boolean.PosFormula (n : ℕ) : Type

A constant-free positive Boolean formula on n variables, built from input variables var i using binary conjunction (and) and disjunction (or).

• var {n : ℕ} (i : Fin n) : PosFormula n

  Input variable i.

• and {n : ℕ} (L R : PosFormula n) : PosFormula n

  Binary conjunction.

• or {n : ℕ} (L R : PosFormula n) : PosFormula n

  Binary disjunction.

@[instance_reducible]

instance Cslib.Circuits.Boolean.instDecidableEqPosFormula {n✝ : ℕ} : DecidableEq (PosFormula n✝)

def Cslib.Circuits.Boolean.instDecidableEqPosFormula.decEq {n✝ : ℕ} (x✝ x✝¹ : PosFormula n✝) : Decidable (x✝ = x✝¹)

def Cslib.Circuits.Boolean.PosFormula.eval {n : ℕ} : PosFormula n → BitString n → Bool

Evaluate a positive formula on an n-bit input.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_var {n : ℕ} (i : Fin n) (x : BitString n) : (var i).eval x = x i

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_and {n : ℕ} (L R : PosFormula n) (x : BitString n) : (L.and R).eval x = (L.eval x && R.eval x)

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_or {n : ℕ} (L R : PosFormula n) (x : BitString n) : (L.or R).eval x = (L.eval x || R.eval x)

def Cslib.Circuits.Boolean.PosFormula.leafSize {n : ℕ} : PosFormula n → ℕ

Number of variable leaves in a positive formula.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_var {n : ℕ} (i : Fin n) : (var i).leafSize = 1

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_and {n : ℕ} (L R : PosFormula n) : (L.and R).leafSize = L.leafSize + R.leafSize

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_or {n : ℕ} (L R : PosFormula n) : (L.or R).leafSize = L.leafSize + R.leafSize

def Cslib.Circuits.Boolean.PosFormula.size {n : ℕ} : PosFormula n → ℕ

Number of binary gates (and and or) in a positive formula.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.size_var {n : ℕ} (i : Fin n) : (var i).size = 0

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.size_and {n : ℕ} (L R : PosFormula n) : (L.and R).size = L.size + R.size + 1

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.size_or {n : ℕ} (L R : PosFormula n) : (L.or R).size = L.size + R.size + 1

def Cslib.Circuits.Boolean.PosFormula.numAnd {n : ℕ} : PosFormula n → ℕ

Number of and gates in a positive formula.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numAnd_var {n : ℕ} (i : Fin n) : (var i).numAnd = 0

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numAnd_and {n : ℕ} (L R : PosFormula n) : (L.and R).numAnd = L.numAnd + R.numAnd + 1

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numAnd_or {n : ℕ} (L R : PosFormula n) : (L.or R).numAnd = L.numAnd + R.numAnd

def Cslib.Circuits.Boolean.PosFormula.numOr {n : ℕ} : PosFormula n → ℕ

Number of or gates in a positive formula.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numOr_var {n : ℕ} (i : Fin n) : (var i).numOr = 0

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numOr_and {n : ℕ} (L R : PosFormula n) : (L.and R).numOr = L.numOr + R.numOr

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.numOr_or {n : ℕ} (L R : PosFormula n) : (L.or R).numOr = L.numOr + R.numOr + 1

def Cslib.Circuits.Boolean.PosFormula.leafSupport {n : ℕ} : PosFormula n → Finset (Fin n)

The set of input variables appearing at the leaves of a positive formula.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSupport_var {n : ℕ} (i : Fin n) : (var i).leafSupport = {i}

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSupport_and {n : ℕ} (L R : PosFormula n) : (L.and R).leafSupport = L.leafSupport ∪ R.leafSupport

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSupport_or {n : ℕ} (L R : PosFormula n) : (L.or R).leafSupport = L.leafSupport ∪ R.leafSupport

def Cslib.Circuits.Boolean.PosFormula.IsReadOnce {n : ℕ} : PosFormula n → Prop

A positive formula is read-once when no input variable appears at more than one leaf.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.isReadOnce_var {n : ℕ} (i : Fin n) : (var i).IsReadOnce

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.isReadOnce_and {n : ℕ} {L R : PosFormula n} : (L.and R).IsReadOnce ↔ L.IsReadOnce ∧ R.IsReadOnce ∧ Disjoint L.leafSupport R.leafSupport

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.isReadOnce_or {n : ℕ} {L R : PosFormula n} : (L.or R).IsReadOnce ↔ L.IsReadOnce ∧ R.IsReadOnce ∧ Disjoint L.leafSupport R.leafSupport

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_pos {n : ℕ} (F : PosFormula n) : 0 < F.leafSize

theorem Cslib.Circuits.Boolean.PosFormula.leafSupport_nonempty {n : ℕ} (F : PosFormula n) : F.leafSupport.Nonempty

theorem Cslib.Circuits.Boolean.PosFormula.size_add_one {n : ℕ} (F : PosFormula n) : F.size + 1 = F.leafSize

theorem Cslib.Circuits.Boolean.PosFormula.numAnd_add_numOr {n : ℕ} (F : PosFormula n) : F.numAnd + F.numOr = F.size

theorem Cslib.Circuits.Boolean.PosFormula.numAnd_add_numOr_add_one {n : ℕ} (F : PosFormula n) : F.numAnd + F.numOr + 1 = F.leafSize

theorem Cslib.Circuits.Boolean.PosFormula.card_leafSupport_le_leafSize {n : ℕ} (F : PosFormula n) : F.leafSupport.card ≤ F.leafSize

theorem Cslib.Circuits.Boolean.PosFormula.isReadOnce_iff_card_leafSupport_eq_leafSize {n : ℕ} (F : PosFormula n) : F.IsReadOnce ↔ F.leafSupport.card = F.leafSize

A positive formula is read-once if and only if its leaf support has cardinality equal to its leaf size.

theorem Cslib.Circuits.Boolean.PosFormula.eval_eq_of_eq_on_leafSupport {n : ℕ} (F : PosFormula n) {x y : BitString n} (h : ∀ i ∈ F.leafSupport, x i = y i) : F.eval x = F.eval y

Evaluation of a positive formula depends only on the variables in F.leafSupport.

theorem Cslib.Circuits.Boolean.PosFormula.monotone_eval {n : ℕ} (F : PosFormula n) : Monotone F.eval

Positive formulas compute monotone Boolean functions.

theorem Cslib.Circuits.Boolean.PosFormula.eval_eq_decide_exists_of_numAnd_eq_zero {n : ℕ} {F : PosFormula n} (h : F.numAnd = 0) (x : BitString n) : F.eval x = decide (∃ i ∈ F.leafSupport, x i = true)

A positive formula with no and gates evaluates to the disjunction of the variables in its leaf support.

Embedding into De Morgan and monotone formulas and circuits

def Cslib.Circuits.Boolean.PosFormula.toFormula {n : ℕ} : PosFormula n → Formula signature n

View a PosFormula as a De Morgan Formula.

def Cslib.Circuits.Boolean.PosFormula.toMonotoneFormula {n : ℕ} : PosFormula n → Formula Monotone.signature n

View a PosFormula as a Monotone.Formula.

def Cslib.Circuits.Boolean.PosFormula.toCircuit {n : ℕ} (F : PosFormula n) : Circuit signature n 1

Compile a PosFormula to a one-output De Morgan circuit.

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_toFormula {n : ℕ} (F : PosFormula n) (x : BitString n) : F.toFormula.eval interpretation x = F.eval x

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_toMonotoneFormula {n : ℕ} (F : PosFormula n) (x : BitString n) : F.toMonotoneFormula.eval Monotone.interpretation x = F.eval x

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_toFormula {n : ℕ} (F : PosFormula n) : F.toFormula.leafSize = F.leafSize

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.size_toFormula {n : ℕ} (F : PosFormula n) : F.toFormula.size = F.size

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.cost_binaryCost_toFormula {n : ℕ} (F : PosFormula n) : Formula.cost binaryCost F.toFormula = F.size

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.eval_toCircuit {n : ℕ} (F : PosFormula n) (x : BitString n) (j : Fin 1) : F.toCircuit.eval interpretation x j = F.eval x

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.size_toCircuit {n : ℕ} (F : PosFormula n) : F.toCircuit.size = F.size

@[simp]

theorem Cslib.Circuits.Boolean.PosFormula.cost_binaryCost_toCircuit {n : ℕ} (F : PosFormula n) : F.toCircuit.program.cost binaryCost = F.size

Subformulas and context invariance in read-once formulas

inductive Cslib.Circuits.Boolean.PosFormula.IsSubformula {n : ℕ} : PosFormula n → PosFormula n → Prop

IsSubformula T F holds when T occurs as a syntactic subformula of F.

• refl {n : ℕ} (T : PosFormula n) : T.IsSubformula T
• and_left {n : ℕ} {T L R : PosFormula n} : T.IsSubformula L → T.IsSubformula (L.and R)
• and_right {n : ℕ} {T L R : PosFormula n} : T.IsSubformula R → T.IsSubformula (L.and R)
• or_left {n : ℕ} {T L R : PosFormula n} : T.IsSubformula L → T.IsSubformula (L.or R)
• or_right {n : ℕ} {T L R : PosFormula n} : T.IsSubformula R → T.IsSubformula (L.or R)

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.leafSupport_subset {n : ℕ} {T F : PosFormula n} (h : T.IsSubformula F) : T.leafSupport ⊆ F.leafSupport

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.isReadOnce {n : ℕ} {T F : PosFormula n} (h : T.IsSubformula F) (hF : F.IsReadOnce) : T.IsReadOnce

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.trans {N : ℕ} {A B C : PosFormula N} (hAB : A.IsSubformula B) (hBC : B.IsSubformula C) : A.IsSubformula C

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.of_or_left {N : ℕ} {L R F : PosFormula N} (h : (L.or R).IsSubformula F) : L.IsSubformula F

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.of_or_right {N : ℕ} {L R F : PosFormula N} (h : (L.or R).IsSubformula F) : R.IsSubformula F

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.of_and_left {N : ℕ} {L R F : PosFormula N} (h : (L.and R).IsSubformula F) : L.IsSubformula F

theorem Cslib.Circuits.Boolean.PosFormula.IsSubformula.of_and_right {N : ℕ} {L R F : PosFormula N} (h : (L.and R).IsSubformula F) : R.IsSubformula F

theorem Cslib.Circuits.Boolean.PosFormula.eval_eq_of_isSubformula_of_eval_eq {n : ℕ} {T F : PosFormula n} (hsub : T.IsSubformula F) (hro : F.IsReadOnce) {w₁ w₂ : BitString n} (hout : ∀ v ∉ T.leafSupport, w₁ v = w₂ v) (heval : T.eval w₁ = T.eval w₂) : F.eval w₁ = F.eval w₂

In a read-once positive formula F, if T is a subformula of F and two inputs w₁, w₂ agree on all coordinates outside T.leafSupport and give T the same Boolean value, then F evaluates to the same value on w₁ and w₂.

Flip-sensitivity bound on numOr

def Cslib.Circuits.Boolean.PosFormula.flipSensitive {n : ℕ} (w₀ : BitString n) (F : PosFormula n) : Finset (Fin n)

The coordinates in F.leafSupport whose flip from w₀ to true changes F.eval from false to true.

theorem Cslib.Circuits.Boolean.PosFormula.card_flipSensitive_le_numOr_add_one {n : ℕ} (w₀ : BitString n) {F : PosFormula n} (hro : F.IsReadOnce) : (flipSensitive w₀ F).card ≤ F.numOr + 1

Gate-elimination bound on OR gates [Ilango2020FOCS, Section III.B; ECCC TR20-183, Section 3, Claim 14, p. 25]: in any read-once positive formula F, for any baseline input w₀, at most F.numOr + 1 coordinates in F.leafSupport flip F.eval from false to true.

Indexed disjunction of positive formulas

def Cslib.Circuits.Boolean.PosFormula.orFin {N : ℕ} (m : ℕ) : 0 < m → (Fin m → PosFormula N) → PosFormula N

Right-nested disjunction of m positive formulas (m > 0).

theorem Cslib.Circuits.Boolean.PosFormula.eval_orFin {N : ℕ} (m : ℕ) (hm : 0 < m) (f : Fin m → PosFormula N) (w : BitString N) : (orFin m hm f).eval w = decide (∃ (i : Fin m), (f i).eval w = true)

theorem Cslib.Circuits.Boolean.PosFormula.leafSize_orFin_of_eq {N : ℕ} (m : ℕ) (hm : 0 < m) (f : Fin m → PosFormula N) (k : ℕ) : (∀ (i : Fin m), (f i).leafSize = k) → (orFin m hm f).leafSize = m * k

theorem Cslib.Circuits.Boolean.PosFormula.mem_leafSupport_orFin {N : ℕ} (m : ℕ) (hm : 0 < m) (f : Fin m → PosFormula N) (v : Fin N) : v ∈ (orFin m hm f).leafSupport ↔ ∃ (i : Fin m), v ∈ (f i).leafSupport

Constant-free negation-normal-form Boolean formulas

inductive Cslib.Circuits.Boolean.LitFormula (n : ℕ) : Type

A constant-free negation-normal-form Boolean formula on n variables, built from literals lit i pol (x i when pol = true, !x i when pol = false) using binary and and or.

• lit {n : ℕ} (i : Fin n) (pol : Bool) : LitFormula n

  Literal on input variable i with polarity pol.

• and {n : ℕ} (L R : LitFormula n) : LitFormula n

  Binary conjunction.

• or {n : ℕ} (L R : LitFormula n) : LitFormula n

  Binary disjunction.

def Cslib.Circuits.Boolean.instDecidableEqLitFormula.decEq {n✝ : ℕ} (x✝ x✝¹ : LitFormula n✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.instDecidableEqLitFormula {n✝ : ℕ} : DecidableEq (LitFormula n✝)

def Cslib.Circuits.Boolean.LitFormula.eval {n : ℕ} : LitFormula n → BitString n → Bool

Evaluate a literal formula on an n-bit input.

def Cslib.Circuits.Boolean.LitFormula.neg {n : ℕ} : LitFormula n → LitFormula n

Negate a literal formula by De Morgan's laws, flipping the polarity of each literal and swapping and and or.

def Cslib.Circuits.Boolean.LitFormula.leafSize {n : ℕ} : LitFormula n → ℕ

Number of literal leaves in a literal formula.

def Cslib.Circuits.Boolean.LitFormula.posLeafCount {n : ℕ} : LitFormula n → ℕ

Number of positive literal leaves (lit i true) in a literal formula.

def Cslib.Circuits.Boolean.LitFormula.posSupport {n : ℕ} : LitFormula n → Finset (Fin n)

The set of input variables occurring positively (lit i true) at a leaf.

def Cslib.Circuits.Boolean.LitFormula.toPosFormula {n : ℕ} : LitFormula n → PosFormula n

Project a literal formula to a positive formula by dropping literal polarities. When all leaves have positive polarity (posLeafCount = leafSize), this preserves evaluation.

@[simp]

theorem Cslib.Circuits.Boolean.LitFormula.eval_neg {n : ℕ} (F : LitFormula n) (x : BitString n) : F.neg.eval x = !F.eval x

@[simp]

theorem Cslib.Circuits.Boolean.LitFormula.leafSize_neg {n : ℕ} (F : LitFormula n) : F.neg.leafSize = F.leafSize

@[simp]

theorem Cslib.Circuits.Boolean.LitFormula.leafSize_toPosFormula {n : ℕ} (F : LitFormula n) : F.toPosFormula.leafSize = F.leafSize

theorem Cslib.Circuits.Boolean.LitFormula.posSupport_subset_leafSupport {n : ℕ} (F : LitFormula n) : F.posSupport ⊆ F.toPosFormula.leafSupport

theorem Cslib.Circuits.Boolean.LitFormula.card_posSupport_le_posLeafCount {n : ℕ} (F : LitFormula n) : F.posSupport.card ≤ F.posLeafCount

theorem Cslib.Circuits.Boolean.LitFormula.posLeafCount_le_leafSize {n : ℕ} (F : LitFormula n) : F.posLeafCount ≤ F.leafSize

theorem Cslib.Circuits.Boolean.LitFormula.eval_toPosFormula_of_posLeafCount_eq_leafSize {n : ℕ} {F : LitFormula n} (h : F.posLeafCount = F.leafSize) (x : BitString n) : F.toPosFormula.eval x = F.eval x

theorem Cslib.Circuits.Boolean.LitFormula.eval_le_of_not_mem_posSupport {n : ℕ} {F : LitFormula n} {i : Fin n} (hi : i ∉ F.posSupport) {y₀ y₁ : BitString n} (hdiff : ∀ (k : Fin n), k ≠ i → y₀ k = y₁ k) (hy₀ : y₀ i = false) (hy₁ : y₁ i = true) : F.eval y₁ ≤ F.eval y₀

If variable i does not occur positively in F, flipping i from false to true can only decrease F.eval.

Unfolding tight binary-cost De Morgan programs into formulas

theorem Cslib.Circuits.Program.exists_litFormula_of_card_biUnion_wireSupport_ge {n g : ℕ} (hn : 0 < n) (p : Program Boolean.signature n g) (frontier : Finset (Wire n g)) (h : frontier.card + p.cost Boolean.binaryCost ≤ (frontier.biUnion p.wireSupport).card) : ∃ (F : Wire n g → Boolean.LitFormula n), (∀ w ∈ frontier, ∀ (x : BitString n), (F w).eval x = p.trace Boolean.interpretation x w) ∧ ∑ w ∈ frontier, (F w).leafSize = frontier.card + p.cost Boolean.binaryCost

When a frontier of wires in a De Morgan program achieves the binary-cost support bound frontier.card + p.cost binaryCost ≤ (frontier.biUnion p.wireSupport).card, every wire in the frontier unfolds into a constant-free NNF formula (LitFormula) such that the leaf sizes across the frontier sum to frontier.card + p.cost binaryCost.

theorem Cslib.Circuits.Circuit.exists_litFormula_of_cost_binaryCost_le {n : ℕ} (hn : 0 < n) (c : Circuit Boolean.signature n 1) (hsupp : n ≤ c.inputSupport.card) (hcost : c.program.cost Boolean.binaryCost + 1 ≤ n) : ∃ (F : Boolean.LitFormula n), (∀ (x : BitString n), F.eval x = c.eval Boolean.interpretation x 0) ∧ F.leafSize = n

A one-output De Morgan circuit with 1 ≤ n, full input support n ≤ c.inputSupport.card, and c.program.cost binaryCost + 1 ≤ n unfolds into a constant-free NNF formula F : LitFormula n of leaf size n computing c.

theorem Cslib.Circuits.Circuit.exists_posFormula_of_cost_binaryCost_le {n : ℕ} (hn : 0 < n) (c : Circuit Boolean.signature n 1) (hcost : c.program.cost Boolean.binaryCost + 1 ≤ n) (hpos : ∀ (i : Fin n), ∃ (y₀ : BitString n) (y₁ : BitString n), (∀ (k : Fin n), k ≠ i → y₀ k = y₁ k) ∧ y₀ i = false ∧ y₁ i = true ∧ c.eval Boolean.interpretation y₀ 0 = false ∧ c.eval Boolean.interpretation y₁ 0 = true) : ∃ (F : Boolean.PosFormula n), F.IsReadOnce ∧ F.leafSize = n ∧ F.size = n - 1 ∧ F.leafSupport = Finset.univ ∧ ∀ (x : BitString n), F.eval x = c.eval Boolean.interpretation x 0

Unfolding a tight binary-cost circuit into a positive read-once formula [Ilango2020FOCS, Section III.B; ECCC TR20-183, Section 3, Claim 13, p. 24]: if c is a one-output De Morgan circuit on n ≥ 1 inputs with c.program.cost binaryCost + 1 ≤ n such that every input coordinate i : Fin n is positively essential for fun x => c.eval interpretation x 0, then there exists a read-once positive formula F : PosFormula n with F.leafSize = n, F.size = n - 1, and F.leafSupport = Finset.univ that computes c.