enc_true
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the corresponding identity for the false bit.
- Does not relate the encoder to any specific recognition structure M.
- Does not derive complexity bounds or query lower bounds.
- Does not address mask restriction or extension operations.
formal statement (Lean)
16@[simp] lemma enc_true (R : Fin n → Bool) : enc (n:=n) true R = (fun i => ! (R i)) := by
proof body
Term-mode proof.
17 funext i; simp [enc]
18
19/-- Restrict a full word to a queried index set `M`. -/