depth_two_separates
plain-language theorem explainer
The depth-two (commutator) coordinate of the loom invariant distinguishes the discovery pair: under the fixed homomorphism table, configuration A and configuration B yield unequal second components. Anyone citing the classical-equal / recognition-unequal certificate or the gauge-orbit separation will use this. The proof is a pure kernel decision on finite natural-number lists.
Claim. Let $I(T,c)=(I_1,I_2)$ be the loom invariant of configuration $c$ under table $T$. With $T$ the search-found homomorphism and $c_A$, $c_B$ the two door-key configurations ("every door has a key that opens it, one master key locks all" versus "every door has a key that locks it, one master key opens all"), one has $I_2(T,c_A)\neq I_2(T,c_B)$.
background
The Loom separation module exhibits two short utterances that agree on every depth-one and abelianised reading yet disagree once commutators are read. Configuration A asserts: every door has some key that opens it, and one master key locks every door. Configuration B swaps the roles of open and lock under the same quantifier pattern. Both are encoded as finite loop lists over a four-letter alphabet; a fixed table (the homomorphism found by exhaustive search) evaluates each configuration to a word whose multiset statistics feed the invariant.
The invariant of a table and configuration is a pair of natural-number lists. The first component aggregates depth-one / abelian data; the second records the depth-two (commutator) reading. Module context stresses that counting alone cannot separate A from B: same one-bit act cost, same per-loop length multiset. Separation must therefore live in non-abelian structure.
Upstream, base is that concrete table of five letter-to-letter pairs; cfgA and cfgB are the two concrete configs. The invariant is obtained by evaluating the config under the table and passing the result to invariantOf.
proof idea
One-line decidability proof. Both sides of the inequality are closed terms of type List Nat built from concrete finite data (the fixed table and the two configs). Lean’s decide tactic discharges inequality of those computed lists by kernel evaluation; no lemmas are invoked beyond the decidable instance on lists of naturals.
why it matters
This is the positive half of the separation witness: depth one and the abelianisation are blind on the pair, while depth two is not. Downstream, depthTwo_separates_cfgAB and discovery_pair_is_certificate_cfgAB re-export the fact as a recognition-depth certificate; classicalEqual_recognitionUnequal_cfgAB packages it with the two blindness theorems into the composite “classical sources equal, recognition sources unequal.” Locally, invariant_separates lifts the second-component inequality to full invariant inequality, which then feeds the gauge-orbit argument that no automorphism image of A is B.
In framework terms the result is a concrete, machine-checked instance of order-sensitive history response: two sources identical under every abelian or single-pass projection become distinct once nested commutators are admitted. The margin is minimal and exact (one coordinate of twenty-one, values in a finite set), matching the module’s stated strength criterion. It does not itself invoke the T0–T8 forcing chain, but it supplies the loom-side certificate used by the classical-source projection analysis in Gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.