Ground
plain-language theorem explainer
Ground is the atom type for a ground reading of relational content: either a polarity-tagged fact over shared vocabulary, or a bare binder occurrence. Separation and loom-ingest arguments cite it as the carrier of what a receiver can see without nesting. It is a two-constructor inductive with decidable equality, not a proved claim.
Claim. A ground atom is either a fact $(\mathrm{pred}, \mathrm{args}, \mathrm{denied})$ with predicate index in $\mathbb{N}$, argument list in $\mathrm{List}\,\mathbb{N}$, and Boolean denial flag, or a binder occurrence $(\mathrm{universal}, \mathrm{name})$ recording whether the binder is universal and its name index. No constructor records which binder scopes a fact.
background
The Loom.Readings module fixes what a collection of local facts can see when the rival in a separation witness must be defined in Lean rather than left external. Two readings of content are introduced: the weaker ground bag and the stronger adjacency bag.
A ground reading is a multiset of typed tuples over shared vocabulary: facts over declared keys, plus counts of which binders occurred. It has no slot for nesting, because a scope node lives only inside one claim and has no name the receiver already knows. Equality of readings is list permutation (multiset equality) and is decidable, so blindness claims are kernel-checked.
Both readings are functions of content alone and never inspect loops. That is what makes separation matter: a carrier that only sees content this way cannot be repaired by a better encoder downstream.
proof idea
No proof body: this is an inductive type definition. Two constructors package the atom shapes. fact carries predicate index, argument list, and a Boolean denial flag (polarity folded into the atom, matching negation-normal form of expressions). binder carries a Boolean for universal versus existential and a name index. Deriving DecidableEq and Repr supplies equality and printing used by multiset permutation checks on ground bags.
why it matters
Ground is the payload type for groundBag, the weaker of the two honest relational readings in this module. Downstream separation and ingest arguments need a kernel-level rival that cannot express binder nesting; this inductive is that vocabulary.
It feeds the ground-bag construction used across loom separation witnesses and is referenced from complexity and gravity scaffolding that talk about ground-state or ground-layer structure. In the Recognition framing, the point is methodological: content-only carriers lose scope before encoding, so blindness is about information, not wire format.
It does not itself touch T5–T8, the RCL, or the mass ladder; it sits in the loom layer that disciplines what rival messages may carry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.