pith. machine review for the scientific record. sign in
def definition def or abbrev high

enc

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  10def enc (b : Bool) (R : Fin n → Bool) : Fin n → Bool :=

proof body

Definition body.

  11  fun i => if b then ! (R i) else R i
  12

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.