Wire and Lean correspondence

Member rules are emitted as ordinary RuleDecl/QueryDecl events; invocation-plane members as ordinary MutationDecl/ComputeDecl events keyed Trait::member@Target — no new AxiomKind. TraitDeclBody.methods carries member signatures (all five planes); ImplDeclBody.items carries member provenance (both fields carry it — the wire is built for this). spec/lean/Argon/Substrate/Trait.lean carries the @[language_interface] shapes; Argon.TypeSystem.Conditional states the coherence contract that OE0673 enforces. The Lean obligations for this design (monomorphization conservativity on the Reasoning/Datalog/ spine; coherence instantiation; structural-tier conformance) are listed in RFD 0026.