← unpingable
Glossary
What the project vocabulary means, in one place. The prose elsewhere uses these terms; this page is where they’re defined. Where receipt identifiers and prose words diverge (prose permission, receipt field standing), the entry notes both.
If you're new, the bridge from plain words to the precise ones:
| plain term | precise term |
| system / component set | constellation |
| what can be relied on | admissibility |
| proposed / not yet accepted | candidate |
| public claim / accepted claim | minting |
| observed evidence | witness testimony |
| permission / scoped authority | standing |
| blocked — required evidence/action missing | obstruction |
| what agents are not allowed to do | non-grant |
admissibility
approval
attestation
authority
authorization
boundary
candidate
claim
custody
expiry
gap
kernel
minting
non-grant
obstruction
permission
policy
preflight
premise
receipt
refusal class
spendability
standing
wicket
witnessed
- admissibility #
- A claim’s eligibility to become a premise for action. Custody decides admissibility; refusal classes name the specific ways it can fail. The Lean theorems live under
Admissibility.* and prove the class boundaries. Prose elsewhere on the site uses the longer phrase “allowed to become a premise” for cold readers; receipt and Lean identifiers use the noun directly.
- approval #
- An explicit operator or gate decision over a specific proposal, at an authority-bearing surface, with scope, time, and evidence recorded. What approval is not: an agent saying “done,” a passing test run, a chat message, a completed rehearsal, a green check, or a demo succeeding. Approval is a bounded authority-bearing act — if nothing recorded a scoped decision, nothing was approved. Contrasts with automatic promotion: agents may propose; approval is a distinct operator/gate step, never a byproduct.
- attestation #
- Evidence that someone or something observed and recorded a claim, with attribution. Distinct from a signature (which proves who said the thing, not whether it was observed) and from a log line (which records but doesn’t attest). Receipts are attestations of custody decisions;
nq records attestations of operational observations.
- authority #
- The right to make a decision binding on a system. Distinct from permission (which is the grant to act) and from policy (which is the rule the authority applies). In the conversion chain, authority sits between premise and action: a premise becomes an action only if some authority licenses it. In prose: an “authority-bearing surface” is one where touching it has binding effect.
- authorization #
- The question of whether an action is allowed under stated rules: returns yes/no over an input claim (“the credential says valid; the role says operator”). What conventional auth checks and most policy engines do well. Distinct from custody: authorization decides whether the action is permitted; custody decides whether the input claim is still good enough to act on.
- boundary #
- A named conversion point in the custody chain where one kind of claim becomes another — e.g., an observed permission becoming one usable at action time. The boundary is the place where the conversion can refuse.
- In receipt fields:
seam.
- candidate #
- A proposed claim, action, or receipt that has entered the system but has not yet been admitted as authoritative. Agent output arrives as candidate: it may carry structure and content, but it does not carry authority until a gate admits it. The word is deliberately distinct from approved or accepted — candidate names the intermediate status where proposal exists but promotion has not.
- claim #
- An assertion that something is true: that a credential is valid, a monitor is green, an action is allowed. Claims arrive from many sources (log lines, API responses, model outputs, human approvals) and may be witnessed, stale, or self-reported. A claim is not yet a premise — whether it may become one is the custody question.
- custody #
- The layer that controls whether a claim may become a premise for action. Distinct from authorization (which asks only whether the action is allowed) and from policy (which decides over premises it has been handed). Custody decides whether the premises it would hand the policy are still good enough to act on.
- expiry #
- The time after which a previously-valid observation can no longer license an action. An observation’s expiry comes from whoever issued it, on a stated clock; the custody check at action time measures against that stated clock, not against wall time.
- In receipt fields and Lean theorems:
horizon.
- gap #
- Elapsed time between when an observation was taken and when it’s being used — measured on a typed clock basis (named source, named epoch). The gap is compared to a bound declared at issuance time; the bound and the expiry are the same issuer-declared limit, expressed as a duration vs. a deadline. Custody refuses when the measured gap exceeds the bound on the named basis. Wall time is not the basis (it can move sideways under NTP); the basis is named explicitly in every receipt.
- kernel #
- The minimal rule core of a check: small enough that its refusal classes can be stated precisely, and in this project, checked in Lean. Distinct from the runtime that implements it. “Custody kernel” = the rules that license refusals; “intent preflight kernel” (wicket) = the small set of conditions an intent must satisfy to become a premise.
- minting #
- Promoting a candidate into an authoritative artifact — a released version, an accepted claim, a receipt others may rely on. Minting is the explicit act of granting authority to something that previously carried none. Distinct from visibility: a candidate can be visible (committed, pushed, published as a draft) without being minted. Custody insists this step be explicit — not something that happens by accident when an agent finishes running.
- non-grant #
- A capability an agent is deliberately not given, with enforcing code and tests on the line that denies it. Not a warning or a policy note — a structural refusal. The non-grant list names what agents cannot do (approve themselves, promote their own output, mint authority from prose, use permissions after expiry, turn rehearsal into production, treat “tests passed” as safe to land) and points at the code that refuses each case.
- obstruction #
- A refusal grounded in missing evidence or action — the gate cannot proceed because a required witness, receipt, seal, or step is absent. Distinct from a substantive refusal (evidence exists but fails a predicate): an obstruction says “I do not have what I need to decide.” Reported as absence rather than inferred away; the point is that the gap is visible and named.
- permission #
- An active grant to perform a thing, observed at a specific moment with a valid-until time. A permission valid when checked is not automatically usable at action time — the gap between check and action may exceed the permission’s expiry.
- In receipt identifiers and the component name:
standing.
- policy #
- A set of rules that decides over inputs a system treats as premises — e.g., OPA/Rego over an input document, RBAC over an identity. Returns a verdict over what it’s been given. Distinct from custody: policy decides over premises; custody decides whether the underlying claims deserved premise status in the first place. The two compose — OPA can run happily inside a custody stack.
- preflight #
- A check that runs before an action is permitted to take effect. Distinct from logging (records but does not gate) and from postmortem (runs after). The custody stack uses preflight at three layers:
nq for observation→claim, wicket for intents, and verifier for declared constraints.
- premise #
- A claim that custody has admitted as the basis of an action. The conversion claim → premise is what custody gates. Policy engines decide over premises; custody decides whether the underlying claims are allowed to become premises in the first place.
- receipt #
- A content-addressed record of a custody decision. The receipt id is a deterministic hash of inputs — the same inputs always yield the same id (you can reproduce
dda5a1e5… from a cold clone). Distinct from a log line: a log describes; a receipt attests, with attribution and a return address.
- refusal class #
- A typed category of refusal that the custody kernel licenses by definition — not a discretionary denial. Example:
standing_before_spendability_not_bounded is the refusal class for “permission observed earlier than the action, with the gap exceeding the bound.” The Lean theorems prove these class boundaries; the receipt attests the instance. See limits for what each does and doesn’t prove.
- spendability #
- A specific boundary check: whether a permission observed earlier is still usable at action time. Receipt fields and refusal-class names use
spendability (e.g., standing_spendability_seam); prose tends to use the longer phrase (“usable at action time”) because the bare noun reads as a coinage to cold readers.
- standing #
- Code and receipt name for a permission observation with age and expiry. In prose, this site usually says permission. The component named
standing produces standing receipts (with observation age); receipt fields like standing_spendability_seam and standing_before_spendability_not_bounded use the code name.
- wicket #
- The intent preflight kernel — decides whether an intent (the AI agent’s proposed action) may become a premise before any effect runs. Refuses intents from revoked or out-of-scope actors.
- witnessed #
- A claim is witnessed when its assertion is traceable to an observation that took it — with the observation’s source, time, and basis preserved. Distinct from signed (which proves an issuer’s signature but not what the issuer actually observed) and from self-reported (an actor asserting something about itself without independent attestation). Witnessing is the property the conversion observation→claim is supposed to preserve.
Notes on choices: this glossary preserves the project’s vocabulary where the ordinary alternative would launder a technical invariant (custody, premise, refusal class) and aligns prose with ordinary wording where it doesn’t (permission, expiry, boundary). Receipt identifiers and Lean theorems keep their original names; this page is the bridge.