Lean 4 formalization of the exchange protocol schemas.
This repository provides a Lean 4 formalization of the structural core of the Exchange Protocol, including canonical record schemas for entities, relationships, and exchanges; a shared RecordEnvelope; retention-policy data shapes; and basic graph-oriented data structures. The code machine-checks the well-formedness and typing of these structures and verifies that the protocol's core representations are internally consistent and composable, without embedding causal, normative, or policy interpretations.
lake update
lake build
lake exe verify