invariant_separates
plain-language theorem explainer
At a fixed basepoint, the Loom invariant of witness configuration A differs from that of B. Cite this when you need the full packaged reading (not just the commutator coordinate) to separate the two door/key utterances. The proof is a one-line projection: equality of invariants implies equality of second factors, which depth-two commutator separation already rules out.
Claim. For the shared basepoint, the Loom invariant of configuration $A$ is unequal to the Loom invariant of configuration $B$: $\mathrm{inv}(\mathrm{base},A)\neq\mathrm{inv}(\mathrm{base},B)$.
background
The Loom separation module builds a kernel-checked witness that two utterances are genuinely different meanings, not two spellings of one. Both utterances cost the same one-bit act budget and share the same per-loop length multiset, so raw counting cannot tell them apart. Depth-one (loop-by-loop) and abelianised readings are identical on the pair; every carrier that stops there conflates them.
What does separate them is the depth-two commutator reading. The packaged invariant at a fixed base is a product-shaped summary whose second factor carries that commutator data (among other coordinates). The module also shows no gauge image of A equals B across the full automorphism, basepoint-move, reversal, and respelling group, so the pair is not related by window symmetry.
Local setting: the weaver reproduces the Python-emitted utterances letter for letter, so all theorems below live in the grammar and semantics, not in opaque external data.
proof idea
Term-mode, two steps. Assume h equating the two invariants. Apply congrArg Prod.snd to project onto the second factor of the product. Feed that equality to depth_two_separates, which already proves the commutator readings of A and B differ. Contradiction, so the invariants are unequal.
No extra algebra: the theorem is exactly the packaging of depth-two separation into the full invariant type.
why it matters
Closes the last packaging step of content B in the module brief: once depth-two separates and the invariant's second coordinate is that reading, the full invariant separates. The module states the strength explicitly: the two invariants differ in one coordinate of twenty-one, the smallest possible margin, exact rather than approximate, because the invariant lands in a finite set.
Together with depth_one_is_blind, abelianised_is_blind, and no_gauge_image_of_A_is_B, this pins that A and B are distinct meanings under the Loom gauge group (order 96 times free basepoint word choice, with all 48 automorphism images checked). No downstream consumers are wired yet in the graph; the result stands as the top-level separation fact for the witness pair.
Framework role: a concrete, kernel-checked instance that recognition structure beyond abelian length data is forced if meanings are to stay distinct, aligning with the broader RS insistence that composition and non-commutative readings carry physical content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.