Module error 

AxError, the one error shape of the whole city, and AxCode, the closed set of 35 error codes. The part crates/kernel/spec/Error.lean specifies this module.

Invariants owned here:

• every wire spelling (E_…) has exactly one authority: AxCode::as_str; serde delegates to it in both directions, so enum and wire cannot drift.
• a gate refusal always carries the three mandatory parts (rule, violation, alternative): AxError::refusal is the only path that sets them and AxError::failure cannot.
• every constructed error says what to do next: both constructors return an ErrorDraft, and ErrorDraft::with_recovery is the only way to obtain an AxError.
• retry defaults to Retry::No; a caller must opt in explicitly (fail-closed).
• account is AccountDisposition::Advance only beside Retry::No with no wait: ErrorDraft::account_unusable is the only path that sets it, and every other retry builder puts it back to Keep.

The carrier-event declaration (AxCode::carrier) lives together with kernel::event because it names EventKind.

Structs

AxError

The unified error shape: seven wire fields and two that are left out when absent, serialized in declaration order (determinism rule 6). The model is the recovery subject: nearby and recovery must hold directly executable information, not apologies.

ErrorDraft

An error that still owes the reader its recovery sentence.

GateRefusal

The three mandatory parts of a gate refusal: rule | violation | compliant alternative (three-part refusal).

Enums

AccountDisposition

Whether the account a request went out on can still take it (crates/kernel/spec/Error.lean D53).

AxCode

Closed set of error codes. Extension is additive only; the wire spelling lives in AxCode::as_str.

Carrier

Where an AxCode surfaces in history: its carrier event, or the loadtime class (the closed C9 exception: the Ledger is not writable yet).

ProviderFailureKind

The kind of one provider failure, as the call site that saw it named it. It travels on the wire so a page can say it in the reader’s own language; the city’s recovery sentence stays beside it for the fold.

Retry

Whether the same request may go out again, said together with whether its effect already landed. On the wire "yes", "no" or "unknown"; a ledger record written as retriable: true/false reads as Yes/No.