enc
plain-language theorem explainer
The definition enc encodes a Boolean bit b by returning the mask R unchanged when b is false and the pointwise negation of R when b is true. Complexity researchers establishing query lower bounds for hidden-bit recognition cite this as the basic hiding construction. It is realized by a direct lambda that branches on b and applies negation at each index of Fin n.
Claim. Let $b$ be a Boolean and $R : [n] → {0,1}$ a mask. Define the encoder by $enc(b,R)(i) = R(i)$ if $b$ is false and $enc(b,R)(i) = ¬R(i)$ if $b$ is true.
background
This definition sits in the BalancedParityHidden module, which constructs query lower bounds showing that any decoder recovering a hidden bit from a masked parity must examine all n indices. The encoder hides b inside R by conditional negation. Sibling operations include restrict, which projects an encoded mask onto a queried subset M, together with the simplification lemmas enc_false and enc_true.
proof idea
The definition is given directly by a lambda expression performing case analysis on b: return R(i) when b is false and negate R(i) when b is true. No lemmas or tactics are applied; it is a primitive functional definition.
why it matters
enc supplies the core encoding step used by enc_false, enc_true, restrict_enc_false, restrict_enc_true, omega_n_queries and recognition_lower_bound_sat. The last two establish that no fixed-view decoder succeeds on fewer than n indices, furnishing the SAT recognition lower bound. This supports the module's contribution to information-theoretic constraints within the Recognition Science monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.