circuit_cannot_sense_moat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim that every circuit of size exponential in n fails on SAT.
- Does not address circuits with adaptive or quantum queries.
- Does not quantify the precise depth required to simulate the moat check.
- Does not prove an unconditional P ≠ NP statement outside the Recognition Science ledger model.
formal statement (Lean)
215theorem circuit_cannot_sense_moat
216 (n : ℕ) (_hn : 0 < n)
217 (M : Finset (Fin n)) (hM : M.card < n)
218 (decoder : ({i // i ∈ M} → Bool) → Bool) :
219 ∃ (b : Bool) (R : Fin n → Bool),
220 decoder (restrict (enc b R) M) ≠ b :=
proof body
Term-mode proof.
221 adversarial_failure M decoder
222
223/-- **THEOREM (Sublinear Circuit Cannot Universally Decode).**
224 No circuit querying fewer than n inputs can universally decode
225 the balanced-parity encoding. -/