extendMask_in
The lemma asserts that the mask extension returns the original assignment value exactly at indices inside the support M. Researchers proving query lower bounds for hidden parity in recognition structures would cite it to simplify mask expressions. The proof is a one-line simp wrapper that unfolds the conditional definition of extendMask and applies the membership hypothesis.
claimLet $M$ be a finite subset of indices and $a$ a partial assignment from $M$ to Boolean values. For any index $i$ belonging to $M$, the total extension satisfies $extendMask(M,a)(i)=a(i)$.
background
extendMask takes a finite index set $M$ and a partial Boolean map $a$ defined only on $M$, then produces a total map on all $n$ indices by returning the value of $a$ inside $M$ and false outside. The surrounding module works inside the Complexity domain on balanced parity arguments that embed partial assignments into full recognition structures. Upstream results supply the concrete definition of extendMask as the conditional that encodes the default-false rule, together with the basic Recognition structure $M$ and its three-cycle instantiation used for concrete lower-bound examples.
proof idea
The proof is a one-line simp wrapper. It unfolds the definition of extendMask and matches the membership hypothesis $h$ to select the branch that returns the value from $a$.
why it matters in Recognition Science
The lemma supplies a recurring simplification step inside proofs of recognition query lower bounds, including the recognition_lower_bound_sat result in the same module. It closes the in-support case for mask manipulations that arise when partial assignments are lifted into full recognition structures such as the three-cycle $M$. Within the Recognition Science framework it supports the complexity analysis that constrains the number of queries needed to distinguish structures.
scope and limits
- Does not specify the value returned for indices outside $M$.
- Does not depend on properties of the recognition relation $R$.
- Does not constrain the size of $n$ or $M$ beyond finiteness.
- Does not interact with $J$-cost, defect distance, or the phi-ladder.
formal statement (Lean)
35@[simp] lemma extendMask_in (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∈ M) :
36 extendMask (n:=n) M a i = a ⟨i, h⟩ := by
proof body
One-line wrapper that applies simp.
37 simp [extendMask, h]
38