Certificates and functional restrictions

CSLib's QueryComplexity.PartialAssignment n is definitionally the arbitrary-coordinate BitString.PartialAssignment (Fin n). The two agreement and support predicates also agree definitionally, so the generic restriction operations apply without conversions.

Main results

• Cslib.QueryComplexity.fill_restrict: filling a coordinate certificate is a piecewise input.
• Cslib.QueryComplexity.forces_iff_forall_fill: a forcing assignment makes the restricted function constant.

References

• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey

@[simp]

theorem Cslib.QueryComplexity.fill_restrict {n : ℕ} (x : BitString n) (S : Finset (Fin n)) (y : BitString n) : BitString.PartialAssignment.fill (restrict x S) y = S.piecewise x y

Filling a partial assignment read from x uses x on its support and y elsewhere.

theorem Cslib.QueryComplexity.forces_iff_forall_fill {n : ℕ} (f : BooleanFunction n) (C : PartialAssignment n) (b : Bool) : Forces f C b ↔ ∀ (x : Fin n → Bool), f (BitString.PartialAssignment.fill C x) = b

An assignment forces b precisely when filling arbitrary inputs always produces value b.