This is a formal-methods treatment of governed computation, not a blockchain, legal-evidence, smart-contract, audit-log, or category-theory system. The calculus asks which evidence justifies a claim while keeping standing, custody, authority, refusal, and obligation distinct. The repository-wide plain-language orientation explains how this v14 calculus sits beside the three-domain v15 Atlas.
Its evidence-returning decisions are about governed claims, not primarily proofs about proofs. Its receipts are typed semantic artifacts, not inherently cryptographic commitments. The bounded BreakGlass instance is an explicit exceptional-authority lifecycle, not an axiom that bypasses the calculus.
This documentation has three entrances. Choose the one that matches the question you are trying to answer; none requires prior knowledge of the repository’s release history.
The common subject is a calculus for evidence-bearing judgments. A complete claim is decided by returning either a claim-indexed witness or a claim-indexed refusal. Authority means that a witness exists. Standing, custody, and obligation remain separate books, and translations must state exactly which judgment or representation they preserve.
Read The Governed Admissibility Calculus if you want the easiest entrance. It develops the intellectual problem in ordinary language through four recurring examples:
Formal names appear only after the underlying idea has been introduced. Lean anchors are short, optional sections.
Read A Mathematical Presentation if you want definitions, inference rules, derivations, and counterexamples in paper notation. Each display is marked as a definition, primitive law, generic theorem, instance theorem, countermodel, or explanatory boundary. The text separates the mathematical rule from its Lean anchor.
This path assumes comfort with dependent types, sums, predicates, and basic proof notation, but not knowledge of the project’s campaign terminology.
Use the numbered chapters when you need a declaration-grounded account:
The glossary defines project vocabulary. The declaration index maps principal prose claims to exact Lean declarations and is the fastest route from a statement in either book to its implementation.
This layer is intentionally denser. It is for readers checking theorem scope, core-versus-instance boundaries, source locations, or proof status.
flowchart LR
C[complete claim c] --> D[decide c]
D -->|accepted| W[witness for c]
D -->|refused| R[refusal for c]
W --> A[authority]
W --> S[standing]
W --> K[custody]
O[obligation] -. separate native book .- A
R --> N[not authority]
R --> E[exact refusal encoding]
E --> V[diagnostic verdict]
Every arrow is one-way unless an equivalence is explicitly proved. Standing, custody, and absence of obligation do not create authority. The core calculus does not impose an obligation lifecycle; the bounded BreakGlass instance supplies one for its own claims.
The public Lean root is
LeanProofs.Admissibility.Calculus.
Its exact imports, theorem footprints, and publication status are repository
facts rather than premises of the mathematical exposition.
The claim register records claim-level status. The readiness ledger preserves detailed admission history and proof accounting. The declaration index links the mathematics to the public source without requiring either ledger as introductory reading.
No chapter claims that a runtime conforms to these definitions. Runtime conformance requires a separate correspondence proof and executable, revision-bound evidence.