circuit_cannot_sense_moat
plain-language theorem explainer
Any decoder reading fewer than n input bits fails to recover the hidden bit b for some choice of b and mask R in the balanced parity encoding. Circuit theorists working on lower bounds for SAT would cite this to separate poly-size circuits from full-ledger recognition. The proof is a one-line wrapper that invokes the adversarial failure lemma on the given M and decoder.
Claim. For every natural number $n > 0$, every subset $M$ of the $n$ indices with $|M| < n$, and every function $d$ from assignments on $M$ to a Boolean, there exist a bit $b$ and a mask $R$ such that $d$ applied to the restriction of the encoded string (bit $b$ masked by $R$) to $M$ differs from $b$.
background
The module treats Boolean circuits as feed-forward sub-ledgers whose gates see only local parents, in contrast to the global J-cost gradient on the full Z³ lattice. The balanced parity encoding hides a bit $b$ inside a mask $R$: the full word is $R$ when $b$ is false and the negation of $R$ when $b$ is true. The restrict operation projects any full word onto the queried coordinates in $M$. The defect moat is the J-cost gap of at least 1 that separates satisfiable from unsatisfiable assignments, proved earlier in RSatEncoding.
proof idea
The proof is a one-line wrapper that applies the adversarial_failure lemma from BalancedParityHidden to the supplied subset M and decoder. That lemma directly constructs the required b and R by flipping the hidden bit on the unseen coordinates, forcing the decoder output to disagree with b.
why it matters
This theorem closes the third stage of the module's separation argument: a poly-size circuit whose Z-capacity is bounded by its gate count cannot cross the defect moat because it lacks full n-bit visibility. It sits downstream of the BalancedParityHidden adversarial lower bound and upstream of the open spectral-gap-to-TM-step translation needed for the full P-vs-NP claim in Recognition Science. The result sharpens the claim that any circuit querying fewer than n variables can be fooled on satisfiability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.