restrict_enc_true
The lemma shows that restricting the true-encoded mask to a query set M produces the pointwise negation of the restricted original mask. Complexity researchers working on hidden parity or recognition lower bounds invoke it when simplifying encoded assignments inside proofs. The proof is a one-line term that applies functional extensionality and then unfolds the definitions of enc and restrict.
claimFor any $R : {0,1,2,…,n-1} → {0,1}$ and any finite $M ⊆ {0,1,2,…,n-1}$, the restriction of the true-encoded mask equals the pointwise negation of the restriction of $R$, i.e., restrict(enc(true, R), M) = ¬ restrict(R, M) on the subdomain indexed by M.
background
The encoder enc takes a boolean flag b and a mask R on Fin n; it returns R unchanged when b is false and returns the pointwise negation of R when b is true. The restrictor projects any boolean-valued function on Fin n onto the subdomain indexed by a finite set M, returning a function whose domain is the subtype {i // i ∈ M}. The lemma sits inside the BalancedParityHidden module, which supplies algebraic identities for hidden-mask encodings used in parity-based recognition arguments; it directly depends on the sibling definitions of enc and restrict together with the recognition structure M imported from Recognition and Cycle3.
proof idea
The proof is a one-line term that first applies funext to reduce the function equality to a pointwise statement, then invokes simp with the definitions of restrict and enc to obtain the negation identity at each index i.
why it matters in Recognition Science
The identity supplies a basic simplification rule for encoded masks inside the Complexity module and is required for the recognition_lower_bound_sat theorem that appears later in the same file. It closes a small algebraic gap in the hidden-parity machinery without touching the T0-T8 forcing chain or the Recognition Composition Law. No open scaffolding remains; the lemma is fully proved and marked simp for routine use.
scope and limits
- Does not establish the corresponding identity when the encoding flag is false.
- Does not extend the statement to infinite index sets or non-finite M.
- Does not address probabilistic or approximate versions of the masks.
- Does not prove any uniqueness or optimality property of the encoding.
formal statement (Lean)
27@[simp] lemma restrict_enc_true (R : Fin n → Bool) (M : Finset (Fin n)) :
28 restrict (n:=n) (enc true R) M = (fun i => ! (restrict (n:=n) R M i)) := by
proof body
Term-mode proof.
29 funext i; simp [restrict, enc]
30
31/-- Extend a partial assignment on `M` to a full mask by defaulting to `false` off `M`. -/