depth_two_separates2
plain-language theorem explainer
Under one fixed homomorphism, the depth-two (commutator) half of the Loom invariant distinguishes two certificate configurations that depth-one readings conflate. Separation and classical-source-projection arguments cite it as the second discovery pair. The proof is a kernel `decide` on finite natural-number lists.
Claim. Let $T_0$ be the fixed homomorphism table found by search, and let $C$ and $D$ be the two certificate configurations (respectively: some door opened by every key and every door opens every key; some door opens every key and every key opens every door). Writing $\mathrm{inv}(T,c)=(v_1,v_2)$ for the Loom invariant, one has $v_2(T_0,C)\neq v_2(T_0,D)$.
background
The Loom separation module compares two quantified door/key utterances that share the same multiset of ground facts and the same one-bit act cost, so length and abelianised readings cannot tell them apart. Configuration $C$ packages "some door is opened by every key, and every door opens every key"; $D$ packages the dual security-hole pattern "some door opens every key, and every key opens every door."
The search-found homomorphism base is a finite table of window pairs. The Loom invariant of a table and config is a pair of natural-number lists: the first coordinate is the depth-one (loop-by-loop / bag) reading; the second is the depth-two commutator reading obtained after evaluating the config through the table.
Module context: depth-one and abelianised carriers are proved blind on the pair, so any genuine separation must live at depth two or in the gauge orbit. This theorem isolates the depth-two coordinate under that single homomorphism.
proof idea
One-line decidability proof. Both sides of the inequality are closed terms of type List Nat (the second projection of invariant base cfgC and invariant base cfgD). Lean’s decide discharges inequality of concrete finite lists by computation; no lemmas are invoked beyond the definitions of the table, the two configs, and the invariant.
why it matters
This is the depth-two half of the second discovery pair in the Loom certificate story. Downstream, depthTwo_separates_cfgCD in ClassicalSourceProjection is a one-line rename: it states the depth-two readings of $C$ and $D$ differ by applying this theorem. The sibling witnesses2_separated uses the same certificate data to push the separation through the full gauge orbit (automorphisms, flips, basepoint moves).
In framework terms it closes the nontriviality claim of the separation module: counting and depth-one bags match, yet the commutator coordinate differs in one of twenty-one slots, the minimal exact margin. It does not itself touch the T0–T8 forcing chain or the RCL; it is Loom infrastructure that later gravity/analysis layers quote when they need a concrete pair that depth-two alone resolves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.