Label
plain-language theorem explainer
Finite vocabulary for what a local reading of a parse-tree node may name: root, atomic predicate (with polarity), conjunction, or quantifier binder. Separation and adjacency constructions cite it as the shared alphabet of ground and edge bags. The declaration is a pure inductive type with decidable equality; no proof obligations.
Claim. A label is one of: the distinguished root; an atom given by a predicate index $p \in \mathbb{N}$, a list of argument indices, and a denial flag; a conjunction marker; or a quantifier marker carrying a universality bit and a binder index. Equality of labels is decidable.
background
The Loom readings module fixes what a relational message can honestly carry about claim content, without looking at loops. Two readings are defined: a ground multiset of typed facts over shared vocabulary (plus binder occurrences), and a strictly stronger adjacency multiset of parent-to-child label pairs from the parse tree.
Labels are the common alphabet of those readings. An atom folds polarity into the label itself (negation-normal form), so a reading that dropped denial would lose to a trivial counterexample. Conjunction and quantifier constructors name internal nodes; the root marks the top edge so the top node is not free in the adjacency bag.
The module imports the Loom grammar for Expr. Equality of readings is list permutation (multiset equality) and is kernel-checked in separation claims.
proof idea
No proof body: this is an inductive type declaration. The four constructors enumerate the local names a reading may attach to a node. DecidableEq and Repr are derived automatically, so later multiset and adjacency comparisons are decidable by construction.
why it matters
Every ground and adjacency bag is built from these labels. Downstream, labelOf assigns a label to each expression, adjacencyEdges and adjacencyBag emit parent-child pairs, and separation witnesses compare those bags by permutation. Gravity-side Gap-2 accounting (gauge volume status, posting-move cardinality, orbit-stabilizer label counts, pinned-weight collapse) reuses the same label vocabulary when counting irreducible inputs and posting layers. The definition therefore sits under the Loom separation claim: content-only readings cannot recover nesting that the ground bag never carried, independent of any later encoder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.