groundBag
plain-language theorem explainer
The ground reading of a loom expression flattens the parse tree into a multiset of atomic facts and binder occurrences, discarding all nesting. Separation arguments cite it as the weaker content-only rival a carrier can extract from a claim. It is defined by structural recursion on atoms, conjunctions, and quantifiers.
Claim. Map an expression $e$ to a list of ground entries: each atom with predicate $p$, argument list $\mathrm{args}$, and denial flag $d$ becomes the singleton fact $(p,\mathrm{args},d)$; a conjunction concatenates the two sub-readings; a quantifier prepends a binder entry (universality flag and binder name) and continues on the body. Nesting and scope attachment are erased.
background
In the Loom readings module, a separation witness must beat honest rivals that read only content, never loops. Two such readings are defined. The weaker one is the ground reading: a multiset of typed tuples over shared vocabulary, exactly what an ingest contract can carry (facts on declared keys, plus which binders occurred). It has no slot for nesting, because a scope node lives only inside one claim and has no receiver-known name.
Each ground entry is either a fact (predicate index, argument indices, denial bit) or a binder occurrence (universal vs existential flag, binder name). Nothing in that type can say which binder a fact sits under. Expressions are already in negation normal form, so denial lives only on atoms. Equality of readings is later stated as list permutation (multiset equality), which is decidable.
The companion adjacency reading is strictly stronger: it also carries every parent-to-child label pair of the parse tree. The ground reading exists so a witness that only defeats the weaker rival can say so explicitly.
proof idea
Pure structural definition on the three expression constructors. An atom becomes a one-element list holding that fact. A conjunction concatenates the recursive readings of the two subexpressions. A quantifier conses a binder entry for that binder onto the recursive reading of the body. No lemmas are invoked; the body is the recursion equation.
why it matters
This is the weaker of the two content-only rivals used to state separation. Downstream, groundBag_blind proves the two flagship witnesses yield the same ground multiset (as a decidable permutation), so any carrier that only ingests facts-plus-binder-counts cannot tell them apart. The module frames that blindness as the honest shape of a relational message: the distinction is already gone before encoding, so no better encoder repairs it. The stronger adjacency reading is the one the flagship actually failed against; the ground reading documents the strictly weaker bar a partial witness might still clear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.