pith. machine review for the scientific record. sign in
def definition def or abbrev high

restrict

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  20def restrict (f : Fin n → Bool) (M : Finset (Fin n)) : {i // i ∈ M} → Bool :=

proof body

Definition body.

  21  fun i => f i.val
  22

used by (30)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.