invariant_weave_reduce
plain-language theorem explainer
The loop invariant of a fully woven utterance equals that of the bare frame loop prepended to the unreduced weave body. Anyone reading content off configuration invariants can ignore free reduction and loop spelling. The proof is a one-line application of the configuration-level reduction lemma for invariants under a valid table.
Claim. Let $T$ be a valid table, $c$ a codebook, and $e$ an accepted expression. Then the invariant of $T$ on the woven configuration of $e$ equals the invariant of $T$ on the configuration formed by the frame generator followed by the weave body of $e$: spelling and free reduction of loops do not change the invariant.
background
The Loom grammar turns accepted content into configurations of closed walks. Content is the inductive type with atoms (a relation on role fillers, possibly denied), unordered conjunction, and quantifiers over shared names. A codebook is a list of integers attaching each shared name to a signed generator; sender and receiver must share it, and it is not pure gauge.
Weaving is the total map from content to configurations forced by the algebra of the content operators: ordered product for relations, inversion for denial, multiset union for conjunction, and binder loops with conjugated bodies for quantifiers. Every utterance also carries the frame loop (the walk that closes the recognition window), and every loop is freely reduced because spelling is not content.
The weave body is the configuration produced from the expression before the frame is attached and full free reduction is applied to the whole utterance. The invariant of a table on a configuration is the quantity that is supposed to be insensitive to how loops are spelled once the table is valid.
proof idea
One-line term proof. It applies the upstream configuration lemma that, for any valid table, the invariant is unchanged by free reduction of loop spelling, instantiated at the woven configuration (the hole filled by the weave of the codebook and expression). No case analysis on the expression tree is needed here; reduction of the full weave to frame-plus-body is discharged by that single lemma.
why it matters
In the Loom stack this seals the module claim that spelling is not content: once a table is valid, the invariant of a woven utterance may be computed on the simpler frame-plus-body configuration. That matches the grammar design in which free reduction is mandatory and the frame loop is obligatory so denial has something to orient against.
No downstream theorems currently cite it (used-by is empty), so it is a local closure fact inside the grammar rather than a step in the T0–T8 forcing chain. It supports the measured separation story in the module: conjugating by oriented binder loops (not bare letters) is what keeps quantifier type visible; this lemma ensures that after that choice, residual free reduction still cannot move the invariant. It does not itself address the residual conflation pair or the fifteen-orbit lower bound on codebooks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.