Expr
plain-language theorem explainer
The Loom grammar's content type: formulas built from signed atoms (predicate index, role-argument indices, denial flag), unordered conjunction, and binders that are universal or existential by a Boolean. Names are codebook indices only; nothing is anonymous or claim-local. Anyone citing weave, well-formedness, or quantifier conjugation starts here. The declaration is an inductive definition with decidable equality, not a proved theorem.
Claim. An expression is generated by three constructors: (i) an atom $P(a_1,\ldots,a_k)$ or its denial, with predicate index $P\in\mathbb{N}$ and argument indices $a_i\in\mathbb{N}$; (ii) unordered conjunction of two expressions; (iii) a quantifier $\forall x.B$ or $\exists x.B$, with binder index $x\in\mathbb{N}$ and body $B$. Equality of expressions is decidable.
background
The Loom module treats language as a map from content to configurations of closed walks on a shared alphabet. Content is never free text: every name is an index into a codebook that sender and receiver already share. The codebook is not pure gauge; orbit counts pin a residual choice of at least fifteen orbits that no relabelling removes.
Five production rules are forced by matching algebraic operations on configurations: ordered product of letters for a relation on roles; inversion for denial; multiset union for conjunction; binder loop with body conjugated by that oriented loop for a universal; the same with reversed binder for an existential (recovered as $\neg\forall x.\neg B$). Conjugation by the oriented binder loop, not the bare letter, makes quantifier type visible inside the scope.
Expressions sit in negation normal form by construction: denial rides only on atoms. There is no structural disjunction, because configurations have no join, and denying a multiset of loops yields "neither" rather than "not both".
proof idea
No proof body: this is an inductive type declaration. Three constructors encode the grammar (atom with denial flag, binary conjunction, quantifier with universal flag and binder index). DecidableEq and Repr are derived automatically. Downstream total maps such as weave and weaveBody pattern-match on these constructors; well-formedness and free reduction live on the image side, not in the inductive itself.
why it matters
This is the carrier of Loom content. Module siblings weave, weaveBody, wellFormed_weave, and invariant_weave_reduce interpret expressions as freely reduced closed walks, including the mandatory frame loop that makes denial orientable. Quantifier conjugation is what keeps universal and existential branches from exchanging atoms when they bind the same names in the same order; bare-letter conjugation conflates hundreds of irredundant pairs that this rule does not.
In the broader Recognition stack the Loom is the linguistic front end for recognition configurations: content in, utterance out, with spelling (free reduction) stripped from content. The inductive refuses disjunction and non-NNF denial structurally, matching the algebra of multiset union and inversion on walks rather than imposing a runtime filter. Parent uses are the weave pipeline and invariant lemmas on quantified bodies, not the unrelated certified-analytic expression tree that shares the name elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.