groundBag_blind
plain-language theorem explainer
The ground-fact multisets of the second rival pair (C and D) coincide: their extracted ground facts and binder occurrences are equal up to permutation. Anyone arguing that a locally labelled, binder-blind reading cannot separate the pair cites this. The proof is a pure kernel decision on finite lists.
Claim. The list of ground facts (including binder occurrences) extracted from witness $C$ is a permutation of the corresponding list for witness $D$; equivalently, the two multisets of ground facts are equal.
background
The Loom separation module exhibits two rival contents that assert the same two relations under the same quantifier patterns and differ only in which relation receives universal force. One is a sound access policy (every door has some opening key; one master key locks all); the other is a security hole (roles of open and lock swapped at the universal end). Counting cost, loop-length multisets, and several shallow readings are engineered to match.
A ground-fact reading flattens each parse tree to the multiset of atomic labelled facts and binder occurrences, with denial folded into atom labels. Equality of those multisets means no reading that treats content as an unordered bag of local facts can tell the rivals apart. The theorem is stated for the second witness pair $(C,D)$ used by the flagship separation, parallel to the first pair $(A,B)$ treated elsewhere in the module.
The surrounding development already shows that the Lean weaver reproduces the encoder output letter for letter, so the comparison is about the grammar and the reading, not opaque data.
proof idea
One-line computational proof: decide asks the kernel to check List.Perm on the two concrete finite lists returned by groundBag. No lemmas are invoked; the permutation certificate is produced and verified entirely by the decision procedure on the closed terms for witnesses $C$ and $D$.
why it matters
This is the ground-fact half of the blindness package for the second rival pair. Together with the depth-one and abelianised blindness results named in the module doc, it shows that every carrier stopping at local labelled facts conflates $C$ and $D$, so separation is nontrivial rather than a length or cost artifact.
Downstream, witnesses2_separated uses the weave equalities and the gauge-image non-equality to prove that no automorphism, basepoint move, reversal, or loop reordering sends the weave of $C$ to the weave of $D$. Ground-fact blindness supplies the matching lower bound: the pair is invisible to bag-of-facts readings yet remains distinct as meanings under the full gauge group of the recognition window (order $96$ times basepoint choice, with all $48$ automorphisms checked).
In Recognition terms this is a concrete Loom witness that structure beyond multiset content is forced if one wants to keep security-sensitive quantifier polarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.