no_gauge_image_of_C_is_D
plain-language theorem explainer
No gauge transform of configuration C can match D under the base invariant: for every window automorphism, flip, basepoint word, and any reordering of the gauged image of cfgC, the invariant differs from that of cfgD. This is the second separation theorem and the strongest claim in the file. Downstream gauge-image and witness-separation theorems cite it. The proof rewrites through permutation and gauge invariance of the invariant, then reads off a precomputed everywhere-separation certificate.
Claim. For every automorphism substitution $\sigma$ among the forty-eight recognition-window automorphisms, every Boolean flip, every basepoint word $g$, and every configuration $c$ that is a list-permutation of the gauge image of $\mathrm{cfg}_C$ under $(\sigma,\mathrm{flip},g)$, one has $\mathrm{inv}_{\mathrm{base}}(c) \neq \mathrm{inv}_{\mathrm{base}}(\mathrm{cfg}_D)$.
background
The Loom separation module compares two pieces of content that share the same multiset of ground facts and the same one-bit act cost profile, so length counting and depth-one readings cannot tell them apart. The second pair (C versus D) is the security-hole dual of the first: same two relations and quantifier patterns, with universal power swapped between open and lock. The module shows they are distinct meanings, not two spellings of one utterance.
A configuration is an assignment of binary sides to independent distinction channels. The gauge action combines a substitution from the forty-eight automorphisms of the recognition window Q3 (the only trusted external table), an optional simultaneous reversal, a free basepoint word, and arbitrary reordering of loops. The base table is the homomorphism found by exhaustive search; the invariant is the reading of a configuration through that table.
Upstream, autSubst lists the action of those forty-eight automorphisms on the five free generators as words. Everything the separation needs is then computed inside Lean from that list. The certificate separates_everywhere2 asserts that under every such automorphism the base invariants of the two fixed configurations already differ.
proof idea
Term-mode, three steps. First rewrite the goal with permutation-invariance of the base invariant along the hypothesis that $c$ is a permutation of the gauge image, then with gauge-invariance of the invariant, reducing to a comparison of invariants of cfgC and cfgD after the automorphism alone. Second, extract from separates_everywhere2 (via List.all_eq_true.mp) the Boolean inequality for the given $\sigma$ in autSubst. Third, simpa converts that Boolean inequality into propositional inequality of the two invariants.
why it matters
Doc-comment calls this the second separation theorem and the strongest statement in the file: two contents that every local-fact reading identifies, and that no gauge transform of the utterance identifies. It is the C/D twin of the A/B no-gauge-image theorem named in the module header.
Immediate parents: gauge_image_ne_D turns invariant inequality into configuration inequality by contradiction; witnesses2_separated specialises that to the woven witness pair after the weaver lemmas identify the Python-emitted utterances with Lean grammar terms. Together they close the claim that the gauge group quotiented over (order 96 times free basepoint choice, all 48 automorphisms checked) cannot identify the two meanings. The invariants differ in one coordinate of twenty-one, the smallest exact margin on a finite set. In the broader RS loom story this is semantic separation under the recognition-window automorphism action, not a length or cost distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.