Formal names are preserved here. Reader-facing descriptions appear first when a project term is unusually compact or opaque.
Admissible / admissibility. Licensed by a particular native judgment for a
complete claim. There is no global repository-wide Admissible predicate.
Authority. For a governed family and claim, Nonempty (F.Witness c).
It intentionally forgets witness multiplicity.
Authority-bearing verdict. A PathVerdict or LocatedVerdict with an empty
obstruction log. Related to family authority only by explicit seam theorems.
Barrier. A paid-reachability refusal: a region containing the origin, closed under native steps, and excluding the fixed goal.
BreakGlass. A bounded, origin- and history-sensitive instance for exceptional authority. It retains ordinary denial, audit history, and one exact obligation lifecycle rather than normalizing them away.
Book. One proposition-valued aspect of a claim: standing, custody, or obligation. The word emphasizes that these records are not interchangeable.
Claim. The family-native index of every witness and refusal. It may retain origin, phase, requested disposition, or other distinctions beyond an endpoint.
Comparison receipt. Proof data attached to one declared projection, classified as exact judgment, exact representation, directional with loss, or separation.
Core obstruction. A shared PathVerdict obstruction that every domain map
leaves unchanged.
Crossing. A binary construction that evaluates two governed families once, stores both native decisions, and derives every later result from that pair. It does not assert that the families share one semantics.
Custody (mathematical). A governed-family predicate whose preservation is required of witnesses.
Custody (repository). Publication and compatibility classification enforced by registries and gates. It is meta-level and must not be inferred from a Lean proof.
Domain obstruction. A native obstruction value in vocabulary δ.
Governed family. The ten-field shared signature connecting indexed evidence, three books, exclusivity, two witness laws, and a total decision.
Carried identity. An identifier preserved from an input by a sanctioned
construction such as foldLocated. Carrying does not authenticate the supplied
identifier.
Located verdict. An ordered log of (identifier, obstruction) pairs.
Lossless encoding. In this calculus, an encoding that exactly recovers full dependent refusal packets and rejects noncanonical successful decodes. It does not serialize accepted witness identity.
Obligation. A separate family-native predicate for outstanding duties. The core gives it no generic lifecycle law.
Refusal. Claim-indexed native data incompatible with a witness for the same claim.
Refusal packet. A dependent pair containing a claim and refusal indexed by that claim.
Refusal spine / spine. The PathVerdict diagnostic projection of a native
decision: accepted decisions become clean; refusals become encoded
obstructions.
Standing. The pre-claim basis book. Every witness requires it; it does not by itself introduce authority.
Stored decision. The pair of native Sum results retained by a binary
crossing and used by every downstream projection.
Weathering. The evidence-age licensing instance. It distinguishes direct reliance from downgrade, reprobe, and explicit stale carry; it is not a model of clocks or runtime monitoring.
Witness. Claim-indexed data that directly introduces derived authority.