trN_weaveBody_quant
plain-language theorem explainer
Wrapping a body in a quantifier conjugates every body loop by the binder loop, so normalized matrix traces agree pointwise with those of the bare body (after dropping the binder loop). Anyone comparing loop-trace invariants of loom utterances cites this. The proof is a short simp-and-map-congruence argument reducing to conjugation invariance of the normalized trace.
Claim. Let $T$ be a valid letter table, $cb$ a codebook, $u$ a quantifier polarity, $b$ a binder index, and $B$ a body expression. Write $W$ for the list of freely reduced loops produced by weaving the quantified formula, and $W_B$ for those of $B$. Then the list of normalized traces $\mathrm{tr}_N$ of the matrix images under $T$ of the tail of $W$ equals the corresponding list for $W_B$.
background
In the Loom grammar, content is an Expr: atoms, unordered conjunction, and quantifiers over shared codebook names. The total map weave turns content into a configuration of closed walks on the letter group. A quantifier is realized as a binder loop whose body loops are conjugated by that same oriented loop (universal) or its reverse (existential). Conjugation by the oriented binder loop, not the bare letter, is what makes quantifier type visible from inside the scope.
A Table assigns matrices to signed generators; evalWord multiplies those matrices along a word. Mat.trN is the normalized matrix trace used as a loop invariant. The sibling weaveBody is the recursive production that builds the multiset of loops for an expression before the outer frame is attached. The hypothesis Table.ok T ensures the table is a valid representation so conjugation identities hold.
The module setting is that five production rules are forced by matching algebraic operations on configurations to the operators of the content language. Free reduction and a mandatory frame loop turn a fragment into an utterance.
proof idea
Unfold weaveBody on the quantifier constructor: the weave is the binder loop consed onto the body loops each conjugated by that binder word. List.tail_cons drops the binder loop; List.map_map turns the outer map-of-comp into a single map of the composite. List.map_congr_left then reduces the claim to a pointwise identity on each body word $w$: the normalized trace of the evaluation of the conjugate of $w$ equals that of $w$. That identity is exactly trN_conjWord under the table-ok hypothesis, applied via Function.comp_apply.
why it matters
This is the algebraic reason loop traces alone fail to separate the witness: depth one cannot see nesting. Only commutators among loops move under quantification; the individual loop traces are blind to the binder. The module doc records the empirical counterpart: on 3,800 irredundant contents, bare-letter conjugation conflates 860 pairs, while oriented-binder conjugation conflates one (a pair with no separating model).
No downstream theorem currently depends on this declaration in the graph, so it stands as a measured-invariant lemma inside Loom.Grammar rather than a step in the T0–T8 forcing chain. It supports the broader claim that the grammar’s quantifier rule is forced by representation theory of the configuration group, not chosen for convenience. Together with wellFormed_weave and invariant_weave_reduce it pins what free reduction and conjugation preserve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.