Prove2Me

Proof of Proposition 5.1 — fG(x)=1f_G(x)=1 iff one of three mutually exclusive colour conditions holds

Proved
DDNNFNeg.proposition_5_1_three_conditions

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

boolean-functionscircuit-complexityknowledge-compilationp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1

Let GG be a graph on [n][n] with an edge colouring by the colours 1,2,31, 2, 3, and for x∈{0,1}[n]x \in \{0,1\}^{[n]} write HcH_c for "GxG_x contains colour cc". Then

fG(x)=1  ⟺  (H1∧¬H2)∨(H2∧¬H3)∨(H3∧¬H1),f_G(x) = 1 \iff (H_1 \wedge \neg H_2) \vee (H_2 \wedge \neg H_3) \vee (H_3 \wedge \neg H_1),

and the three conditions H1∧¬H2H_1 \wedge \neg H_2, H2∧¬H3H_2 \wedge \neg H_3, H3∧¬H1H_3 \wedge \neg H_1 are pairwise mutually exclusive.

This rewrites fGf_G as a disjunction of three disjoint events, each computable by a small OBDD, which is how the linear d-DNNF upper bound is obtained.

Formalization Note Colours 1,2,31, 2, 3 are 0,1,2∈Fin 30, 1, 2 \in \mathrm{Fin}\,3.

Differences from the source:

  • generalization: G 3-regular with a proper 3-edge-colouring → any graph on Fin n and any colouring by three colours; reason: the equivalence and the exclusivity are propositional and use neither regularity nor properness; the paper's G is a special case
  • encoding: colours 1, 2, 3 → 0, 1, 2 : Fin 3; reason: Lean convention; same instances
Preamble
import Mathlib
import Definitions.Def_DDNNFNeg_fG
Formal statement
namespace DDNNFNeg

/-- **Proof of Proposition 5.1**, the three exclusive conditions (Arenas–Broadrick–Liew–Van den Broeck, *d-DNNF is Not Polynomially Closed Under Negation*, STOC 2027 submission manuscript (sha256 64e42127…fbb68), p.11): `f_G(x) = 1` if
and only if `G_x` contains colour 1 but not colour 2, or colour 2 but not colour 3, or colour 3
but not colour 1; and the three conditions are mutually exclusive.

**Formalization Note** Colours `1, 2, 3` are `0, 1, 2 : Fin 3`. The statement holds for every
graph on `Fin n` and every colouring, so the paper's 3-regularity and properness are not
assumed. -/
theorem proposition_5_1_three_conditions {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (c : Sym2 (Fin n) → Fin 3) (x : Fin n → Bool) :
    (fG G c x = true ↔
      (HasColor G c x 0 ∧ ¬ HasColor G c x 1) ∨ (HasColor G c x 1 ∧ ¬ HasColor G c x 2) ∨
        (HasColor G c x 2 ∧ ¬ HasColor G c x 0)) ∧
    ¬ ((HasColor G c x 0 ∧ ¬ HasColor G c x 1) ∧ (HasColor G c x 1 ∧ ¬ HasColor G c x 2)) ∧
    ¬ ((HasColor G c x 0 ∧ ¬ HasColor G c x 1) ∧ (HasColor G c x 2 ∧ ¬ HasColor G c x 0)) ∧
    ¬ ((HasColor G c x 1 ∧ ¬ HasColor G c x 2) ∧ (HasColor G c x 2 ∧ ¬ HasColor G c x 0)) := by sorry

end DDNNFNeg
Source
Arenas–Broadrick–Liew–Van den Broeck, d-DNNF is Not Polynomially Closed Under Negation, STOC 2027 submission manuscript (sha256 64e4212767c37c44…fbb68), proof of Proposition 5.1, p.11
Human review

  • Endorsed by Shuze Chen · Nov 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph