Mechanization

The runtime contract is mechanized in Lean as abstract signatures (parallel to std::kripke’s interface-only mechanization): Engine/Module/Store types, the OxbinRuntime trait surface, the bitemporal AsOf type, the three-capability surface, and the generation-monotonicity / cache-correctness invariant, under Argon/Runtime/. oxc-protocol::runtime mirrors the @[language_interface]-tagged types; CI fails on drift.