extendMask_notin
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not determine the value of the extension at indices inside M.
- Does not invoke any property of the recognition structure beyond the Finset M.
- Does not apply when the index belongs to M.
- Does not use the cycle construction from Cycle3.M.
formal statement (Lean)
39@[simp] lemma extendMask_notin (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∉ M) :
40 extendMask (n:=n) M a i = false := by
proof body
One-line wrapper that applies simp.
41 simp [extendMask, h]
42