Restrictions

A restriction is a partial assignment that fixes some variables to constants and leaves the rest free — the basic operation behind random-restriction and switching-lemma arguments (roadmap track L4). This module defines restrictions, their composition, and proves that evaluating a restricted Boolean formula agrees with evaluating the original under the restriction applied to the assignment (evaluation commutes with restriction).

Main definitions and results

• Restriction, Restriction.applyTo, Restriction.comp
• Restriction.On — a finite-arity restriction suitable for finite counting
• Restriction.applyTo_comp — applying a composite restriction is applying the two in sequence
• BoolFormula.restrict, BoolFormula.eval_restrict, BoolFormula.restrict_comp — evaluation and composition laws

@[reducible, inline]

abbrev Complexity.Restriction : Type

A restriction: a partial assignment fixing some variables (some b) and leaving the rest free (none).

Equations

• Complexity.Restriction = (ℕ → Option Bool)

def Complexity.Restriction.empty : Restriction

The restriction leaving every variable free.

Equations

• Complexity.Restriction.empty x✝ = none

def Complexity.Restriction.applyTo (ρ : Restriction) (α : ℕ → Bool) : ℕ → Bool

Apply a restriction on top of a total assignment: fixed variables take the restriction's value, free variables fall back to the assignment.

Equations

• ρ.applyTo α i = (ρ i).getD (α i)

def Complexity.Restriction.comp (ρ₁ ρ₂ : Restriction) : Restriction

Compose two restrictions: the first takes precedence, the second fills in the variables the first leaves free.

Equations

• ρ₁.comp ρ₂ i = (ρ₁ i).or (ρ₂ i)

@[simp]

theorem Complexity.Restriction.empty_apply (i : ℕ) : empty i = none

@[simp]

theorem Complexity.Restriction.applyTo_empty (α : ℕ → Bool) : empty.applyTo α = α

@[simp]

theorem Complexity.Restriction.empty_comp (ρ : Restriction) : empty.comp ρ = ρ

@[simp]

theorem Complexity.Restriction.comp_empty (ρ : Restriction) : ρ.comp empty = ρ

theorem Complexity.Restriction.comp_assoc (ρ₁ ρ₂ ρ₃ : Restriction) : (ρ₁.comp ρ₂).comp ρ₃ = ρ₁.comp (ρ₂.comp ρ₃)

Restriction composition is associative, with the leftmost fixed value taking precedence.

theorem Complexity.Restriction.applyTo_comp (ρ₁ ρ₂ : Restriction) (α : ℕ → Bool) : (ρ₁.comp ρ₂).applyTo α = ρ₁.applyTo (ρ₂.applyTo α)

Applying a composite restriction is the same as applying the two restrictions in sequence.

Finite-arity restrictions

@[reducible, inline]

abbrev Complexity.Restriction.On (N : ℕ) : Type

A restriction on exactly N variables.

Unlike the ambient Restriction = Nat → Option Bool, this is a finite type and can therefore be used directly as a finite probability space.

Equations

• Complexity.Restriction.On N = (Fin N → Option Bool)

def Complexity.Restriction.On.empty {N : ℕ} : On N

The finite restriction leaving every coordinate free.

Equations

• Complexity.Restriction.On.empty x✝ = none

def Complexity.Restriction.On.single {N : ℕ} (index : Fin N) (value : Bool) : On N

Fix exactly one coordinate and leave every other coordinate free.

Equations

• Complexity.Restriction.On.single index value other = if other = index then some value else none

def Complexity.Restriction.On.comp {N : ℕ} (ρ₁ ρ₂ : On N) : On N

Left-biased composition of finite restrictions.

Equations

• ρ₁.comp ρ₂ index = (ρ₁ index).or (ρ₂ index)

def Complexity.Restriction.On.applyTo {N : ℕ} (ρ : On N) (x : BitString N) : BitString N

Apply a finite-arity restriction to a matching bit string.

Equations

• ρ.applyTo x i = (ρ i).getD (x i)

def Complexity.Restriction.On.freeVariables {N : ℕ} (ρ : On N) : Finset (Fin N)

The finite set of coordinates left free by a finite-arity restriction.

Equations

• ρ.freeVariables = {index : Fin N | ρ index = none}

def Complexity.Restriction.On.toRestriction {N : ℕ} (ρ : On N) : Restriction

Extend a finite-arity restriction by leaving every index outside its declared arity free.

Equations

• ρ.toRestriction i = if h : i < N then ρ ⟨i, h⟩ else none

@[simp]

theorem Complexity.Restriction.On.toRestriction_apply {N : ℕ} (ρ : On N) (i : Fin N) : ρ.toRestriction ↑i = ρ i

@[simp]

theorem Complexity.Restriction.On.empty_apply {N : ℕ} (index : Fin N) : empty index = none

@[simp]

theorem Complexity.Restriction.On.single_apply_self {N : ℕ} (index : Fin N) (value : Bool) : single index value index = some value

theorem Complexity.Restriction.On.single_apply_of_ne {N : ℕ} {index other : Fin N} (h : other ≠ index) (value : Bool) : single index value other = none

@[simp]

theorem Complexity.Restriction.On.applyTo_empty {N : ℕ} (x : BitString N) : empty.applyTo x = x

@[simp]

theorem Complexity.Restriction.On.mem_freeVariables {N : ℕ} (ρ : On N) (index : Fin N) : index ∈ ρ.freeVariables ↔ ρ index = none

theorem Complexity.Restriction.On.applyTo_single {N : ℕ} (index : Fin N) (value : Bool) (x : BitString N) : (single index value).applyTo x = Function.update x index value

Applying a singleton restriction is function update at its fixed index.

@[simp]

theorem Complexity.Restriction.On.empty_comp {N : ℕ} (ρ : On N) : empty.comp ρ = ρ

@[simp]

theorem Complexity.Restriction.On.comp_empty {N : ℕ} (ρ : On N) : ρ.comp empty = ρ

theorem Complexity.Restriction.On.comp_assoc {N : ℕ} (ρ₁ ρ₂ ρ₃ : On N) : (ρ₁.comp ρ₂).comp ρ₃ = ρ₁.comp (ρ₂.comp ρ₃)

theorem Complexity.Restriction.On.comp_comm_of_disjoint {N : ℕ} (first second : On N) (hdisjoint : ∀ (index : Fin N), first index = none ∨ second index = none) : first.comp second = second.comp first

Disjoint finite restrictions commute despite composition being left-biased in general.

theorem Complexity.Restriction.On.applyTo_comp {N : ℕ} (ρ₁ ρ₂ : On N) (x : BitString N) : (ρ₁.comp ρ₂).applyTo x = ρ₁.applyTo (ρ₂.applyTo x)

Finite restriction application respects left-biased composition.

def Complexity.BoolFormula.restrict (ρ : Restriction) : BoolFormula → BoolFormula

Apply a restriction to a formula, replacing each fixed variable by the corresponding constant and leaving free variables in place.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BoolFormula.restrict ρ Complexity.BoolFormula.tru = Complexity.BoolFormula.tru
• Complexity.BoolFormula.restrict ρ Complexity.BoolFormula.fls = Complexity.BoolFormula.fls
• Complexity.BoolFormula.restrict ρ φ.neg = (Complexity.BoolFormula.restrict ρ φ).neg
• Complexity.BoolFormula.restrict ρ (φ.conj ψ) = (Complexity.BoolFormula.restrict ρ φ).conj (Complexity.BoolFormula.restrict ρ ψ)
• Complexity.BoolFormula.restrict ρ (φ.disj ψ) = (Complexity.BoolFormula.restrict ρ φ).disj (Complexity.BoolFormula.restrict ρ ψ)

@[simp]

theorem Complexity.BoolFormula.restrict_empty (φ : BoolFormula) : restrict Restriction.empty φ = φ

The empty restriction is the identity on formulas.

theorem Complexity.BoolFormula.eval_restrict (ρ : Restriction) (α : ℕ → Bool) (φ : BoolFormula) : eval α (restrict ρ φ) = eval (ρ.applyTo α) φ

Evaluation commutes with restriction. Evaluating a restricted formula at α equals evaluating the original formula at the restriction applied to α.

theorem Complexity.BoolFormula.restrict_comp (ρ₁ ρ₂ : Restriction) (φ : BoolFormula) : restrict ρ₂ (restrict ρ₁ φ) = restrict (ρ₁.comp ρ₂) φ

Applying ρ₁ and then ρ₂ to a formula is syntactically the same as applying their left-biased composition.

theorem Complexity.BoolFormula.restrict_size (ρ : Restriction) (φ : BoolFormula) : (restrict ρ φ).size = φ.size

Restriction preserves the tree size: fixing a variable replaces a leaf by a constant leaf, and connectives are untouched. So (restrict ρ φ).size = φ.size — restriction never grows a formula (a fact width/size arguments rely on).

theorem Complexity.BoolFormula.restrict_leaves (ρ : Restriction) (φ : BoolFormula) : (restrict ρ φ).leaves = φ.leaves

Restriction also preserves the leaf count: (restrict ρ φ).leaves = φ.leaves.

theorem Complexity.BoolFormula.restrict_depth (ρ : Restriction) (φ : BoolFormula) : (restrict ρ φ).depth = φ.depth

Restriction preserves the formula depth exactly: it only relabels leaves, leaving the connective tree — and hence every root-to-leaf path length — untouched. So (restrict ρ φ).depth = φ.depth.

theorem Complexity.BoolFormula.vars_restrict_subset (ρ : Restriction) (φ : BoolFormula) : (restrict ρ φ).vars ⊆ φ.vars

Restriction only ever removes variables: vars (restrict ρ φ) ⊆ vars φ. Fixing a variable turns its leaf into a constant (dropping it); free variables are untouched. This is the variable-tracking fact switching-lemma arguments use to bound the surviving support after a random restriction.

theorem Complexity.BoolFormula.vars_restrict_eq_filter (ρ : Restriction) (φ : BoolFormula) : (restrict ρ φ).vars = {i ∈ φ.vars | ρ i = none}

Restriction removes exactly the fixed variables from a formula's support.