The Agreement Walk Calculus: A Federated Formalization in Lean, Coq, and Agda

Initial public release of the Agreement Walk Calculus — three independent proof-kernel formalizations of a position assistant. Contents Lean 4 (lean/): Full formalization with AgreementWalk.lean and ProofKernel.lean Coq (coq/): Independent formalization with AgreementWalk.v and ProofKernel.v Agda (agda/): Independent formalization with AgreementWalk.agda and ProofKernel.agda Each kernel proves the same three theorems: Walk well-formedness (every step is a valid transition) Agreement preservation (agreement holds at every step) Termination (every walk reaches a terminal state) Verification All three proof kernels type-check independently. See VERIFICATION.md for instructions. Related QICT-NOTE-001: doi:10.5281/zenodo.22309225 Companion paper: doi:10.5281/zenodo.22548389