enc_false
plain-language theorem explainer
The lemma shows that the hidden mask encoder applied to the false bit returns its input mask unchanged. Researchers establishing query lower bounds via parity arguments in complexity settings would invoke this identity to eliminate trivial cases. The proof is a one-line term that reduces the functional equality via extensionality and simplifies directly against the encoder definition.
Claim. For any natural number $n$ and any map $R$ from the finite set of size $n$ to the booleans, the hidden mask encoder applied to false and $R$ equals $R$.
background
The module introduces the hidden mask encoder whose definition states that the bit b with mask R is R if b is false and the pointwise negation of R if b is true. This construction supports parity-based arguments that track how an unknown bit flips or preserves a reference mask. The upstream definition of the encoder supplies the computational rule that the present lemma specializes to the false case.
proof idea
The proof is a one-line term-mode wrapper. It applies function extensionality to reduce the equality of functions to pointwise equality on Fin n, then simplifies using the encoder definition, which yields the identity immediately when the boolean argument is false.
why it matters
This identity supplies a basic simplification rule inside the development of parity-based complexity bounds. It carries the simp attribute so that it fires automatically when expressions involving the encoder appear in later lemmas on recognition lower bounds. Within the Recognition Science framework it supports the analysis of query complexity in the complexity domain without adding hypotheses on the mask.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.