IndisputableMonolith.Loom.Grammar
Defines the Loom grammar: well-formed expressions whose names are codebook indices, never anonymous or claim-local. Builds weave constructions that turn closed recognition walks into typed content over a shared vocabulary. Downstream Readings, Semantics, and Separation import it to compare claims without syntactic accidents. Mostly inductive types and well-formedness lemmas, not deep proof work.
claimThe Loom grammar is the set of well-formed expressions $E$ over a shared codebook $C$, with letters drawn by index and weaves assembling closed recognition words into content. Names are always codebook indices; nothing is anonymous or scoped to a single claim. Well-formed weaves preserve the free-group word structure of closed walks on the eight-state window.
background
Loom is a certificate language for configurations of closed recognition walks. From the Core module: a recognition history is a walk on states; a finished history closes. On the eight-state, three-axis window fixed by the forcing chain, closed walks up to homotopy form a free group of rank $E-V+1=5$. A closed walk is thus a word in five signed generators, and a finished utterance is a finite list of such words sharing one basepoint.
This module supplies the syntactic layer those utterances inhabit. Content the language accepts is named only by indices into a shared codebook, so nothing anonymous and nothing per-claim is ever named. Sibling constructions include expressions, the codebook, letter extraction, weave bodies, the weave operation itself, and well-formedness and invariance facts for weaves (including a quantitative trace identity on weave bodies).
proof idea
This is primarily a definition module: inductive expression types, codebook indexing, and weave constructors that package free-group words into well-formed content. Supporting lemmas check that weaves are well-formed, that reduction preserves the relevant invariant, and that a quantitative identity holds for the trace of a weave body. No deep forcing or analytic argument lives here; the work is structural bookkeeping on top of Core.
why it matters in Recognition Science
Grammar is the shared surface syntax that Readings, Semantics, and Separation all import. Readings needs it so rival content can be stated as ground bags of typed tuples over the same vocabulary rather than left in external scripts. Semantics needs it so "different content" means different claims, not merely different trees: syntactic inequality alone would be an embarrassment if the logic equated the formulas. Separation uses both to certify that two door-and-key style utterances lie in different gauge orbits while asserting the same relations with swapped quantifier roles. Without a codebook-indexed grammar, the separation witness would not be kernel-checkable inside the monolith.
scope and limits
- Does not define semantic equality of claims; that is Semantics.
- Does not construct the separation witness or rival readings.
- Does not prove freeness of the rank-5 walk group; that is assumed from Core and the forcing chain.
- Does not assign physical units, masses, or coupling constants.
- Does not decide gauge orbits; Separation consumes the grammar for that.