depth_one_is_blind
plain-language theorem explainer
The depth-one (loop-by-loop) invariant of the two separation configurations agrees exactly. Anyone arguing that bag-of-loops or multiset readings already separate the pair must confront this equality. The proof is a pure decidability check on finite data: both sides evaluate to the same first component.
Claim. For the fixed basepoint and the two separation configurations $A$ and $B$, the first component of the depth-one invariant agrees: $\mathrm{inv}_1(\mathrm{base},A)=\mathrm{inv}_1(\mathrm{base},B)$. Equivalently, any reading that is a multiset of per-loop quantities conflates $A$ with $B$.
background
The Loom separation module exhibits two utterances that assert dual quantifier patterns over the same two relations ("every door has some key that opens it, and one master key locks every door" versus the security-hole dual). They are engineered so that a multiset of ground facts and the same per-loop length multiset cannot tell them apart.
The depth-one invariant is the loop-by-loop reading: each loop contributes a quantity, and the carrier only keeps the multiset (bag) of those quantities. The module doc states the point of this lemma: the loop-by-loop reading and the abelianised reading are identical on the pair, so every carrier that stops at depth one conflates them. That is what makes the later depth-two separation nontrivial rather than a restatement of a length difference.
Configurations cfgA and cfgB are the concrete pair produced by the weaver from the grammar; the invariant is evaluated at a fixed basepoint. Upstream scaffolding supplies the finite certificate data and the recognition-window automorphism action against which gauge-triviality is later checked.
proof idea
One-line decidability proof. Both sides of the equality are closed finite terms (the first projection of the depth-one invariant on the two fixed configurations). Lean discharges the goal with decide, so no algebraic rewriting or external lemma application is required beyond the decidable equality instance on the invariant's first component.
why it matters
This is the blindness half of the separation witness. Downstream, ClassicalSourceProjection packages it as G0 (depth-one sources of A and B agree) and as Decoy D2: any reading that factors as the depth-one bag is blind on the discovery pair. The composite certificate classicalEqual_recognitionUnequal_cfgAB is literally the triple of this lemma, abelianised blindness, and depth-two separation.
OrderSensitiveHistoryResponse4D reuses it the same way: finite certificates and the order-sensitive gate open with depth-one equality and close with a history-response inequality (and a metric-edge non-membership). Inside the module, witnesses2_separated depends on it so the pair is known to be nontrivial before gauge-orbit checks.
In Recognition terms, the result pins that classical bag-of-loops sources cannot see the distinction the recognition reading later isolates. The module strength claim is that the two invariants differ in one coordinate of twenty-one after quotienting by a gauge group of order 96 times basepoint choice; blindness at depth one is the necessary first step of that argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.