IndisputableMonolith.Loom.Core
Core types for the Loom: words in five signed cotree generators, treated as closed walks up to homotopy, plus reduction, inversion, and conjugation. Certificate data and the grammar import this layer. Definitions and elementary list lemmas on free reduction; no deep theorems here.
claimA Loom word is a finite list of letters from five signed cotree generators. A configuration is a collection of such words (closed walks up to free reduction). The module supplies free reduction $w \mapsto \mathrm{reduce}(w)$, the reducedness predicate, inversion $w^{-1}$, and conjugation, with the usual list identities.
background
The Loom models closed walks on a cotree skeleton by words in a free group of rank five (signed generators). Homotopy of walks is free cancellation: adjacent inverse pairs drop. That is the content of reduceWord and isReduced.
Config packages one or more such reduced words. Downstream, the measured certificate records a homomorphism from this free group into $\mathrm{SL}_2(\mathbb{Z}/3\mathbb{Z})$ together with automorphism tables; the grammar turns abstract content into configurations of closed walks via five production rules (ordered products, conjugations, and so on).
Imports are ordinary Mathlib list, permutation, and modular-arithmetic support. No Recognition forcing chain (T0–T8) is invoked at this layer; the module is pure combinatorial group data for the Loom stack.
proof idea
This is a definition module. It introduces Word, Config, free reduction (consRed, reduceWord), reducedness, inversion, and conjugation, then proves short list lemmas (reduceWord_cons, invWord_cons, isReduced_cons_cons, isReduced_tail, isReduced_consRed) by induction and rewriting. No global existence or uniqueness argument lives here.
why it matters in Recognition Science
Every Loom certificate and every grammatical utterance sits on these types. CertificateData imports the module to host the search-found base homomorphism and the forty-eight $Q_3$ automorphism tables as Lean values. Grammar imports it so that weave can emit configurations of closed walks from inductive content (Expr), with production rules forced by matching algebraic operations on configurations. Without a shared reduced-word layer, certificate checking and grammar soundness would not share a carrier.
scope and limits
- Does not define the base homomorphism into SL_2(Z/3Z); that lives in CertificateData.
- Does not prove that reduction is confluent beyond the listed cons/tail lemmas.
- Does not encode the five grammar production rules or weave.
- Does not connect words to Recognition forcing (T5–T8), mass, or alpha.
- Does not assert freeness or residual finiteness of the ambient group.
used by (2)
declarations in this module (106)
-
abbrev
Word -
abbrev
Config -
def
consRed -
def
reduceWord -
def
isReduced -
def
invWord -
def
conjWord -
theorem
reduceWord_cons -
theorem
invWord_cons -
theorem
isReduced_cons_cons -
theorem
isReduced_tail -
theorem
isReduced_consRed -
theorem
isReduced_reduceWord -
def
frameGen -
def
wellFormed -
structure
Mat -
theorem
eq_of -
def
one -
def
mul -
def
det -
def
adj -
def
tr -
def
trN -
theorem
mul_assoc' -
theorem
one_mul' -
theorem
mul_one' -
theorem
mul_def -
theorem
one_def -
theorem
det_mul -
theorem
det_one -
theorem
adj_mul -
theorem
adj_adj -
theorem
tr_adj -
theorem
tr_mul_comm -
theorem
mul_adj_of_det_one -
theorem
adj_mul_of_det_one -
def
cj -
theorem
adj_cj -
theorem
adj_one -
theorem
cj_mul -
theorem
tr_cj -
def
comm -
theorem
comm_cj -
theorem
det_adj -
theorem
tr_comm_symm -
theorem
trN_comm_symm -
theorem
trN_comm_adj -
abbrev
Table -
def
entryOk -
def
matAt -
theorem
entryOk_one -
theorem
entryOk_matAt -
def
letterMat -
theorem
det_letterMat -
theorem
letterMat_mul_neg -
def
evalWord -
def
evalConfig -
theorem
evalWord_cons -
theorem
evalWord_singleton -
theorem
evalWord_append -
theorem
det_evalWord -
theorem
letterMat_neg -
theorem
evalWord_invWord -
theorem
evalWord_consRed -
theorem
evalWord_reduceWord -
abbrev
Subst -
def
getWord -
def
substLetter -
def
substWord -
theorem
substWord_cons -
def
substConfig -
def
tableOfSubst -
theorem
ok_tableOfSubst -
theorem
matAt_tableOfSubst -
theorem
evalWord_substLetter -
theorem
evalWord_substWord -
def
insertNat -
def
sortNat -
def
pairTraces -
def
invariantOf