extendMask
plain-language theorem explainer
The definition takes a finite set M of indices together with a boolean assignment a on M and returns the total function on all n indices that agrees with a on M and is false off M. Researchers analyzing query complexity or partial-view lower bounds inside Recognition Science would cite it when constructing fooling assignments for decoders. The implementation is the direct conditional expression that branches on membership in M.
Claim. Let $M$ be a finite subset of the index set $I = {0,1,…,n-1}$ and let $a$ map each element of $M$ to a boolean. The extended mask is the total function $f:I→{true,false}$ given by $f(i)=a(i)$ whenever $i∈M$ and $f(i)=false$ otherwise.
background
In BalancedParityHidden, masks encode partial assignments that arise when a decoder is allowed only a restricted set of queries. The upstream RecognitionStructure M supplies the universe U together with the recognition relation R; Cycle3.M instantiates this structure on the three-element cycle whose successor relation is the modular successor on Fin 3. The sibling definitions enc, restrict and their variants supply the complementary operations that turn total masks into partial ones and back.
proof idea
The definition is given directly by the lambda expression fun i => if h : i ∈ M then a ⟨i,h⟩ else false. No lemmas are invoked; the expression simply uses the standard Finset membership test and the dependent function type {i // i ∈ M} → Bool.
why it matters
extendMask feeds the three immediate lemmas extendMask_in, extendMask_notin and restrict_extendMask that simplify mask manipulations in downstream arguments. The last of these lemmas records that any fixed-view decoder on a queried set M can be fooled by a suitable (b,R) pair. Within Recognition Science the construction therefore supports lower-bound arguments that relate the number of queries to the ability to distinguish recognition structures, consistent with the query-complexity side of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.