adjacencyBag_blind
plain-language theorem explainer
The parent-to-child adjacency bags of rival witnesses C and D coincide as multisets (denial folded into atom labels). Anyone arguing that a local labelled-fact reading cannot separate this pair cites this fact. The proof is a pure kernel decision on the two concrete finite lists.
Claim. The multisets of parent-to-child adjacency labels of the parse trees of the two rival witnesses $C$ and $D$ are identical: the adjacency bag of $C$ is a list-permutation of the adjacency bag of $D$ (denial folded into the atom labels).
background
The Loom separation module exhibits pairs of utterances that assert the same two relations under the same quantifier patterns and differ only in which relation receives universal force. Counting one-bit acts, loop-length multisets, and shallow readings therefore agree, so separation is nontrivial.
Rival two is the pair written witnessC / witnessD. The adjacency bag of a witness is the multiset of every parent-to-child label pair in its parse tree, with denial folded into the atom labels. A reading that treats content as a collection of locally labelled facts sees only this bag.
The module already records that depth-one and abelianised readings are blind on the flagship pair; the present fact is the matching blindness statement for the adjacency content of rival two, the pair the flagship failed against.
proof idea
One-line computational proof: decide evaluates the two concrete finite adjacency lists and checks that one is a permutation of the other. No lemmas are invoked; the kernel simply accepts the closed decision.
why it matters
This is the local-fact blindness half of the rival-two separation story. Downstream, witnesses2_separated shows that no gauge image of the woven form of C equals the woven form of D (automorphism, basepoint move, reversal, respelling, loop reorder). Blindness of the adjacency bag is what makes that gauge separation meaningful rather than a restatement of a length or bag difference.
In the module's terms: every carrier that stops at collections of parent-child labelled facts conflates the pair. The separation that remains is carried by deeper structure (commutator / depth-two reading and the order-96 gauge quotient), matching the institute requirement that the two invariants differ in one coordinate of twenty-one on a finite set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.