frameGen
plain-language theorem explainer
The frame generator is the integer label 2 naming the cotree edge that closes the Gray cycle on the eight-state window. That loop is the complete recognition window: an orientation reference with no content of its own. Loom well-formedness and the weaver both require this generator to be present as a singleton loop. The declaration is a one-line integer constant.
Claim. Define the frame generator to be the integer $2$. It labels the cotree edge that closes the Gray cycle, hence the loop that is the full recognition window on the eight-state, three-axis graph.
background
Loom is a certificate language for finished recognition histories: closed walks on the eight-state window forced by the T0–T8 chain (in particular T7’s eight-tick octave). Closed walks up to homotopy form a free group of rank $E-V+1=5$, so a finished utterance is a finite list of words in five signed generators sharing one basepoint.
Content is defined by two refusals. Spelling is not content (free reduction). Basepoint choice is not content (simultaneous conjugation). The module supplies a total well-formedness checker, a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and proofs that the invariant is blind to exactly those two operations.
Among the five generators, one is special: the cotree edge that closes the Gray cycle. Census data put all ninety-six Hamiltonian walks in a single gauge class, so this loop can fix orientation without carrying independent content. The constant here is simply that generator’s integer name.
proof idea
One-line definition: the constant equals $2$. No proof obligations. Downstream code treats the singleton word $[2]$ as the mandatory frame loop when checking or constructing configurations.
why it matters
Every honest Loom utterance must carry the frame loop. The checker wellFormed accepts a configuration only when every word is freely reduced and the list contains the singleton $[2]$. The weaver builds utterances by prepending that singleton and reducing, and wellFormed_reduceConfig_frame proves the checker always accepts the result. The grammar-level theorems weave and invariant_weave_reduce likewise thread the frame through reduction so the invariant is independent of spelling.
In the Recognition framework this is the discrete stand-in for the complete recognition window on the eight-tick octave: an orientation scaffold, not a content carrier. Without a fixed frame generator, well-formedness and the conjugation-blind invariant would have no canonical loop against which to measure the other four generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.