enc_true
plain-language theorem explainer
The lemma shows that the hidden mask encoder applied with the true bit inverts the mask R at every position. Researchers analyzing balanced parity encodings in recognition systems would reference this when reducing expressions that involve bit inversion. The proof applies function extensionality followed by direct simplification on the encoder definition.
Claim. For any positive integer $n$ and function $R: [n] → {true, false}, the encoding of the true bit with mask $R$ equals the pointwise negation of $R$.
background
The encoder maps a boolean bit b and mask R to a function on [n] that returns R(i) when b is false and the negation of R(i) when b is true. This construction appears inside the module on balanced parity hidden encodings, which operates over recognition structures M consisting of a universe U and a recognition relation R. The lemma depends on the explicit definition of the encoder and on the standard recognition structure M from the Recognition and Cycle3 modules.
proof idea
The proof is a one-line term that applies function extensionality to equate the two functions on [n] and then simplifies using the definition of the encoder.
why it matters
This simp lemma supplies the true-case reduction for the encoder, supporting algebraic steps in later complexity arguments that manipulate masks under parity. It directly instantiates the encoder definition for the true bit and sits among sibling results on restriction and extension of masks. No downstream theorems are recorded yet, indicating it functions as a basic simplification tool for recognition lower-bound derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.