recognition_lower_bound_sat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when the queried set has full cardinality n.
- Does not construct or exhibit any decoder.
- Covers only the specific mask-or-complement encoding.
- Addresses worst-case adversarial inputs, not average-case behavior.
- Remains silent on probabilistic or approximate decoders.
formal statement (Lean)
105theorem recognition_lower_bound_sat
106 (n : ℕ) (M : Finset (Fin n))
107 (g : (({i // i ∈ M} → Bool)) → Bool)
108 (hMlt : M.card < n) :
109 ¬ (∀ (b : Bool) (R : Fin n → Bool),
110 g (Complexity.BalancedParityHidden.restrict
111 (Complexity.BalancedParityHidden.enc b R) M) = b) := by
proof body
Term-mode proof.
112 classical
113 simpa using
114 (Complexity.BalancedParityHidden.omega_n_queries (n:=n) M g hMlt)
115
116end IndisputableMonolith