adjacencyEdges
plain-language theorem explainer
Collects every parent-to-child labelled edge in a Loom expression tree (no artificial root). Separation and blindness arguments use it as the recursive spine of the stronger adjacency reading. Defined by structural recursion on atoms, conjunctions, and quantifiers.
Claim. Map an expression $e$ to the list of ordered pairs $(\ell_p,\ell_c)$ of node labels for every parent-to-child edge in the parse tree of $e$. Atoms yield the empty list. A conjunction yields edges from the conjunction label to each child's label, concatenated with the recursive edges of both subtrees. A quantifier yields an edge from its quantifier label to the body's label, concatenated with the body's recursive edges.
background
In Loom.Readings, two content-only readings support separation witnesses against rival carriers. The ground reading is a multiset of typed facts and binder occurrences with no nesting. The adjacency reading is strictly stronger: it also carries every parent-to-child label pair of the parse tree.
Expr (from Loom.Grammar) is content in negation-normal form: atoms (predicate, role fillers, denial flag), unordered conjunction, and quantifiers over shared codebook names. Nothing anonymous or per-claim is named in the grammar itself.
Label is what a local reading can name at a node: root, atom (with polarity folded in), conj, or quant. labelOf projects an expression to its top-node label. Equality of readings is List.Perm (decidable multiset equality), so blindness claims are kernel-checked.
proof idea
Definition by structural recursion on Expr, not a proved theorem. Pattern-match: atoms return []; conjunction prepends the two edges from Label.conj to each child's labelOf, then appends the recursive edge lists; quantifier prepends the edge from Label.quant u b to the body's labelOf, then recurses on the body. No lemmas are applied.
why it matters
Feeds adjacencyBag, which prepends the root edge (Label.root, labelOf e) so the top node is not free. That bag is the honest stronger rival in the module's separation story: a witness that only defeats ground should say so, and a reading that dropped polarity would fall to a triviality. Both readings ignore loops and depend on content alone, so a carrier blind to nesting cannot be repaired by a better encoder downstream. This is scaffolding for the Loom separation layer, not a T0-T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.