IndisputableMonolith.Loom.Readings
Defines the local reading layer on Loom configurations: node labels, ground bags, and adjacency data extracted from a woven parse. Anyone proving separation or kernel checks on two contents cites these maps. The module is definitional scaffolding over Grammar; it packages what a local observer can name without re-running the full weave.
claimOn a woven configuration, a reading assigns each node a label (what a local parse can name), a ground multiset of base tokens, and an adjacency bag of incident edges. The maps $\mathrm{labelOf}$, $\mathrm{groundBag}$, $\mathrm{adjacencyEdges}$, and $\mathrm{adjacencyBag}$ extract these from the Grammar weave of an expression.
background
Upstream, Loom.Grammar fixes the content language: an inductive type Expr and a total map weave sending content to a configuration of closed walks. Five production rules are forced by matching algebraic properties of content operators to operations on configurations (ordered products of letters for relations on roles, and so on).
This module sits one layer above that weave. A label is what a local reading of the parse tree is allowed to name at a node. Ground data records the base tokens visible there; adjacency data records which edges touch the node. Together they turn a global closed-walk configuration into a bag of local observations without inventing new content operators.
The setting is purely combinatorial: readings are derived views, not new physics constants or forcing-chain steps. They prepare equality and inequality checks used later when two contents must be told apart by what locals can see.
proof idea
This is a definition module, no proofs. It introduces the label and ground types and the extraction maps (labelOf, groundBag, adjacency edge and bag constructors) as pure data over Grammar configurations. Downstream modules import these names and reason about equality of bags or existence of distinguishing labels.
why it matters in Recognition Science
Separation imports this module as its observational substrate. The Separation doc frames two contents that assert the same two relations on doors and keys yet differ in security meaning: one has a master key that locks every door after every door has some opening key; the other flips open/lock and is a hole. Kernel checks that distinguish those contents need a precise notion of what a local reading can name and which ground or adjacency bags it sees.
Without Readings, Separation would re-derive node-local projections inside the witness argument. Packaging labels, ground bags, and adjacency here keeps the separation witness focused on relational asymmetry rather than parse-tree bookkeeping. The module does not itself close a T0–T8 forcing step; it is Loom infrastructure that makes content-level separation checkable.
scope and limits
- Does not define Expr, weave, or the five Grammar production rules.
- Does not prove separation of any two contents; that lives downstream.
- Does not assign physical units, masses, or RS constants to labels.
- Does not claim completeness of local readings for global configuration equality.
- Does not introduce kernel decision procedures or security theorems.