enc_false
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the corresponding identity when the bit is true.
- Does not quantify over spatial dimension or relate to the phi-ladder.
- Does not connect to physical constants or forcing-chain steps.
formal statement (Lean)
13@[simp] lemma enc_false (R : Fin n → Bool) : enc (n:=n) false R = R := by
proof body
Term-mode proof.
14 funext i; simp [enc]
15