Monotone Boolean formulas

MonotoneFormula N is a typed formula tree over N variables using only conjunction and disjunction. Its syntax makes monotonicity structural rather than a side condition on a formula with negations.

The public results prove exact compatibility with BoolFormula, semantic monotonicity, locality, and two elementary lower bounds: distinct variables and essential variables are both bounded by the number of formula leaves.

theorem Complexity.MonotoneFormula.eval_toBoolFormula {N : ℕ} (formula : MonotoneFormula N) (input : BitString N) : BoolFormula.eval input.toTotal formula.toBoolFormula = eval input formula

Erasing finite-index proofs preserves evaluation.

theorem Complexity.MonotoneFormula.size_toBoolFormula {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.size = formula.size

Erasing finite-index proofs preserves total tree size.

theorem Complexity.MonotoneFormula.leaves_toBoolFormula {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.leaves = formula.leaves

Erasing finite-index proofs preserves the leaf count.

theorem Complexity.MonotoneFormula.depth_toBoolFormula {N : ℕ} (formula : MonotoneFormula N) : formula.toBoolFormula.depth = formula.depth

Erasing finite-index proofs preserves depth.

theorem Complexity.MonotoneFormula.eval_monotone {N : ℕ} (formula : MonotoneFormula N) : IsMonotoneBoolFun fun (input : BitString N) => eval input formula

Every formula in the structurally monotone syntax computes a monotone Boolean function.

theorem Complexity.MonotoneFormula.eval_eq_of_agree {N : ℕ} (formula : MonotoneFormula N) {x y : BitString N} (agree : ∀ index ∈ formula.vars, x index = y index) : eval x formula = eval y formula

Evaluation depends only on variables that occur in the formula.

theorem Complexity.MonotoneFormula.card_vars_le_leaves {N : ℕ} (formula : MonotoneFormula N) : formula.vars.card ≤ formula.leaves

The number of distinct variables is at most the number of leaves.

theorem Complexity.MonotoneFormula.leaves_le_two_pow_depth {N : ℕ} (formula : MonotoneFormula N) : formula.leaves ≤ 2 ^ formula.depth

A depth-d binary formula has at most 2 ^ d leaves.

theorem Complexity.MonotoneFormula.essentialInputs_subset_vars {N : ℕ} (formula : MonotoneFormula N) : (essentialInputs fun (input : BitString N) (x : Fin 1) => eval input formula) ⊆ formula.vars

Every essential input of the computed one-bit function occurs in the formula.

theorem Complexity.MonotoneFormula.card_essentialInputs_le_leaves {N : ℕ} (formula : MonotoneFormula N) : (essentialInputs fun (input : BitString N) (x : Fin 1) => eval input formula).card ≤ formula.leaves

The number of essential inputs is at most the formula's leaf count.

theorem Complexity.MonotoneFormula.card_essentialInputs_le_leaves_of_computes {N : ℕ} (formula : MonotoneFormula N) (function : BitString N → Bool) (computes : formula.Computes function) : (essentialInputs fun (input : BitString N) (x : Fin 1) => function input).card ≤ formula.leaves

A formula computing function needs at least one leaf per essential input of function.