restrict_extendMask
The lemma shows that extending a partial Boolean assignment on a finite index set M and then restricting back to M recovers the assignment unchanged. Complexity theorists studying query lower bounds for hidden-bit decoders would reference this identity when simplifying mask expressions. The proof is a direct one-line application of function extensionality followed by unfolding the definitions of restrict and extendMask.
claimLet $M$ be a finite subset of indices and let $a$ map elements of $M$ to Boolean values. Then restricting the extension of $a$ (which pads with false outside $M$) back to $M$ equals $a$.
background
In the BalancedParityHidden module the encoder combines a secret bit $b$ with a full mask $R$ by flipping $R$ precisely when $b$ is true. The auxiliary operations handle partial assignments on a queried index set $M$: extendMask pads a partial assignment $a$ on $M$ to a total function on all $n$ indices by defaulting to false off $M$, while restrict projects any total function back onto the subdomain $M$ (see the definitions of enc, extendMask and restrict). This identity is a basic algebraic fact used inside the module's adversarial constructions for query lower bounds.
proof idea
The proof applies function extensionality to reduce the functional equality to a pointwise statement. It then simplifies the resulting expression directly with the definitions of restrict and extendMask, which immediately returns the original partial assignment $a$ on every index inside $M$.
why it matters in Recognition Science
The identity supports the construction of adversarial examples that fool any decoder limited to a proper subset $M$, feeding the no_universal_decoder result that forces any correct decoder to inspect all $n$ indices. It therefore contributes to the module's query lower bound, consistent with the Recognition Science emphasis on minimal recognition resources and the eight-tick octave structure.
scope and limits
- Does not address infinite index sets or continuous domains.
- Does not analyze the full encoder enc or its parity properties.
- Does not derive numerical query bounds or complexity classes.
- Does not connect to phi-ladder mass formulas or physical constants.
formal statement (Lean)
43@[simp] lemma restrict_extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) :
44 restrict (n:=n) (extendMask (n:=n) M a) M = a := by
proof body
Tactic-mode proof.
45 funext i
46 simp [restrict, extendMask]
47
48/-- Any fixed-view decoder on a set `M` of queried indices can be fooled by a suitable `(b,R)`. -/
49 theorem adversarial_failure (M : Finset (Fin n))
50 (g : (({i // i ∈ M} → Bool)) → Bool) :
51 ∃ (b : Bool) (R : Fin n → Bool),
52 g (restrict (n:=n) (enc b R) M) ≠ b := by
53 classical
54 -- Pick an arbitrary local view `a` and force the decoder to predict `b' := g a`.
55 let a : {i // i ∈ M} → Bool := fun _ => false
56 let b' : Bool := g a
57 -- Choose the true bit to be the opposite of the decoder's prediction.
58 let b : Bool := ! b'
59 -- Choose the mask so that the restricted encoding equals `a`.
60 let R : Fin n → Bool :=
61 if b then extendMask M (fun i => ! (a i)) else extendMask M a
62 have hRestr : restrict (n:=n) (enc b R) M = a := by
63 funext i
64 dsimp [restrict, enc, R, extendMask]
65 by_cases hb : b
66 · -- b = true
67 simp [hb, dif_pos i.property]
68 · -- b = false
69 simp [hb, dif_pos i.property]
70 refine ⟨b, R, ?_⟩
71 have hval' : g (restrict (n:=n) (enc b R) M) = g a := by
72 simpa [hRestr]
73 have hval : g (restrict (n:=n) (enc b R) M) = b' := by
74 simpa [b'] using hval'
75 have hbrel : b = ! b' := rfl
76 have ne : b' ≠ ! b' := by cases b' <;> decide
77 have : g (restrict (n:=n) (enc b R) M) ≠ ! b' := by simpa [hval]
78 simpa [hbrel]
79
80/-- If a decoder is correct for all `(b,R)` while querying only `M`, contradiction. -/
81 theorem no_universal_decoder (M : Finset (Fin n))
82 (g : (({i // i ∈ M} → Bool)) → Bool) :
83 ¬ (∀ (b : Bool) (R : Fin n → Bool), g (restrict (n:=n) (enc b R) M) = b) := by
84 classical
85 intro h
86 rcases adversarial_failure (n:=n) M g with ⟨b, R, hw⟩
87 have := h b R
88 exact hw this
89
90/-- Query lower bound (worst-case, adversarial): any universally-correct decoder
91 must inspect all `n` indices. -/