cairn_atproto^10 No Lean value holds a token

What it says

No type in cairn_atproto holds an access or refresh token: the session state has DIDs, handles, service URLs, request ids and the app's calls; SessionInfo has no token field and its decoder never reads accessJwt or refreshJwt (SessionInfo.ofJson_replaceTokens). By construction; checked by the trusted-base fuzz.

Evidence

assumed	Stated, not proved. The proofs rely on it.
fuzzed	Not shown yet: the trusted-base fuzzer's check `atproto.no-token` held. A CI step will publish it (#95).

Where it's defined

Declaration: CairnAtproto.Claims.noTokens
Module: CairnAtproto.Claims
Source: lean/CairnAtproto/Claims.lean:137 at v0.1.0
Statement hash: -

Ledger

cairn_atproto^10 is active in this version's claims.lock. An id never moves or changes meaning.