weave_witnessD

The Loom separation module compares two families of quantified door/key claims that share the same multiset of ground facts and the same one-bit act costs, yet differ in which relation carries universal force. Counting and depth-one readings are blind to the distinction; the module shows a depth-two (commutator) reading and a full gauge sweep separate them.

weave is the certified Lean reconstruction of the Python encoder: given a codebook and a witness term it emits a concrete configuration tree. The module already records the same fact for witnesses A and B. Here the second codebook cb2 and witness D are the inputs, and cfgD is the target configuration used downstream as the D side of the C/D pair.

Nothing in this lemma is semantic. It only pins the syntactic bridge so later theorems can rewrite cfgD as weave cb2 witnessD and inherit grammar lemmas about well-formedness and gauge images.

One-line computational proof: by decide. Both sides are closed ground terms built from the Grammar/Readings/CertificateData stack, so the kernel decision procedure checks definitional equality and closes the goal. No lemmas are invoked.

This is the D-side anchor of the second separation pair in Loom.Separation. Downstream, wellFormed_D rewrites through it and applies wellFormed_weave to conclude wellFormed cfgD = true. The separation theorem witnesses2_separated rewrites both the C and D weaves, then invokes gauge_image_ne_D to show that no automorphism image of C (any of the 48 window automorphisms, basepoint move, optional reversal) equals the D configuration.

Together with the A/B block in the module doc, these identities make the separation about the grammar and the gauge quotient, not about opaque encoder data. The module's strength claim (order-96 gauge times basepoint freedom, exact one-coordinate margin in a 21-coordinate invariant) rests on having cfgD literally equal to the woven witness.