extendMask_notin
plain-language theorem explainer
The lemma asserts that extending a partial Boolean assignment a on a Finset M of Fin n yields false at any index i outside M. Analysts of parity lower bounds or recognition complexity in finite structures cite this when simplifying expressions over extended masks. The proof is a direct one-line simplification using the definition of extendMask and the non-membership hypothesis.
Claim. Let $M$ be a finite subset of indices in a set of size $n$, and let $a$ map elements of $M$ to Boolean values. For any index $i$ not in $M$, the extended mask satisfies $extendMask(M,a)(i) = false$.
background
The lemma sits in BalancedParityHidden, which builds auxiliary facts for parity-query lower bounds under partial assignments in recognition structures. The central definition is extendMask: given a Finset M of Fin n and a partial map a from M to Bool, it returns the total function on Fin n that matches a on M and defaults to false off M. Upstream results include the base Recognition.M structure and the Cycle3.M specialization to a 3-cycle on Fin 3, both supplying the ambient recognition setting.
proof idea
The proof is a one-line wrapper that applies simp to the definition of extendMask together with the hypothesis that i is not in M. This unfolds the conditional in extendMask directly to the false branch.
why it matters
The result supplies a basic reduction for mask extensions that supports lower-bound arguments in the Recognition framework, particularly when controlling support outside active index sets. It fills a routine case needed by sibling facts such as recognition_lower_bound_sat. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.