omega_n_queries
plain-language theorem explainer
Any decoder that must recover a hidden bit b from its masked encoding for every possible mask R cannot succeed when restricted to a query set M of size less than n. Query-complexity and circuit-lower-bound researchers in the Recognition framework would cite the result to rule out sublinear universal decoders. The proof is a one-line term application of the no_universal_decoder lemma.
Claim. Let $M$ be a finite subset of $[n]$ with $|M|<n$ and let $g$ map assignments on $M$ to booleans. Then no such $g$ satisfies $g(r_M(e(b,R)))=b$ for every boolean $b$ and every mask $R:[n]→$Bool, where $e(b,R)$ returns $R$ or its pointwise negation according to $b$ and $r_M$ projects an assignment onto the coordinates in $M$.
background
The BalancedParityHidden module introduces the encoder enc that hides bit $b$ inside mask $R$ by returning $R$ when $b$ is false and the negation of $R$ when $b$ is true. The restrict operation projects any full assignment on $n$ bits onto the coordinates belonging to the Finset $M$. The local setting is an adversarial query model for recognition tasks; the theorem relies on upstream collision-free and ledger-edge results imported from OptionAEmpiricalProgram and SimplicialLedger.EdgeLengthFromPsi.
proof idea
The proof is a term-mode one-line wrapper that applies the no_universal_decoder lemma directly to the parameters $M$, $g$ and the cardinality hypothesis $hMlt$.
why it matters
The result supplies the query lower bound invoked by recognition_lower_bound_sat and by no_sublinear_universal_decoder in CircuitLedger; it is also used inside ledger_forces_separation to exhibit the separation forced by the ledger's double-entry structure. In the Recognition Science framework it confirms that partial observation is information-theoretically insufficient, consistent with the eight-tick octave and the requirement of full index inspection for recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.