adjacencyBag
plain-language theorem explainer
The adjacency reading of a loom expression is the multiset of every parent-to-child label pair in its parse tree, headed by a synthetic root edge to the top node. Separation arguments cite it as the stronger local view of content: any carrier that only sees labelled adjacencies cannot tell the flagship pair apart. The body is a one-line cons of that root edge onto the recursive edge list.
Claim. For a loom expression $e$, the adjacency reading is the list $(\mathrm{root},\,\ell(e))$ followed by every parent-to-child label edge of the parse tree of $e$, where $\ell$ sends each subexpression to its local label (atom with polarity, conjunction, or quantifier binder).
background
The Loom readings module fixes what a collection of local facts can see about accepted content. Content is a loom expression: an atom (predicate index, role fillers, denial flag), an unordered conjunction, or a quantifier over a shared binder name. Names are codebook indices only; nothing anonymous or per-claim is named in the grammar itself.
A node's label is the fragment a local reading can name: a distinguished root, an atom carrying polarity, a bare conjunction mark, or a quantifier mark with universality and binder index. The map from expression to label forgets children and keeps only that local tag. The recursive edge list walks the parse tree and emits every parent label paired with each child's label (empty on atoms; two conj edges plus recursions on conjunctions; one quant edge plus recursion on quantifiers).
The module contrasts two honest relational readings. The ground reading is a multiset of typed facts and binder occurrences with no nesting. The adjacency reading is strictly stronger: it also carries the labelled parent-to-child skeleton. Denial is folded into atom labels because expressions are already in negation-normal form. Equality of readings is list permutation (multiset equality), which is decidable.
proof idea
Pure definition, not a proof. The body prepends the single synthetic edge from the distinguished root label to the label of the whole expression onto the recursive parent-to-child edge list. That recursive list is defined by structural recursion on atoms (empty), conjunctions (two edges from the conj label plus concatenated sublists), and quantifiers (one edge from the quant label plus the body list). No lemmas are applied.
why it matters
This is the stronger of the two content-only readings used to state blindness of rivals in the separation development. Downstream, the theorem that the adjacency reading is blind shows that every parent-to-child label pair (denial folded into atoms) is the same, up to permutation, for the two flagship witnesses. The module doc is explicit: that is the rival the flagship failed against, so no reading of content as a collection of locally labelled facts can tell them apart.
Because the reading never inspects loops and depends only on content, a carrier limited to this view cannot be repaired by a better encoder later; the distinction is already erased. The definition exists so a witness that only defeats the weaker ground rival can still be stated honestly against this stronger bag. It sits in the Loom separation chain rather than the T0-T8 forcing spine, but it is the concrete object that makes the decidable permutation checks in Separation meaningful.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.