evalConfig
plain-language theorem explainer
Pointwise evaluation of an utterance: each closed walk is sent to its image matrix under a fixed generator table. Anyone building or citing the Loom invariant uses this as the first step from combinatorial words to SL(2,Z/3Z) data. The body is a one-line list map of the single-word evaluator.
Claim. Given a generator table $T$ (pairs of matrices for each signed generator) and a configuration $c$ (a finite list of words in those generators), $\mathrm{evalConfig}(T,c)$ is the list of matrices obtained by evaluating each word of $c$ under $T$.
background
In the Loom module, a finished recognition history is an utterance: a finite list of closed walks on the eight-state, three-axis window, all sharing one basepoint. Combinatorially this is a Config, i.e. a list of words in five signed generators (the free group of rank $E-V+1=5$).
A Table assigns to each generator a pair of matrices in the componentwise $2\times 2$ ring over $\mathbb{Z}/3\mathbb{Z}$ (the structure Mat), one for the generator and one for its inverse. The single-word map evalWord multiplies those letter matrices from the head of the word, with the empty word mapping to the identity.
The module's job is a total well-formedness checker and a computable invariant of configurations that is blind to free reduction and simultaneous conjugation. Evaluation of whole configurations is the bridge from the word list to the matrix list that the invariant then reads (traces and pairwise commutator traces).
proof idea
Pure definition: apply List.map of evalWord T to the configuration. No lemmas, no tactics; the empty body is the list comprehension itself. Downstream proofs rewrite with evalConfig and then use List.map_map or congruence on the word-level evaluator.
why it matters
This is the evaluation step that every Loom soundness theorem factors through. The invariant is defined as invariantOf (evalConfig T c), so conjugation blindness (invariant_conjWord), inversion blindness (invariant_map_invWord), free-reduction blindness (invariant_reduceConfig), and automorphism/relabelling soundness (invariant_substConfig) all begin by pushing evalConfig through the corresponding list map and reducing to a matrix identity (class function of trace, or homomorphism properties of the table).
In the Recognition framework this sits inside the certificate layer for closed walks on the eight-tick window forced by T7, not inside the forcing chain itself. It carries no model and no search: it only turns a finished combinatorial object into the SL(2,Z/3Z) data the invariant needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.