docs: update all stale status markers in gap analysis tables

Fix 8 outdated ⚠️ status descriptions to reflect P0+P1 implementation:
- CEK Machine: "exists but not primary" → "upgraded to full executor (21 tests)"
- Cost vector: "not per CEK spec" → "per CEK spec, Prop. 23 enforced"
- MCP JSON Schema: "compiler ignores" → "Json(S) subtyping reuses JSON Schema"
- Runtime type checks: "runtime only" → "static T-Compose + runtime"

All ⚠️ markers eliminated from both zh-CN and en sections.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

RESEARCH_GAP_ANALYSIS.md

@@ -56,8 +56,8 @@
 | β-归约执行器 | `Executor.reduce()`，基于 isinstance 分派 | ✅ 覆盖全部 11 个构造 |
 | ReAct 7 阶段大步规则（B-React） | `ReActEngine` + `TerminationOracle` | ✅ 完成 |
 | 轨迹记录 | 每次 LLM/工具调用记录在 `TraceEntry` 中 | ✅ 完成 |
-| CEK 机器 | `cek_machine.py`（420 LOC） | ⚠️ 存在但非主运行时 |
-| 成本向量 `c = (τ, λ, μ)` | 轨迹记录 token/时长 | ⚠️ 未按 CEK 规范实现 |
+| CEK 机器 | `cek_machine.py`（P1-1 升级：IfK/RouteK 帧、handler 集成、async） | ✅ 已升级为完整执行器（21 tests） |
+| 成本向量 `c = (τ, λ, μ)` | CEK 每步跟踪 CostVector + cost_summary() + 单调性检查 | ✅ 按 CEK 规范实现（Prop. 23 enforced） |
 
 ### 差距
 
@@ -79,8 +79,8 @@
 
 | 理论贡献 | 实现 | 状态 |
 |---------|------|------|
-| MCP 工具 JSON Schema | MCP 工具有 schema 声明 | ⚠️ 存在但编译器忽略了 |
-| 运行时类型检查 | 执行器中的 `isinstance` | ⚠️ 仅运行时，非静态 |
+| MCP 工具 JSON Schema | MCP 工具有 schema 声明 | ✅ Json(S) 子类型复用 JSON Schema（`types.py`） |
+| 运行时类型检查 | 执行器中的 `isinstance` | ✅ 静态 T-Compose 检查 + 运行时（`types.py`, 44 tests） |
 
 ### 差距
 
@@ -364,8 +364,8 @@ P1: CEK 机器
 | β-reduction executor | `Executor.reduce()` with isinstance dispatch | ✅ Covers all 11 constructs |
 | ReAct 7-stage big-step rule (B-React) | `ReActEngine` with `TerminationOracle` | ✅ Complete |
 | Trace recording | Every LLM/tool call recorded in `TraceEntry` | ✅ Complete |
-| CEK Machine | `cek_machine.py` (420 LOC) | ⚠️ Exists but NOT the main runtime |
-| Cost vector `c = (τ, λ, μ)` | Trace records token/duration | ⚠️ Not per CEK spec |
+| CEK Machine | `cek_machine.py` (P1-1 upgrade: IfK/RouteK frames, handler integration, async) | ✅ Upgraded to full executor (21 tests) |
+| Cost vector `c = (τ, λ, μ)` | CEK per-step CostVector + cost_summary() + monotonicity check | ✅ Per CEK spec (Prop. 23 enforced) |
 
 ### Gaps
 
@@ -387,8 +387,8 @@ P1: CEK 机器
 
 | Theoretical Contribution | Implementation | Status |
 |--------------------------|----------------|--------|
-| MCP tool JSON Schema | MCP tools have schema declarations | ⚠️ Exists but compiler ignores it |
-| Runtime type checks | `isinstance` in executor | ⚠️ Runtime only, not static |
+| MCP tool JSON Schema | MCP tools have schema declarations | ✅ Json(S) subtyping reuses JSON Schema (`types.py`) |
+| Runtime type checks | `isinstance` in executor | ✅ Static T-Compose checking + runtime (`types.py`, 44 tests) |
 
 ### Gaps