depth_one_is_blind2
plain-language theorem explainer
The depth-one (loop-by-loop) component of the Loom invariant agrees on the second certificate pair cfgC and cfgD under the search homomorphism base. Anyone citing the nontriviality of the second separation witness needs this equality: counting and per-loop readings cannot tell the two utterances apart. The proof is a pure kernel decision on finite natural-number lists.
Claim. Under the fixed Loom homomorphism table $T_0$ found by search, the first component of the Loom invariant of configuration $C$ equals that of configuration $D$: $\mathrm{inv}_1(T_0,C)=\mathrm{inv}_1(T_0,D)$. Here $C$ encodes "some door is opened by every key, and every door opens every key" and $D$ encodes "some door opens every key, and every key opens every door".
background
The Loom separation module builds two pairs of short quantified utterances about doors and keys that share the same multiset of ground facts and the same one-bit act cost profile, yet mean different things. The second pair is packaged as concrete configs cfgC and cfgD in CertificateData, evaluated through a fixed table homomorphism base discovered by exhaustive search.
The Core invariant of a table and config is a pair of natural-number lists obtained by evaluating the config and reading off two projections. The first component is the depth-one, loop-by-loop reading: it records what any carrier that inspects loops separately can see. Module documentation states that depth-one and abelianised readings are identical on each separation pair, so every depth-one carrier conflates them; that is what makes later commutator separation nontrivial rather than a length artifact.
Upstream, invariant is just invariantOf (evalConfig T c), and base, cfgC, cfgD are closed concrete data. The Gravity.EchoHorizonObstruction base lemma in the depends list is an unrelated reachability base case sharing a name; the proof here only needs the CertificateData table.
proof idea
One-line decidable proof: both sides reduce to concrete List Nat values once invariant, base, cfgC, and cfgD are unfolded, and Lean closes the equality by decide. No algebraic lemma is invoked; the certificate data are small enough that the kernel compares the two first components directly.
why it matters
This is the depth-one blindness half of the second separation witness. Downstream, depthOne_equal_cfgCD in ClassicalSourceProjection is literally a rename: it packages the equality as DepthOneProjection.Equal on the classical source projections of cfgC and cfgD ("Second discovery pair: depth-one equal"). The sibling separation theorem witnesses2_separated then uses the full gauge-image machinery to show no automorphism, basepoint move, reversal, or loop reordering sends the C weave to the D weave.
In the module's own terms, depth-one blindness is required so the separation is not a restatement of a length or cost difference: counting cannot tell the pair apart, yet the commutator (depth-two) reading and the order-96 gauge quotient check do. Within Recognition Science this sits in the Loom layer that certifies distinct meanings under the recognition-window automorphism action, feeding gravity-side classical source projection comparisons rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.