Assign
plain-language theorem explainer
An environment maps bound variable names (naturals) to elements of a finite universe of size n. Semantic evaluation of Loom expressions threads such maps; separation witnesses use them to exhibit models where one formula holds and another fails. The definition is a plain function type, with a pointwise update helper for quantifier cases.
Claim. For $n \in \mathbb{N}$, an assignment is a map $\mathrm{Nat} \to \{0,\ldots,n-1\}$ sending each bound name to an element of the shared finite universe of cardinality $n$.
background
The Loom semantics module fixes what content means so that "different content" is not syntactic taste. The separation theorem needs two utterances in different gauge orbits only when they are genuinely different claims: some finite model makes one true and the other false. Syntactic tree inequality is not enough (two formulas can differ as trees and agree as claims).
The interpretation is deliberately plain: one finite universe shared by every bound name; a bound name is a variable, not a sort. That choice is load-bearing. A two-sorted reading (e.g. doors ranging only over doors) would separate more pairs but is a stronger assumption and weakens the witness. Measured on the searched family, 88 of 112 pairs that defeat labelled-adjacency remain distinct on this reading.
Expressions are in negation normal form, so denial sits on the atom. An assignment is the environment that evaluation uses when interpreting atoms and opening quantifiers over that finite universe.
proof idea
Definitional abbreviation: Assign n is exactly the function type from natural-number names to Fin n. No proof obligations. A companion update Assign.set env name x returns the environment that sends name to x and agrees with env elsewhere; quantifier clauses in evaluation use that pointwise override.
why it matters
Assignments are the environment parameter of expression evaluation and of the separation relation. Evaluation decides truth of content in a model because the universe is finite; two expressions are different claims when some model and environment make their Boolean values differ. That semantic distinctness is what a separation witness must exhibit, not mere syntactic inequality. The single-sorted finite-universe design keeps witnesses strong while still covering most of the searched family that defeats coarser readings. Downstream, evaluation and separation both take an assignment; without it the Loom semantics layer cannot state model-relative truth or decidable claim-difference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.