lean

3. Books, authority, and checking

“Authorized” is too coarse if it hides the basis for making a claim, the provenance a witness must preserve, or a duty that remains open. The calculus keeps those questions separate before defining authority.

Three separate books

For a claim c, a governed family carries three independent propositions, called books because they record different aspects of the claim:

F.Standing c
F.Custody c
F.Obligation c

Standing records the pre-claim basis required by the family. Custody records provenance intactness. Obligation records outstanding duties. They are separate because the public examples make different combinations meaningful:

• the bare paid claim has custody vacuously but no authority (custody_does_not_grant_dynamic_authority);
• the BreakGlass audit-laundering claim has settlement standing but is refused by the independent audit-history condition (audit_launder_has_settlement_standing);
• BreakGlass obligation is absent before commit, live at commit, and closed at settlement (three lifecycle theorems).

Collapsing the books into a single “good” predicate would erase these states. The abstraction exports no theorem Standing c → Authority c, Custody c → Authority c, or ¬ Obligation c → Authority c.

Authority is derived

Authority is not a field supplied by an instance:

def GovernedFamily.Authority (c : F.Claim) : Prop :=
  Nonempty (F.Witness c)

(source). Thus an instance cannot install a second authority introduction rule while still using this definition. Authority deliberately squashes witness identity. The theorem authority_has_no_multiplicity makes that explicit: consumers that count receipts must count native Witness data, not proofs of Authority.

Theorem — authority_requires_standing. Authority entails standing because every contained witness must entail standing. It does not say that standing suffices.

Theorem — authority_preserves_custody. Authority entails custody because every contained witness preserves custody. It does not say that custody supplies or repairs a witness.

Theorem — refusal_refutes_authority. Native refusal evidence and authority cannot coexist, by the family’s exclusive law.

The total evidence-returning checker

The checker has the exact shape

F.decide : (c : F.Claim) → Sum (F.Witness c) (F.Refusal c)

It is total because every input claim produces one branch. It is not a generic search procedure: each instance supplies its own implementation. For example, the paid family uses a hand-written two-constructor match (source); this proves no arbitrary reachability decision algorithm.

The Boolean branch view is derived only after the native evidence exists:

F.Authority c ↔ (F.decide c).isLeft = true

(authority_iff_decide_isLeft). This Boolean is a view of a stored Sum; it is not the checker contract and cannot recover refusal data by itself.

flowchart TD
  D[decide c] --> L[Sum.inl witness]
  D --> R[Sum.inr refusal]
  L --> A[Authority c]
  L --> S[Standing c]
  L --> C[Custody c]
  R --> N[not Authority c]
  O[Obligation c] -. family-native lifecycle .- D

The diagram contains no arrow from any book back into Authority. That absence is part of the signature’s meaning.

Instance boundary. The core supplies no obligation lifecycle. The before/commit/settlement facts above belong only to BreakGlass.

This site is open source. Improve this page.