restrict
plain-language theorem explainer
The restrict definition projects a Boolean function on Fin n down to any chosen index subset M, returning a map on the subtype of elements in M. Complexity analysts working on query bounds for hidden parity in recognition structures cite it when counting probes needed to extract information from masked assignments. The implementation is a direct one-line projection that evaluates the original function at the underlying value of each restricted index.
Claim. Let $f : {0,1,…,n-1} → {true,false}$ and let $M ⊆ {0,1,…,n-1}$. The restriction $f|_M : M → {true,false}$ is defined by $(f|_M)(i) = f(i)$ for each $i ∈ M$.
background
In BalancedParityHidden, Boolean functions on finite index sets represent hidden parity bits attached to recognition queries. The upstream Recognition.M supplies the general RecognitionStructure whose universe is typically Fin n, while Cycle3.M specializes it to the cyclic triple on Fin 3 with successor recognition. The restrict definition supplies the projection that lets downstream code simulate partial observations of these structures without altering the underlying assignment.
proof idea
The definition is a one-line wrapper that applies the projection fun i => f i.val, where i.val extracts the underlying natural-number index from the subtype {i // i ∈ M}.
why it matters
This definition supports the omega_n_queries construction inside the same module and is invoked in thirty sites within ContinuumLimit2D, chiefly when establishing dominated convergence for Galerkin forcing modes and Duhamel kernels. It supplies the basic masking step that converts discrete recognition lower bounds into the continuous forcing hypotheses required for the fluid limit. No open scaffolding remains attached to the definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.