rules.kz — the CLAIMS REGISTRY for Koru A claim is something an author asserts about a declaration, written in the vertical annotation block where the reader already is: [ - measured no-alloc-in-kernel This variant compiles the kernel body to a compute shader; the shape is checked by running it, not by inspection. ]proc compute|gpu { ... } The entry is the machine's half — a STAMP and an optional RULE NAME. The prose underneath is the reader's half. They live in one block, so they cannot drift apart. koruc main.k claims # the census, per stamp koruc main.k claims json # the export koruc main.k assumes build # what a declaration's flows rest on koruc main.k assumes build json WHO OWNS WHAT. The compiler carries an opaque entry list and, since the prose change, the prose beside it; it does not know the word "claim". This module defines the vocabulary — which words are stamps, what a key is, what counts as a collision — and it errs loudly AS ITSELF when it evaluates something it cannot (the consumer-relative-rejection rule from frag-annotation-entries-are-expressions). A different module may ship a different vocabulary over the same annotations and get identical support. WHAT THIS DOES NOT DO. It never judges whether a claim is TRUE. `proven` and `measured` are discharged by runners; `inferred` is discharged by whatever external engine the author points at the export. This module only guarantees that every claim has a unique key, so an engine that judges one can say which one it judged. `assumes` walks the CALL GRAPH instead of the annotation list. Literature: Lean's `#print axioms`. Point at a declaration; get the transitive set of declarations its flows can reach, graded by what each callee asserts about itself — and, first-class, which reached declarations assert NOTHING. A `measured` flow that calls five unclaimed things is telling you its measurement did not cover them. The audit never judges truth; it reports reach, and reach is a fact about the program, not a belief about it.