The light client: verify everything, re-execute nothing
The point of the whole construction is a reader who cannot be fooled. A
light client holds one aggregate root and runs one check —
verify agg.root — and from that single verification learns that
every turn in the history executed correctly, in order, under every guarantee
of the previous rungs: authority non-amplified, value conserved, receipts binding,
nullifiers fresh. It re-executes nothing, holds no witnesses, and trusts no executor.
This works because proofs fold: each turn's proof attests its own step plus the proof before it, and the seam between steps is pinned — the post-root of step i must be the pre-root of step i+1. A reordered, dropped, or spliced history cannot produce a verifying aggregate; the binding fails structurally, not by convention. Tampering anywhere in the past is not "detectable" — it is unprovable.
Proofs are attestation, not permission
Between parties that already trust each other's execution, turns flow as signed receipts and nobody waits on a prover. The proof layer is additive: it exists so that someone who was not there — a new node, a counterparty's auditor, a phone — can verify the whole past at the cost of one check. Sovereign cells carry this to its end: a cell whose host keeps only a commitment proves its own transitions, so a far federation admits it knowing only how to check a proof, never how to re-run it.
The assumption floor
"Verify everything" is unconditional in the Lean-kernel sense modulo a small, explicit set of cryptographic and liveness carriers. This is the entire list — stated plainly because a floor you can't enumerate is a floor you can't stand on:
- Poseidon2-permutation collision-resistance — the arithmetization-friendly hash; the sponge/Merkle/state-commitment/MMR collision-resistance is reduced to permutation-CR (
Crypto.Poseidon2*,Crypto.Merkle, therecStateCommitinjectivity portal, the receipt-indexLightclient.MMR.mroot_binds_position, and the sorted-set/queueApps.QueueRoot.RootCR/LenBindCRand identity-keysetApps.PreRotation.KeySetCRcarriers — every one a named CRPropover aPoseidon2/BLAKE3image, NOT anaxiom). - BLAKE3 collision-resistance — the out-of-circuit content/transcript hash.
- ed25519 EUF-CMA — turn / strand-block signature unforgeability.
- HMAC (PRF/MAC) unforgeability — macaroon caveat-chain tags (
Authority.CaveatChain). - AEAD confidentiality+integrity — sealed-value / disclosure payloads.
- Discrete-log hardness — Pedersen value commitments (
Crypto.Pedersen). - FRI / the STARK soundness chain — a verifying proof attests its statement; the one recursion obligation
RecursiveAggregation.EngineSound.recursive_sound. - PostGSTProgress — the network is eventually synchronous (after GST); the consensus LIVENESS carrier (
World.gst_liveness, derived from a DLS88/HotStuffPacemaker).
Dregg2/AssuranceCase.lean. These enter as Prop-portals (typeclass fields /
hypotheses), never as axioms; no other assumption is load-bearing anywhere in the case.Everything above this floor is theorem; nothing else is load-bearing. In particular there is no trusted executor, no out-of-band "this was authorized" premise, and no field of the post-state left uncommitted.
Grounding
Circuit/RecursiveAggregation.lean—light_client_verifies_whole_history(the headline),attested_history_conserves(conservation lifted to the full run),tampered_aggregate_cannot_bindandleaf_pairing_defeats_swap(the anti-tamper teeth).Distributed/HistoryAggregation.lean—wellformed_attests_whole_history,root_tooth_pins_state(a client seeing only roots learns state continuity).Dregg2/AssuranceCase.lean— Guarantee E, with the floor above as its only carriers.
Touch it: the explorer surfaces each turn's proof and trust tier; the badges are driven by the same generated assurance catalog this page embeds.