Config
plain-language theorem explainer
A configuration (utterance) is a finite list of closed recognition walks that share one basepoint. Each walk is a word in the five signed cotree generators of the free group of rank five on the eight-state window. Anyone working on Loom certificates, free reduction, or conjugation-blind invariants cites this type. It is a one-line type synonym, not a proved claim.
Claim. A configuration is a finite list of words, where each word is a list of integers coding a closed walk (up to homotopy) in the five signed cotree generators. The list is an utterance: several closed loops sharing a single basepoint.
background
The Loom module is a certificate language for finished configurations of closed recognition walks. On the eight-state, three-axis window fixed by the forcing chain (T7 eight-tick octave, T8 $D=3$), closed walks up to homotopy form a free group of rank $E-V+1=5$. A single closed walk is therefore a word in five signed generators; an utterance is a finite list of such words on one shared basepoint.
A sibling abbreviation defines a word as a list of integers (the signed generators). Spelling is not content, so later material reads words up to free reduction. Basepoint choice is not content either: simultaneous conjugation of every loop by the same word is quotiented out, now partly justified by closure (rotate_is_conjugation) and vertex homogeneity rather than pure phenomenology.
The module supplies a total well-formedness checker, a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ (including pairwise commutator traces), and theorems that the invariant is blind exactly to free reduction and simultaneous conjugation.
proof idea
One-line type abbreviation: Config is defined to be List Word, and Word is itself List Int. No proof obligations; pure naming of the utterance type used by the checker and the invariant.
why it matters
This is the carrier type for every Loom certificate. Downstream, CostFromDistinction builds an abstract configuration space (empty config, join, consistency, independence) and proves additivity of cost, calibration, and the recognition-work constraint; several of those theorems and structures take Config as their ambient type. Inside Loom itself the type feeds free reduction, the reduced-word checker, conjugation, and the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ trace invariant that separates automorphism images the abelianised reading cannot.
Framework landmarks: the free group of rank five sits on the eight-tick window (T7) in three spatial dimensions (T8). The invariant’s use of class functions and depth-two commutator traces is exactly what makes conjugation blindness a ring identity rather than a canonicalisation step. The definition itself closes no open question; it is the shared vocabulary on which the checker and the blindness theorems rest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.