rs_adversarial_lower_bound
plain-language theorem explainer
Any decoder g that inspects only a proper subset M of variables can be fooled by suitable choice of secret bit b and full mask R. Complexity theorists studying natural proofs would cite this as the Recognition Science formulation of the barrier against local certificates for unsatisfiability. The proof reduces immediately to the adversarial_failure result in BalancedParityHidden.
Claim. For any natural number $n$, any finite subset $M$ of the indices $[n]$, and any function $g$ from assignments on $M$ to a bit, there exist a bit $b$ and a full assignment $R$ on $[n]$ such that $g$ applied to the restriction of the encoded mask (flipped according to $b$) differs from $b$.
background
The BalancedParityHidden module supplies the encoder enc(b, R) that returns R when b is false and the bitwise negation of R when b is true, together with the restrict operation that projects a full assignment onto the coordinates in M. These definitions formalize a hidden-mask encoding whose local views can be adversarially controlled. The present theorem lives inside the R̂ SAT Encoding module, whose MODULE_DOC states that R̂ supplies a non-natural polytime certifier separating recognition-time complexity from Turing computation time, with the natural-proof-barrier connection listed as a hypothesis.
proof idea
The proof is a one-line wrapper that directly invokes BalancedParityHidden.adversarial_failure on the supplied M and g.
why it matters
This supplies the combinatorial content for the natural-proof-barrier link inside the R̂ SAT Encoding module. It shows that no local property of the formula can certify unsatisfiability, supporting the module's claim that R̂ reaches zero J-cost for satisfiable instances in O(n) steps while unsatisfiable instances encounter topological obstructions. The result aligns with the Recognition Science separation of recognition-time complexity from Turing time without claiming a full P ≠ NP theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.