restrict_enc_false
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the corresponding equality for true-encoding of the mask.
- Does not quantify over the number of queries or derive any lower bound.
- Does not generalize beyond boolean masks to arbitrary functions.
- Does not reference the forcing chain, phi-ladder, or spatial dimension results.
formal statement (Lean)
23@[simp] lemma restrict_enc_false (R : Fin n → Bool) (M : Finset (Fin n)) :
24 restrict (n:=n) (enc false R) M = restrict (n:=n) R M := by
proof body
Term-mode proof.
25 funext i; simp [restrict, enc]
26