We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.

翻译：我们提出ZX-演算（知识演化演算），它是马丁-洛夫依赖类型论（MLTT）的保守扩展，整合了迹索引类型、预层非单调语义以及构造性AGM信念修正。论文附带Coq机械化证明（34个完整证明；两个核心结果零未证断言）。（I）迹类型。FinTrace(s0,sn)是类型化执行迹的归纳族。FinTrace与Star(Step)作为路径类型同构但非判断相等；TraceElim显式暴露事件标签e:Event，为事件驱动归纳提供更符合人体工学接口。我们证明了迹可达性对应性、确定性重演性，以及基于可归约候选的典则性框架与传输引理（RC消去推迟；其余核心结果均经Coq验证）。（II）层语义。迹索引命题是自由迹偏序范畴Tf上的逆变层。分离定理（显式反模型）区分了证明论单调性与语义非单调性。项模型是初始CwF（句法泛性质，非经典完备性）。（III）AGM信念修正。我们给出显式构造性偏交缩减算法，经(C1)-(C4)验证。全部八条AGM公设(R1)-(R8)均为定理。R7与R8的证明使用析取固守引理，并附独立构造性推导。（IV）集成。B^AGM不满足序贯修正的层复合律BP-comp（显式反模型，Coq验证）。我们引入单步修正系统（SSRS），证明B^AGM是有效SSRS（Coq验证），并表明这足以支持迹态射、收缩刻画与修正见证。BP-comp失效揭示了路径依赖信念修正与函子一致性之间的根本张力——此问题此前未被发现。