restrict_extendMask
plain-language theorem explainer
The lemma shows that extending a partial Boolean assignment on a finite index set M and then restricting back to M recovers the assignment unchanged. Complexity theorists studying query lower bounds for hidden-bit decoders would reference this identity when simplifying mask expressions. The proof is a direct one-line application of function extensionality followed by unfolding the definitions of restrict and extendMask.
Claim. Let $M$ be a finite subset of indices and let $a$ map elements of $M$ to Boolean values. Then restricting the extension of $a$ (which pads with false outside $M$) back to $M$ equals $a$.
background
In the BalancedParityHidden module the encoder combines a secret bit $b$ with a full mask $R$ by flipping $R$ precisely when $b$ is true. The auxiliary operations handle partial assignments on a queried index set $M$: extendMask pads a partial assignment $a$ on $M$ to a total function on all $n$ indices by defaulting to false off $M$, while restrict projects any total function back onto the subdomain $M$ (see the definitions of enc, extendMask and restrict). This identity is a basic algebraic fact used inside the module's adversarial constructions for query lower bounds.
proof idea
The proof applies function extensionality to reduce the functional equality to a pointwise statement. It then simplifies the resulting expression directly with the definitions of restrict and extendMask, which immediately returns the original partial assignment $a$ on every index inside $M$.
why it matters
The identity supports the construction of adversarial examples that fool any decoder limited to a proper subset $M$, feeding the no_universal_decoder result that forces any correct decoder to inspect all $n$ indices. It therefore contributes to the module's query lower bound, consistent with the Recognition Science emphasis on minimal recognition resources and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.