restrict_enc_false
plain-language theorem explainer
The lemma establishes that restricting a false-encoded mask to a query set yields the identical result as restricting the original mask. Researchers deriving query lower bounds for hidden parity models in recognition structures cite this to simplify encoded expressions during reductions. The proof is a one-line term that applies functional extensionality followed by definitional simplification on the encoder and restrictor.
Claim. Let $R$ map indices in a set of size $n$ to boolean values and let $M$ be a finite subset of those indices. Then the restriction of the false-encoded version of $R$ to $M$ equals the restriction of $R$ to $M$, where false-encoding leaves the mask unchanged.
background
The encoder takes a boolean bit $b$ and mask $R$, returning $R$ itself when $b$ is false and the pointwise negation of $R$ when $b$ is true. The restrict operation projects a full bit vector onto a queried finite subset $M$ by restricting its domain to the elements of $M$ while preserving the boolean values at those positions.
proof idea
This is a one-line term proof that applies functional extensionality to equate the two restricted functions pointwise, then simplifies both sides directly using the definitions of restrict and the encoder.
why it matters
The lemma supplies a basic simplification rule for false-encoded masks inside the BalancedParityHidden module, supporting reductions needed for recognition lower-bound arguments. It operates within the complexity analysis of recognition structures and cycle-based models, enabling clean substitution steps without altering the underlying query behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.