weaveBody
plain-language theorem explainer
Recursive map from Loom content (atoms, conjunction, quantifiers) to a multiset of freely reduced closed walks, given a shared codebook of signed generators. Anyone citing the five production rules or the content-to-utterance pipeline uses this body map. Defined by structural recursion: atoms become framed reduced words (inverted if denied), conjunction concatenates configurations, quantifiers prepend an oriented binder marker and conjugate every body loop by it.
Claim. Fix a codebook assigning each shared name a signed generator. The weave body of an expression is the configuration of closed walks defined by: an atom $P(a_1,\ldots,a_n)$, denied or not, becomes the singleton freely reduced word $p\,a_1\cdots a_n\,p$ (inverted when denied); conjunction is multiset union of the two bodies; a universal (resp. existential) binder $q$ over body $B$ yields the marker loop $[q]$ (resp. $[-q]$) followed by every loop of the body of $B$, each conjugated by that marker.
background
The Loom grammar turns accepted content into an utterance: a configuration of closed walks on the free group generated by the loom letters. Content is the inductive type with three constructors: a relation applied to role fillers in order (optionally denied), unordered conjunction, and a quantifier over a shared name (universal or existential). Names are indices into a codebook, a finite list of signed generators that sender and receiver already share; the codebook is not pure gauge (fifteen orbits are needed).
The module forces five production rules by matching algebraic operations on configurations to the operators on content: ordered product opened and closed by the predicate letter; inversion for denial; multiset union for conjunction; binder loop with body conjugated by that oriented loop for universals; the reversed binder for existentials (recovered from double negation). Configurations here are lists of words (closed walks). Free reduction is applied at the atom so spelling is not content. Denial rides only on atoms (negation-normal form), which the algebra itself enforces: inverting a binder flips universal to existential.
This definition is the body half only. The full utterance still frames the body by the complete-window loop and reduces the whole configuration; those steps live on the outer weaver.
proof idea
Not a theorem: a total recursive definition on the expression tree. Three cases.
Atom: look up the predicate letter and each argument letter in the codebook; form the word $p$ followed by the argument letters followed by $p$; freely reduce; if denied, invert the reduced word; emit a singleton configuration.
Conjunction: recurse on both sides and concatenate the resulting lists of words (multiset union).
Quantifier: look up the binder letter $q$; take marker $[q]$ if universal and $[-q]$ if existential; recurse on the body; conjugate every body word by the marker; cons the marker itself onto that list so the binder loop is visible in the utterance.
No external lemmas are invoked beyond letter lookup, free reduction, inversion, and conjugation of words.
why it matters
This is the algebraic heart of the Loom grammar: the five production rules as one total function. Downstream, the outer weaver frames the body by the complete recognition window and freely reduces the whole configuration, yielding a total content-to-utterance map answerable in linear time. Soundness of that weaver against the checker rests on every honest body being well formed.
Two sibling theorems read the body directly. The invariant of a woven utterance is independent of loop spelling, reducing through the framed body. Depth-one loop traces cannot see nesting: every loop of a quantified body is a conjugate of the corresponding body loop, so traces agree pointwise and only commutators move; that is the measured fact that traces alone fail to separate witnesses.
The conjugation-by-oriented-marker choice (not bare letter) is what makes quantifier type visible inside scope and cuts conflations from 860 to 1 on 3800 irredundant contents. Structurally there is no disjunction and no denial of conjunction: the language refuses them because configurations have no join and inversion acts loopwise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.