autSubst_length
plain-language theorem explainer
The concrete substitution table for window automorphisms has exactly forty-eight entries. Separation arguments that quantify over every gauge image of utterance A cite this to know the enumeration is complete rather than a sample. The proof is a pure kernel decision on the length of a closed list.
Claim. The finite list of automorphism substitutions of the recognition window has length $48$.
background
In the Loom separation module, two woven utterances A and B share the same depth-one and abelianised readings, so length and one-bit cost cannot tell them apart. Separation is nontrivial only if no gauge move turns A into B.
The gauge action includes the automorphisms of the recognition window. The module enumerates those automorphisms as an explicit list of substitution words (autSubst). Completeness of later universal claims (no image of A equals B under any automorphism, basepoint move, reversal, or loop reordering) requires that this list really has forty-eight entries, matching the known order of the window automorphism group.
The surrounding check also tracks a factor of two from optional simultaneous reversal, giving the order-96 gauge skeleton quoted in the module header, times free basepoint choice.
proof idea
One-line computational proof: decide asks the kernel to evaluate List.length on the closed concrete value of the substitution table and confirm the numeral equals 48. No lemmas are invoked; the equality is a ground fact about a finite list literal.
why it matters
Module documentation states the separation strength explicitly: the gauge group quotiented over has order 96 times free basepoint choice, and "the check covers all 48 automorphism images exactly (autSubst_length)". Without this length fact, no_gauge_image_of_A_is_B would only rule out a proper subset of window automorphisms.
That completeness is what upgrades the depth-two commutator distinction from a reading difference into a meaning difference: A and B are not two spellings of one content under the recognition-window gauge. The result sits in the Loom certificate layer that the institute uses to argue the separation is exact (one coordinate of twenty-one) rather than a tolerance claim.
No downstream Lean users are recorded yet; the citation value is documentary and for any proof that unfolds the full automorphism sweep.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.