Model
plain-language theorem explainer
A finite relational model of size n: one shared universe Fin n together with a Boolean predicate saying which relation indices hold of which argument lists. Loom semantics uses it so that two expressions are distinct claims exactly when some model satisfies one and fails the other. Pure structure definition; no proof obligations.
Claim. A model of size $n\in\mathbb{N}$ is a single field $\mathrm{holds}:\mathbb{N}\to\mathrm{List}(\{0,\ldots,n-1\})\to\{\mathsf{true},\mathsf{false}\}$ recording, for each relation index and each finite tuple from the universe, whether that atom is true. Arity is read off the tuple; no signature is fixed in advance.
background
The Loom separation theorem only matters if two utterances really make different claims, not merely different syntax trees. This module therefore gives content a plain first-order-style semantics: exhibit one finite model where one expression holds and the other fails.
The load-bearing design choice is a single shared universe Fin n for every bound name. Names act as variables, not as sorts. A two-sorted reading (e.g. doors ranging only over doors) would separate more pairs but would be a stronger assumption and a weaker witness. Empirically, 88 of 112 pairs that already defeat a labelled-adjacency reading remain distinct on this plainer reading.
Expressions are in negation normal form, so denial lives on the atom. The grammar's weave only emits content with no free names, so assignments never need to interpret unbound variables at an atom.
proof idea
Structure definition, not a proved statement. One parameter n : Nat (universe cardinality) and one field holds, a predicate on a relation index and a list of elements of Fin n. No constructors beyond the structure, no axioms, no tactics.
why it matters
This is the semantic carrier for Loom content. Downstream evaluation (evalExpr) and the separation predicate (SeparatedBy) read truth in a Model, turning syntactic inequality of weaves into a theorem: two claims are distinct when some finite model satisfies one and not the other.
That closes the embarrassment case flagged in the module doc (trees that differ but agree as claims). The single-universe choice keeps witnesses minimal and aligns with the Recognition stance that distinctions must be forced, not assumed by extra sorts. It sits under the Loom domain that feeds gauge-orbit separation of utterances, rather than under the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.