Coined terms used across the documents, one line each, with the pointer that defines them. Language constructs the Reference defines (shape, refinement, rule, guard, fold, capture, tick, act) aren't repeated here — this covers the working vocabulary invented along the way. Rule of use: a doc's first use of one of these terms should read sensibly to someone who has only this file.

• Reference / Reference §N — the Velle Language Reference: the numbered pages Reference-01-Principles through Reference-22-Open-unresolved of this wiki, one per section, cited everywhere (documents, spec comments, validator diagnostics) as "Reference §N" by section number. It was the repository's README until 2026-10-15.
• act — a shape declared act, whose instances are committed from outside the system; also such an instance, a request or message crossing the trust boundary (Reference §4, §22).
• transient act — an act that exists only within its own commit's transaction (transient act): an input to the state, not a member of it (Reference §4; decided 2026-08-10 on the principle that an incoming mutation is an input to the state, not automatically a member of it).
• prohibition — what a never or a requires declares: a configuration that is impossible, stated as the forbidden configuration (never) or as what every record satisfies (requires, whose prohibition is its complement; inside a requirement, membership may be spelled to be). The umbrella noun (adopted 2026-10-10 in place of "invariant", which named only the proven kind); a prohibition is a refusal, a constraint, or a guarantee, by who it binds (Reference §21).
• refusal — a prohibition that binds the caller: a prohibition over a transient act, checked once — at the door when the request's handling leaves what it reads alone, at the settled transaction otherwise; the record the request leaves carries nothing (Reference §21).
• door / door-checked — the moment right after an act's closure is inserted and before any rule runs, where the prohibitions no rule can move (reading nothing any rule writes, creates, or deletes) are evaluated once and then skipped at the transaction end; a door-checked prohibition is one of those (Reference §21; evaluation.md "An exposed call"; ruled 2026-10-14).
• constraint — a prohibition that binds the books: a prohibition over a persistent shape, holding at the end of every transaction for as long as the record exists; any act or tick that would leave the books otherwise is rejected; it may not read the clock, since the books could age into it with no act to refuse (Reference §21; checks.md V30).
• guarantee — a prohibition that binds the spec's own rules: only rules can produce the state, nobody is refused, and the compiler proves the rules cannot reach it; a runtime violation is a bug (Reference §21; evaluation.md [S5]).
• door rule — the owner's name for a refusal: "turn this request away", about the act being recorded at the moment it is submitted, and silent about it afterwards (Reference §21).
• actor — the person, job, or system that committed an act: bound by the act's by Shape [as name] clause under the name actor (or the as name), a fact of the commit the binding hands in and the committer never claims, stored on a durable act like its timestamp; the security field's principal, under the word the spec uses (Reference §22, "The actor"; OQ33, settled 2026-10-15).
• principal — the security field's word (JAAS, Kerberos, cloud IAM) for the identity an action is performed on behalf of; in velle the actor, above. Used in prose about the concept, never as a spelling in a spec.
• role gate — a prohibition on who may commit an act, spelled in the act's header (by Administrator, a refinement after by) or as a requirement over the actor in the body (requires actor to be Administrator); one desugaring, the same refusal (Reference §22, "The actor"; §21).
• viewer — the person a read is for: the record the binding hands the generated read(viewer), bound in a visibility clause's predicate under actor or the clause's as name; the same kind of thing as an actor, seen from the read side (Reference §8, "Who may see a record"; §22, "The actor").
• visibility clause — visible to <Shape> [as name] [where ...] or visible to anyone: on a shape body, which viewers its records are returned to; after a field, which viewers that field is returned to within its record; at the top level, the spec-wide default a shape's own clauses replace. Applied by the read surface only, never inside evaluation (Reference §8; checks V32).
• the engineer's view — a read with no viewer: the generated system's read, unfiltered, the engineer reading the store they own. Not an identity; what a job that reads uses (Reference §22, "The actor").
• seed / seeded record — a record that exists without any act having committed it: a migration or fixture row, the engineer's own write through the store, or VelleSystem.seed in memory — no door, no rule, no prohibition; outside the trust boundary by construction. How the first administrator arrives where hiring is gated on one (Reference §22, "The actor"; evaluation.md, "An exposed call").
• books rule — the owner's name for a constraint: "the records never look like this", about valid committed state at every moment, and violable by later acts, ticks, and deletions (Reference §21).
• drift / drift-exposed partition — a partition of a persistent act over mutable state is re-evaluated at every later change to that state, so a long-handled act "drifts" between sides: a spurious refusal per flip, a stale re-fired write per flip back. Worked exhibit: examples/partition-drift/; flagged by advisory A4.
• handled-once act partition — the fix idiom for drift under persistence: the partition is scoped to unhandled acts, each side anchored by its own rule's outcome evidence. Live in payments.velle.
• anchor / anchored spelling — the outcome-evidence conjunct (... where not exists EditApplication for this) that pins an already-handled act out of its partition.
• correlation key — a client-supplied business key (the idempotency-key pattern) a transient act carries and its outcomes copy, so callers can match responses to requests and duplicate submissions can be recognized (Reference §4 "Transient acts"): a documented idiom, deliberately not language machinery — the key's uniqueness is the client's to own, the dedup guard the author's to write.
• C0 pinning — a transient act's partitions are evaluated against the state at its arrival commit and never re-evaluated by its own consequences (evaluation.md, "Transient acts").
• closure / exposure closure / input closure — what one commit carries: the act plus the inline parts its with declaration says arrive with it, statically shaped, with the single instance as the degenerate case (Reference §4; §6 "Inline part creation").
• HOLDS / TAX / GAP — stress-pass verdicts: the design handles the case · handles it at a cost (a restructured spelling, a coarse check to work around) · needs a new obligation or fails (a check, the runtime, or the generator is wrong or missing).
• surface — the set of calls available to code outside the system: the typed surface is the generated Kotlin API (the act input values and the commit overloads over them, accessors, model objects, the query API), the query surface or read surface is the part of it that gets data out, the store surface is the typed interface a store implements. Plain synonym: API. Used in Reference §22; the reads work says "read API".

• errors-are-refinements — valid/invalid are refinement memberships, not control flow; consequence rules hang off the valid subset (Reference §8).
• rejection-as-data — a refusal lands as a fact the caller reads back; nothing unwinds (patterns.md, "Validation rejection is data").
• conditioned acceptance — "don't accept unless X" is the definition of accepted, not a transaction statement (patterns.md).
• intent-before-effect — an external effect hangs off a durable intent fact; executing the effect is the engineer's loop observing the intent (Reference §11).
• materialize, then decide — the transient-act idiom for async work: the handler copies the act into a durable intent within its transaction; decisions and effects hang off the intent (patterns.md, "Materialize, then decide").
• ledger / episode — history patterns: an append-only record read via latest · a bounded occurrence fact counted later (Reference §12, §20).
• rung / rung recognition — a spelling's position on the pattern spectrum (e.g. incremental vs. recompute — one description, two spellings); diagnostics point at the twin rung (Reference §19–§20).
• predecessor recurrence — the derived-history spelling of an order-dependent fold: a derived previous (latest ... by the ordering datum) plus self-reference one hop through it, so each record derives its running value from its predecessor's and the current total is a selector read; the served spelling for tick-cadence order-dependent folds (Reference §19).
• arrival-order semantics — what a commit-cadence stored fold describes: commits are serialized, so fold order is commit order — the order records arrived — which diverges from the business's ordering datum when a record arrives late (Reference §19).

• ownership (of a relationship) — what one/many declare: the declaring shape's property is the stored side — rules assign it, committers supply it — and the inverse is inferred, derived, unassignable; direction is not encoded because inference makes both sides traverse (Reference §6).
• graduation point — the moment an edge carries data (when, who, a grade, a quantity), it stops being a bare many edge and becomes a business fact with its own shape; join shapes are never ceremony, only facts (Reference §6).
• fan-out assignment — a collection-path assignment (this.invoices.customer = ...): one write per member of the collection, one many hop only, the mutated field named in the statement (Reference §6; checks V20, V1's coarse extension).

• fail-closed — when the prover can't decide, the spec is rejected, never silently accepted; calibration then grows the provable set.
• calibration — the post-v0 work of running realistic specs to learn how coarse the fail-closed checks can stay before they reject too much, and where the certificate whitelist (V14, V16) grows.
• one-writer — every stored field has provably one writing rule per coincidence class (Reference §12; check V1).
• disarm proof — showing a rule's effects falsify its own trigger condition, breaking a re-fire cycle (check V2).
• sibling firings / siblings — two rule firings triggered by the same commit, where neither firing caused the other, so the runtime may run them in either order (evaluation.md, "Processing one commit" step 6). "Sibling" in these docs always means sibling rule firings, never a data relationship.
• confluence — sibling firings commute: every firing order yields the same outcome (check V15).
• quiescence — a transaction terminates: eventually no rule's condition is newly matched (check V16).
• discharge — satisfy a derived proof obligation; standard proof-theory usage, throughout Reference §18–§21. "The disarm proof discharges" = the compiler completes the required proof (the body provably falsifies its trigger); a "dischargeable state" is a trigger state the rule's own effects provably exit; an "undischarged obligation" is a compile error.
• spent prohibition — an established never used as a proof input by other analyses ("the author states the prohibition; the prover uses it," Reference §21); only a fully-discharged prohibition is spendable.
• certificate — the stated reason a static cycle provably ends, drawn from a decidable whitelist: strict descent on a creation-fixed datum plus a base case, or acyclicity supplied by a never prohibition. Consumed by V14 for definition-graph cycles and V16 for cascade quiescence; one shared vocabulary, grown by calibration.
• pinned (firing set) — a commit's entrant/leaver sets are computed from one pre/post diff before any sibling firing runs, so a sibling's write cannot change who fires at that commit; what it can change is read by bodies, which see the evolving state (evaluation.md step 5/6; the distinction V15's read-write leg is built on).
• polarity (of a consult) — which way creating an instance can move a predicate: toward true (+), toward false (−), or both/unknown (0); signs come from exists under negation, refinement absorption, and count comparisons. Same-direction sibling effects on one predicate cannot race (checks.md V15; Validator.kt, canCoFire).
• fresh-instance argument — a freshly created instance cannot satisfy a positive exists ... for this over a shape the same commit does not create, because nothing can reference it yet; so its creation provably cannot move consults gated behind such a refinement, and a fresh instance never leaves anything (checks.md V15; the V12/V18 family's reasoning aimed at consult analysis).
• check IDs — V1–V18 are validator errors, A-series are advisories (A4 = drift-exposed partition), F-series are type/form checks; all cataloged in checks.md.

• projection principle — every generated artifact (runtime, tests, diagrams) is a deterministic projection of the one authored spec: same spec in, same artifact out, regenerated at every compile — nothing is hand-maintained, so nothing can drift or disagree with a sibling (diagrams.md).
• may-fire / may-cause — the artifacts' over-approximation stance, matching the runtime's relevance gating: omitting a possible consequence lies, showing an unreachable one merely hedges. Proofs sharpen the picture (one-way arrows, pruned edges, exclusive diamonds); missing proofs weaken it honestly ("may flip"), never guess.
• membership axis — one independently varying dimension of refinement membership on a shape; state-flow diagrams render one small machine per axis, grouping refinements onto a shared axis only when their predicates are provably disjoint (diagrams.md).
• rule graph — the whole system's cause map on one page: acts and rules as nodes, "this commit's writes can change that rule's condition" as edges, guards on the edges, decision diamonds only where exclusivity is proven (diagrams.md).

• envelope — one act's transaction: the act's commit plus every consequence commit, all-or-nothing.
• universal transaction — the five-clause contract (U1 snapshot, U2 atomicity, U3 serialization, U4 permanence, U5 no side doors) the engineer's storage must honor per envelope; normative in evaluation.md; U3's queue-key derivation is the U3 clause and checks.md A5.
• serialization domain — the compiler-computed key set an envelope revolves around, expressed as paths from the act ({this.account} for a deposit): two envelopes conflict iff their domains intersect, so the domain is exactly what an implementation queues conflicting work on — derived from the envelope's footprint, never declared (evaluation.md U3; built in compiler/.../Domains.kt).
• queue key — the engineer/PO-facing name for one member of a serialization domain: work sharing a queue key is handled one item at a time in arrival order; separate queues run independently. Chosen over "lock"/"synchronized" (which name one mechanism) and "serialize" (which engineers read as data marshalling) (stated on the generated commit functions).
• contention map — a compilation artifact (text or diagram) stating each act's queue key in business words ("deposits queue per account"), what contends with what, and every wide domain with the read that caused it — how unintentional system-wide queueing becomes visible to engineers and product owners before production (built — ContentionMapGen.kt, emitted in DIAGRAMS-<System>.md, normative in diagrams.md).
• hydration / resolver — the runtime demand-fetches the state an envelope needs through engineer-implemented storage questions: by key, by reference, by shape, captures (Hydration.kt, StateResolver).
• candidate pre-filter / superset contract — a compiled query trusted only for exclusion: it may over-return, never under-return; the authoritative predicate check stays in one evaluator, in memory (Hydration.kt, fetchCandidates; Query.kt).
• polarity-dual — how the pre-filter compiler keeps the superset contract: inexpressible predicate parts degrade to TRUE in positive position, FALSE under an odd number of negations (Query.kt).
• relevance gating — a commit evaluates only the watched conditions its mutation footprint can affect, per static read summaries (Runtime.kt).
• self-contained condition — one reading nothing beyond the base shape's own columns; the criterion for using the pre-filter soundly mid-envelope (Runtime.kt).
• scan floor — the fallback fetch: all of a shape, when no keyed or filtered path applies.
• retraction — deletion of a capture row at the exit commit's close: the contract's one sanctioned delete, legal because a capture is memory, not a record of the world (evaluation.md U2; Hydration.kt, Retraction).
• session handle / store key — runtime identity is process-local; durable identity belongs to the store and round-trips as Ref.Persisted/StoreKey (Hydration.kt). Session handles never reach the engineer: the surface works in references (below).

• query — one read request: a root (a shape or refinement), a filter in the spec's predicate language over the root's members, a required order, a page; composed by whoever asks, never declared in the spec (Reference §22; compiler/src/main/kotlin/velle/Read.kt). Called a "query", never a "question".
• registered query — a query the engineer writes with the typed builder and registers under a name (QueryRegistry), so it is checked against the spec at the engineer's build and can be named for the store (Reference §22).
• reference (Ref<T>) / model object — one reference type for both sides of the store boundary (2026-10-13): a record's concrete shape and store key, typed by the model object it points at. A model object is the shape's generated data class, every field read once at the moment of the read, and is itself a Ref<T> to its record: it passes wherever a reference is taken and equals any reference to the same record (equality is identity; whether two reads differ is a comparison of fields, the engineer's call — Dave, 2026-10-13). A reference field holds a Ref<T>; read(ref) resolves it. In memory the key is the runtime's own identity (Reference §22; Hydration.kt, Keyed).
• hidden tie-break — the store key carried inside a page cursor beside the last row's order datums, so pages stay stable when the caller's order does not tell two rows apart; never exposed as an ordering datum (Reference §5, §22).