weave
plain-language theorem explainer
Maps shared codebook plus accepted content to a freely reduced configuration of closed walks: frame the woven body, then reduce. Anyone citing Loom soundness, spelling-invariant cost, or separation certificates depends on this total encoder. Definition is a one-line composition of body weaving, frame insertion, and free reduction.
Claim. Given a codebook $cb$ (list of signed generators for shared names) and an expression $e$ built from atoms, unordered conjunction, and binders, the weave of $e$ under $cb$ is the configuration $\mathrm{reduce}([\mathrm{frame}] :: \mathrm{body}(cb,e))$: prepend the frame loop that closes the recognition window, then freely reduce every loop.
background
The Loom grammar turns content into utterances. Content is the inductive type with three constructors: a relation applied to role fillers (optionally denied), unordered conjunction, and a quantifier over a shared name (universal or existential). Names are indices into a codebook, the list of signed generators that sender and receiver already share; that list is not pure gauge (fifteen orbits are needed).
Five production rules, forced by the algebra of configurations, build the body: ordered product of letters for a relation, inversion for denial, multiset union for conjunction, and binder-loop conjugation for quantifiers (existential is the dual via double denial). Two further rules make an utterance rather than a fragment: every utterance carries the frame loop (so denial has something to orient against), and every loop is freely reduced (spelling is not content).
Config here is a list of closed walks on the generator group, not the multi-distinction or ILG structures of the same name elsewhere. Free reduction is the group-word normal form used throughout the Loom core.
proof idea
Pure definition, not a proof. Body is the single composition reduceConfig ([frameGen] :: weaveBody cb e): compute the recursive body from the five production rules, cons the frame generator in front, then apply free reduction of the resulting configuration. No lemmas are invoked at the definition site; downstream theorems discharge well-formedness and invariant stability by applying the corresponding facts about reduceConfig.
why it matters
This is the total content-to-utterance map of the Loom. Soundness of the weaver against the checker is exactly well-formedness of every weave: the checker never rejects an honest utterance. The spelling-invariant theorem states that the table invariant of a weave equals the invariant of the unreduced framed body, so cost does not depend on loop spelling.
Separation certificates (weave_witnessA through D, and the two-witness separation theorem) pin concrete Python-encoder outputs to this definition by decide, so those certificates are about the grammar rather than a transcription coincidence. Semantics builds models and assignments on top of the same encoder: free names never reach an atom because weave refuses them.
In the broader Recognition picture the frame loop is the closed recognition window (eight-tick octave scale sits upstream); conjugation-by-binder rather than bare letter is what keeps quantifier type visible inside scope and collapses only one irredundant pair on the measured corpus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.