recognition_lower_bound_sat
plain-language theorem explainer
Any decoder that recovers a hidden bit from its masked or complemented version must query every one of the n positions; when restricted to a proper subset M the decoder necessarily fails on some bit and mask pair. Complexity researchers cite the result for query-complexity lower bounds on recognition tasks. The argument is a one-line wrapper that invokes the omega_n_queries theorem after classical reasoning.
Claim. For any natural number $n$, any subset $M$ of indices with $|M|<n$, and any function $g$ from Boolean assignments on $M$ to Boolean values, no such $g$ satisfies: for every bit $b$ and every mask $R$, $g$ applied to the restriction of the encoded word equals $b$, where the encoding returns the mask when $b$ is false and its complement when $b$ is true.
background
The module defines a hidden-mask encoder that returns the input mask $R$ when the hidden bit is false and the pointwise complement when the bit is true. The restrict operation projects any full-length Boolean word onto the coordinates in the queried set $M$. The upstream theorem omega_n_queries states that any universally correct decoder must inspect all $n$ indices in the worst case; its proof rests on the auxiliary lemma no_universal_decoder. The two Recognition.M definitions supply the ambient structure in which these complexity statements are embedded.
proof idea
The proof opens classical reasoning, then applies simpa to reduce the goal directly to the statement of omega_n_queries (n:=n) M g hMlt. That theorem in turn calls no_universal_decoder, discharging the universal quantifier over bits and masks by exhibiting an adversarial pair on which any partial-view decoder errs.
why it matters
The declaration supplies a proved, dimensionless query lower bound inside the Complexity section of the Recognition Science development. It closes the information-theoretic side of recognition by showing that partial views are insufficient for universal correctness, consistent with the framework's emphasis on full inspection in the forcing chain. No downstream theorems are recorded, leaving the result as a terminal complexity fact available for later integration with mass or constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.