diff --git a/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.md b/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.md
index a491058c5b..a8594d8d31 100644
--- a/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.md
+++ b/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.md
@@ -82,10 +82,17 @@ default-entry adoption.
 | `task_lease.acquire.decide`, `task_lease.lifecycle.decide`, `coordination.handoff_mode.plan` RPC registrations | Only those retired facades / handler tests; native transactions call the same typed rules directly | Obsolete private RPCs now reject unsupported methods. Keep `task_lease.owner_eligibility` and write-scope overlap: actual Python callers remain. |
 | Lease-only `local_snapshot.py` normalization and error projection | No remaining caller; native executors own lease facts and errors | Keep `todo_snapshot_from_mapping`, used by live Todo mutation authorization. No store, receipt, backup or migration reader is removed. |
 
-`authority_core.py` is still a live Todo bridge. `LeaseAction` and
-`LeaseModeGateCommand` also remain because the semantic-vocabulary registry
-explicitly retains that input contract until its M4 review. This slice does not
-lower semantic coverage floors to discard a declared compatibility obligation.
+`authority_core.py` remains a live Todo bridge. At the #5395 boundary,
+`LeaseAction` / `LeaseModeGateCommand` remained registered until M4 review.
+The bounded M4 package now retires that unused private input and its union,
+with a regrowth/import guard and explicit internal import incompatibility.
+The valuable native lifecycle subset proof is rehomed to its actual TS request
+owner; the 26/51/9 coverage floors and all remaining budgets stay unchanged.
+Installed File/SQLite lease/recovery tests run with the old input truly absent.
+Restore the previous code package to recover private imports, without a state
+conversion. Public lease transactions, source writers/outbox, legacy policy,
+historical backup/format/receipt readers and permanent Host IO remain. This
+is a last-caller slice, not whole C1/M4, D2 or release-default completion.
 Old facade-only tests retired with their implementation; public/native behavior
 tests remain. Reverting this slice restores the internal crossing without a data
 conversion. Local CLI adoption at `db3672f3c` verifies a clean source manifest,
diff --git a/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.zh-CN.md b/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.zh-CN.md
index 266f0023bc..f6f9a86d3d 100644
--- a/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.zh-CN.md
+++ b/docs/architecture/rfcs/ledger/shared-goal-authority-state-provider-v0/2026-09-28-retirement-cadence.zh-CN.md
@@ -73,9 +73,15 @@ Python 退役收益。调用方清单如下：
 | `task_lease.acquire.decide`、`task_lease.lifecycle.decide`、`coordination.handoff_mode.plan` RPC 注册 | 只剩这些旧 facade／handler 测试；原生事务直接复用同一 TS 规则 | 废弃私有 RPC 明确拒绝；保留仍有 Python 调用方的 `task_lease.owner_eligibility` 和 write-scope overlap。 |
 | `local_snapshot.py` 中仅供 lease 的规范化和错误投影 | 已无调用方；原生执行器拥有 lease 事实与错误 | 保留真实 Todo mutation authorization 使用的 `todo_snapshot_from_mapping`；不删 store、回执、备份或迁移 reader。 |
 
-`authority_core.py` 仍是活跃 Todo bridge。`LeaseAction`、`LeaseModeGateCommand`
-也保留：semantic-vocabulary 注册表明确将该输入契约保留到 M4 评审。本切片不通过
-降低语义覆盖下限丢弃已有兼容义务。仅服务旧 facade 的测试随实现退役，公共／原生
+`authority_core.py` 仍是活跃 Todo bridge；#5395 当时将
+`LeaseAction`／`LeaseModeGateCommand` 保留到 M4 评审。有界 M4 包现退役无人
+使用的私有输入及其 union，加入定义／import 回生守卫，明确内部 import 不兼容。
+有价值的原生 lifecycle 子集证明改为引用实际 TS request owner；26／51／9
+覆盖下限及其他预算保持。安装态 File／SQLite lease／恢复测试在旧接口真正
+不存在时执行。回退旧代码包即可恢复私有 import，无需状态转换。公共 lease
+事务、source writer／outbox、legacy 策略、历史备份／格式／回执 reader 和永久
+Host IO 保留。这是最后调用方切片，不代表整项 C1／M4、D2 或发布默认资格完成。
+仅服务旧 facade 的测试随实现退役，公共／原生
 行为测试保留。回退该切片可恢复内部跨界，无需转换数据。本机 CLI 已采用
 `db3672f3c`，验证了干净源码清单、具备资格的 SQLite runtime、已知权威格式均为
 当前版本及健康的 canonical 合同读回。这不证明所有已安装 Host 或 D2 已验收。
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 76ae922a42..b6405d5528 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -439,7 +439,7 @@ not a proof of reachability or whole-program data flow.
 `uv run python examples/semantic-vocabulary-drift-smoke.py --report` lists unresolved
 production locations. Unresolved parts cannot supply missing value evidence; known
 conditional branches remain structural witnesses, not reachability proofs.
-The producer guard covers all six kernel entries using distinct evidence lanes:
+The producer guard covers the five live kernel entries using distinct evidence lanes:
 `effective_action`, `turn_route`, `loop_disposition`, and
 `agent_scope_frontier_action` have source witnesses; `turn_result_kind` also has
 executable input witnesses at the fixed `transaction._result_kind` decoder.
@@ -448,13 +448,32 @@ invalid probes must report rejection. This proves a permitted production path,
 not that a Host has emitted every member or that every host execution is valid.
 `input_producer` cannot select arbitrary code: the verifier is fixed in the smoke.
 
-`lease_action` is explicitly legacy/compatibility-only: in-repository runtime
-callers use whole native acquire/renew/transfer/release transactions. Unconsumed
-Python command facades are retired independently of this declared input contract.
-Its four members remain available to the existing typed `LeaseModeGateCommand` input
-interface until M4 caller/migration review. No persisted usage is asserted.
-The producer list is empty only because every value carries an explicit reason
-and retirement milestone. A newly observed producer invalidates that declaration. Kernel families without producer metadata are printed as coverage pending; their
+M4 retires the unused private Python `LeaseAction`, `LeaseModeGateCommand` and
+its `CoordinationCommand` union, after source/registration and isolated installed
+caller review. `lease_action` leaves the registry with that input contract. This
+changes internal Python import compatibility; it does not remove the shipped
+lease verbs, the `legacy` ownership policy, or pre-canonical Goal recovery.
+
+The useful lifecycle subset check now references the actual TypeScript request
+owner, `TASK_LEASE_LIFECYCLE_OPERATIONS`, registered as
+`task_lease_lifecycle_operation`: renew/transfer/release plus terminal/holder
+verification and fence cleanup. Acquisition retains its separate native
+transaction. The mutation decision subset excludes those three verification and
+cleanup operations. Coverage floors remain 26 vocabularies, 51 owner symbols and
+9 relations; no empty owner or fake producer replaces the retired interface.
+Its native request values carry notes and owner/subset checks, but production
+liveness is explicitly unverified: the formal producer domain now has six
+entries, five kernel and one cross-runtime, with twenty cross-runtime entries
+outside it. No surviving producer check or inventory budget is relaxed.
+
+The drift smoke rejects restored definitions or statically resolved imports of
+the retired input; fresh-wheel negative imports and real File/SQLite
+lease/replay/conflict and unpromoted Goal paths qualify the installed boundary.
+Dynamic/external imports are not a whole-program compatibility proof. Retain the
+live Todo bridge, historical backup/format/receipt readers and Host IO. Reverting
+this code package restores the private imports without converting persisted
+state. This slice does not complete all M4, C1 or release-default qualification.
+Kernel families without producer metadata are printed as coverage pending; their
 owner parity must not be reported as I12/I13 completion. M0.5 remains incomplete
 until all required families meet its acceptance rows.
 
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
index 099afd8f6a..e5237b33ca 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -332,19 +332,32 @@ TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript
 数据流证明。
 
 `uv run python examples/semantic-vocabulary-drift-smoke.py --report` 列出未解析的生产
-位置。unknown 不能补足缺失值的生产证据。生产者守卫对六个 kernel 条目使用不同证据：`effective_action`、`turn_route`、
+位置。unknown 不能补足缺失值的生产证据。生产者守卫对五个活跃 kernel 条目使用不同证据：`effective_action`、`turn_route`、
 `loop_disposition` 和 `agent_scope_frontier_action` 使用源码见证；
 `turn_result_kind` 另有固定入口 `transaction._result_kind` 的可执行输入见证。
 真实解码器必须为每个注册输入返回相同的类型化成员，并拒绝非法探测输入。这证明
 存在允许的生产路径，不表示 Host 实际发出过全部成员或所有 Host 执行都合法。
 `input_producer` 不能从数据任意指定执行代码，验证入口固定在 smoke 中。
 
-`lease_action` 明确分类为 legacy/兼容保留：仓库运行时调用者直接使用
-完整的 native acquire／renew／transfer／release 事务。已无调用方的 Python command
-facade 独立退役，不因此丢弃这个已声明的输入契约。四个成员为旧的类型化
-`LeaseModeGateCommand` 输入接口保留到 M4 调用者/迁移评审；不声称存在持久化
-使用。只有每个值都带保留理由及退休里程碑时，生产者列表才能为空。新发现的
-生产者必须让原兼容声明失败。
+M4 在源码、注册入口和隔离安装态调用方评审后，退役无人使用的私有 Python
+`LeaseAction`、`LeaseModeGateCommand` 及其 `CoordinationCommand` union；
+`lease_action` 随输入契约退出注册表。这改变内部 Python import 兼容性，不删除
+公共 lease 动词、`legacy` 所有权策略，也不强迫 pre-canonical Goal 升级。
+
+有价值的 lifecycle 子集检查改为引用实际 TS request owner
+`TASK_LEASE_LIFECYCLE_OPERATIONS`，登记为 `task_lease_lifecycle_operation`：
+renew／transfer／release，以及 terminal／holder 验证和 fence 清理。acquire
+仍有独立原生事务；mutation decision 子集排除这三项验证／清理操作。覆盖下限
+仍为 26 个词表、51 个 owner、9 项关系，不用空 owner 或伪造生产者替代旧接口。
+原生 request 值仍接受含义、owner 和子集检查，但生产活性明确未验证；形式化
+生产者域现为六项（五项 kernel、一项 cross-runtime），域外二十项 cross-runtime
+保持未验证。不放宽其他生产者检查或 inventory 预算。
+
+drift smoke 拒绝恢复旧定义或静态解析出的旧 import；fresh-wheel 负例与真实
+File／SQLite lease、重放、争用和 unpromoted Goal 路径验证安装态边界。动态／
+外部 import 不因此获得全程序兼容证明。保留活跃 Todo bridge、历史备份／格式／
+回执 reader 和 Host IO；回退代码包即可恢复私有 import，无需数据转换。本切片
+不代表全部 M4、C1 或发布默认资格完成。
 没有生产者元数据的 kernel 词表会明确
 报告为覆盖待完成，不能把 owner 一致性宣称为 I12/I13 完成。所有要求的词表通过
 相应验收行之前，M0.5 仍未完成。
diff --git a/docs/reference/glossary.md b/docs/reference/glossary.md
index dae3fdc1fa..3abbf0a74d 100644
--- a/docs/reference/glossary.md
+++ b/docs/reference/glossary.md
@@ -112,15 +112,6 @@ Authority handoff mode between agents.
 - typescript: [`HANDOFF_MODES`](../../loopx/control_plane/coordination/handoff_mode_vocabulary.ts).
 - Values / 值: `legacy`, `soft_claim`, `hard_lease`.
 
-## lease_action
-
-Authority-core lease mutation verb.
-
-- Tier / 层级: `kernel`; status / 状态: `legacy`.
-- python: [`LeaseAction`](../../loopx/control_plane/coordination/authority_core.py).
-- Values / 值: `acquire`, `renew`, `transfer`, `release`.
-- Compatibility only / 兼容保留: `acquire`, `release`, `renew`, `transfer`.
-
 ## loop_disposition
 
 Pure controller verdict for the outer loop after combining the last Turn receipt with the fresh route.
@@ -193,6 +184,14 @@ Effect-program settlement step executed for one Turn.
 - typescript: [`SETTLEMENT_STEP_KINDS`](../../loopx/control_plane/effect_program.ts).
 - Values / 值: `validation`, `durable_writeback`, `quota_spend`, `terminal_closeout`.
 
+## task_lease_lifecycle_operation
+
+Operation accepted by the shipped native lease lifecycle request decoder; acquisition has its own transaction.
+
+- Tier / 层级: `cross_runtime`; status / 状态: `canonical`.
+- typescript: [`TASK_LEASE_LIFECYCLE_OPERATIONS`](../../loopx/control_plane/work_items/task_lease_lifecycle_request.ts).
+- Values / 值: `renew`, `transfer`, `release`, `terminal_verify`, `holder_verify`, `fence_close`.
+
 ## todo_completion_continuation
 
 Continuation declared by a completing Todo.
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index bac704c699..1ce94c5c6a 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -14,6 +14,7 @@
 
 from __future__ import annotations
 
+import ast
 import json
 import re
 import sys
@@ -208,7 +209,7 @@
     "settlement_binding_kind": "loopx/control_plane/effect_program.ts::settlementIdentity",
 }
 PRODUCER_VOCABULARY_ANCHOR = {
-    "effective_action", "turn_route", "loop_disposition", "agent_scope_frontier_action", "turn_result_kind", "lease_action",
+    "effective_action", "turn_route", "loop_disposition", "agent_scope_frontier_action", "turn_result_kind",
     # First cross-runtime vocabulary carrying executed production evidence. One
     # named boundary, not a claim about the rest of the cross-runtime set.
     "settlement_binding_kind",
@@ -569,6 +570,47 @@ def check_invariant_domain(invariant: dict[str, Any], registry: dict[str, Any])
             f"formal invariant {name} cannot verify more members than the registry holds")
 
 
+# M4 disposed of this private Python input. Keep its import boundary absent,
+# rather than claiming liveness from a compatibility-only enum with no callers.
+# The native lifecycle relation is retained against its actual TypeScript owner.
+RETIRED_LEASE_INPUT_MODULE = "loopx.control_plane.coordination.authority_core"
+RETIRED_LEASE_INPUT_SYMBOLS = frozenset({"LeaseAction", "LeaseModeGateCommand", "CoordinationCommand"})
+
+
+def check_retired_lease_input(registry: dict[str, Any], sources: list[SourceFile]) -> None:
+    from importlib.util import resolve_name
+
+    require("lease_action" not in registry["vocabularies"],
+            "retired lease input must not return to the registry")
+    lifecycle = registry["vocabularies"].get("task_lease_lifecycle_operation", {})
+    require(lifecycle.get("owners") == {
+        "python": None,
+        "typescript": "loopx/control_plane/work_items/task_lease_lifecycle_request.ts::TASK_LEASE_LIFECYCLE_OPERATIONS",
+    }, "native lease lifecycle coverage must retain its actual owner")
+    for source in sources:
+        if source.suffix != ".py":
+            continue
+        module = source.path.removesuffix(".py").replace("/", ".")
+        package = module.rpartition(".")[0]
+        for node in ast.walk(ast.parse(source.text)):
+            if module == RETIRED_LEASE_INPUT_MODULE:
+                names = set()
+                if isinstance(node, (ast.ClassDef, ast.FunctionDef)):
+                    names.add(node.name)
+                elif isinstance(node, ast.Assign):
+                    names.update(target.id for target in node.targets if isinstance(target, ast.Name))
+                elif isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name):
+                    names.add(node.target.id)
+                retired = sorted(names & RETIRED_LEASE_INPUT_SYMBOLS)
+                if retired:
+                    raise Drift(f"{source.path}:{node.lineno}: retired lease input definition {retired}")
+            if isinstance(node, ast.ImportFrom):
+                target = resolve_name("." * node.level + (node.module or ""), package) if node.level else node.module
+                if target == RETIRED_LEASE_INPUT_MODULE:
+                    retired = sorted({alias.name for alias in node.names} & RETIRED_LEASE_INPUT_SYMBOLS)
+                    require(not retired, f"{source.path}:{node.lineno}: retired lease input import {retired}")
+
+
 def check_coverage_floor(registry: dict[str, Any]) -> str:
     try:
         quota_action_domain(registry)
@@ -1129,6 +1171,7 @@ def main() -> int:
     registry = load_registry()
     coverage = check_coverage_floor(registry)
     sources = load_sources(REPO_ROOT)
+    check_retired_lease_input(registry, sources)
     registry_io_manifest = json.loads(
         (REPO_ROOT / PROJECT_REGISTRY_IO_MANIFEST).read_text(encoding="utf-8")
     )
diff --git a/loopx/control_plane/coordination/authority_core.py b/loopx/control_plane/coordination/authority_core.py
index 31e33fae8b..c66a4c44fb 100644
--- a/loopx/control_plane/coordination/authority_core.py
+++ b/loopx/control_plane/coordination/authority_core.py
@@ -6,9 +6,8 @@
 storage outcomes deliberately live outside this module. Todo lifecycle admission,
 ownership routing and terminal fences adapt to canonical TypeScript decisions.
 Lease and handoff writers use their whole native transactions directly; their
-unconsumed Python decision facades are retired. Python retains live Todo
-snapshot/result adaptation and the explicitly registered legacy lease-mode
-input contract until its semantic-vocabulary retirement review.
+unconsumed Python decision facades and lease-mode input are retired. Python
+retains the live Todo snapshot/result adaptation, not a second lease rule.
 """
 
 from __future__ import annotations
@@ -36,13 +35,6 @@ class TodoAction(StrEnum):
     SUPERSEDE = "supersede"
 
 
-class LeaseAction(StrEnum):
-    ACQUIRE = "acquire"
-    RENEW = "renew"
-    TRANSFER = "transfer"
-    RELEASE = "release"
-
-
 class DecisionOutcome(StrEnum):
     APPLY = "apply"
     NO_CHANGE = "no_change"
@@ -123,14 +115,6 @@ class TodoMutationCommand:
     allow_user_gate_auto_acquire: bool = False
 
 
-@dataclass(frozen=True)
-class LeaseModeGateCommand:
-    action: LeaseAction
-
-
-CoordinationCommand = TodoMutationCommand | LeaseModeGateCommand
-
-
 @dataclass(frozen=True)
 class TransitionPlan:
     outcome: DecisionOutcome
@@ -382,31 +366,9 @@ def ownership_gate_requirement(
     return OwnershipGate(payload["ownership_gate"])
 
 
-def _lease_handoff_rejection(snapshot: CoordinationSnapshot) -> str | None:
-    if snapshot.handoff_mode is HandoffMode.SOFT_CLAIM:
-        return "handoff_mode_forbids_lease"
-    return None
-
-
-def _decide_lease_mode_gate(
-    snapshot: CoordinationSnapshot,
-    command: LeaseModeGateCommand,
-) -> TransitionPlan:
-    if (
-        command.action is not LeaseAction.RELEASE
-        and (rejection := _lease_handoff_rejection(snapshot)) is not None
-    ):
-        return _result(DecisionOutcome.REJECTED, rejection)
-    return _result(
-        DecisionOutcome.APPLY,
-        "lease_mutation_allowed",
-        next_snapshot=snapshot,
-    )
-
-
 def decide(
     snapshot: CoordinationSnapshot,
-    command: CoordinationCommand,
+    command: TodoMutationCommand,
 ) -> TransitionPlan:
     """Evaluate one normalized command without reading or writing state."""
 
@@ -414,6 +376,4 @@ def decide(
         return _result(DecisionOutcome.REJECTED, "invalid_lease_snapshot")
     if isinstance(command, TodoMutationCommand):
         return _typescript_todo_decision(snapshot, command)
-    if isinstance(command, LeaseModeGateCommand):
-        return _decide_lease_mode_gate(snapshot, command)
     raise TypeError(f"unsupported coordination command: {type(command).__name__}")
diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json
index 9ba202987b..1002d59dab 100644
--- a/loopx/semantics/vocabulary_v0.json
+++ b/loopx/semantics/vocabulary_v0.json
@@ -13,7 +13,7 @@
   "formal_model": {
     "schema_version": "loopx_semantic_formal_model_v0",
     "universes": {
-      "vocabularies": "V: registered vocabulary identifiers; Producers(V) ⊆ V is exactly the subset declaring a producers key (including compatibility-only entries with an empty list). Kernel(V) ⊆ Producers(V). Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified.",
+      "vocabularies": "V: registered vocabulary identifiers; Producers(V) ⊆ V is exactly the subset declaring a producers key (including compatibility-only entries with an empty list). Kernel(V) ⊆ Producers(V). Producers(V) contains 6 vocabularies: 5 kernel and 1 outside the kernel tier. The 20 cross_runtime vocabularies outside Producers(V) are unverified.",
       "values": "U(v): ambient runtime values; S(v): registered admitted values",
       "sites": "L: source locations that define, produce, consume, interpret, pass through, project, or persist values",
       "scopes": "Scope: global or bounded_context(context_id); ScopeDeclarations are the forked names the registry declares as bounded contexts",
@@ -73,24 +73,24 @@
     "invariants": [
       {
         "id": "F1_producer_closedness",
-        "statement": "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified. Production outside the scan reach is unverified rather than proven closed.",
+        "statement": "∀v ∈ Producers(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Producers(V) contains 6 vocabularies: 5 kernel and 1 outside the kernel tier. The 20 cross_runtime vocabularies outside Producers(V) are unverified. Production outside the scan reach is unverified rather than proven closed.",
         "enforcement": "m0_5",
         "evidence": "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES reach in loopx/semantics/production.py; check_producers visits only vocabularies that declare producers, and validate_production claims no whole-program closedness; unresolved dynamic sites are reported, not treated as proven safe",
         "domain": {
           "quantifies_over": "vocabularies[producers].producers",
-          "verified": 7,
+          "verified": 6,
           "registered": 26,
           "evidence_bound": "producer_scan_reach"
         }
       },
       {
         "id": "F2_canonical_value_liveness",
-        "statement": "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). Producers(V) contains 7 vocabularies: 6 kernel and 1 outside the kernel tier. The 19 cross_runtime vocabularies outside Producers(V) are unverified. Liveness outside the walked set is not proven.",
+        "statement": "∀v ∈ Producers(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). Producers(V) contains 6 vocabularies: 5 kernel and 1 outside the kernel tier. The 20 cross_runtime vocabularies outside Producers(V) are unverified. Liveness outside the walked set is not proven.",
         "enforcement": "m0_5",
         "evidence": "every value of a vocabulary in Producers(V) has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted",
         "domain": {
           "quantifies_over": "vocabularies[producers].producers",
-          "verified": 7,
+          "verified": 6,
           "registered": 26,
           "evidence_bound": "producer_scan_reach"
         }
@@ -369,44 +369,29 @@
         ]
       }
     },
-    "lease_action": {
-      "meaning": "Authority-core lease mutation verb.",
-      "tier": "kernel",
-      "status": "legacy",
+    "task_lease_lifecycle_operation": {
+      "meaning": "Operation accepted by the shipped native lease lifecycle request decoder; acquisition has its own transaction.",
+      "tier": "cross_runtime",
+      "status": "canonical",
       "owners": {
-        "python": "loopx/control_plane/coordination/authority_core.py::LeaseAction",
-        "typescript": null
+        "python": null,
+        "typescript": "loopx/control_plane/work_items/task_lease_lifecycle_request.ts::TASK_LEASE_LIFECYCLE_OPERATIONS"
       },
       "values": [
-        "acquire",
         "renew",
         "transfer",
-        "release"
+        "release",
+        "terminal_verify",
+        "holder_verify",
+        "fence_close"
       ],
-      "producers": [],
-      "compatibility_only": {
-        "acquire": {
-          "reason": "Retained by the legacy typed LeaseModeGateCommand input interface; current in-repository runtime callers use whole native acquire/renew/transfer/release transactions, not this vocabulary. No persisted use is asserted.",
-          "retirement": "M4: retire the legacy Python lease-mode input interface after caller and migration review."
-        },
-        "renew": {
-          "reason": "Retained by the legacy typed LeaseModeGateCommand input interface; current in-repository runtime callers use whole native acquire/renew/transfer/release transactions, not this vocabulary. No persisted use is asserted.",
-          "retirement": "M4: retire the legacy Python lease-mode input interface after caller and migration review."
-        },
-        "transfer": {
-          "reason": "Retained by the legacy typed LeaseModeGateCommand input interface; current in-repository runtime callers use whole native acquire/renew/transfer/release transactions, not this vocabulary. No persisted use is asserted.",
-          "retirement": "M4: retire the legacy Python lease-mode input interface after caller and migration review."
-        },
-        "release": {
-          "reason": "Retained by the legacy typed LeaseModeGateCommand input interface; current in-repository runtime callers use whole native acquire/renew/transfer/release transactions, not this vocabulary. No persisted use is asserted.",
-          "retirement": "M4: retire the legacy Python lease-mode input interface after caller and migration review."
-        }
-      },
       "value_notes": {
-        "acquire": "Compatibility-only input member; no observed in-repository producer. Preserve the typed caller interface until its M4 retirement review.",
-        "renew": "Compatibility-only input member; no observed in-repository producer. Preserve the typed caller interface until its M4 retirement review.",
-        "transfer": "Compatibility-only input member; no observed in-repository producer. Preserve the typed caller interface until its M4 retirement review.",
-        "release": "Compatibility-only input member; no observed in-repository producer. Preserve the typed caller interface until its M4 retirement review."
+        "renew": "Chosen by native renewal callers to extend an existing holder execution with the expected version.",
+        "transfer": "Chosen by native transfer callers to move an existing holder execution to another eligible owner.",
+        "release": "Chosen by native release callers to retire an existing holder execution; cleanup remains legal after a policy transition.",
+        "terminal_verify": "Chosen by Todo terminal callers to verify the current holder fence before completing or superseding work.",
+        "holder_verify": "Chosen by ownership mutation callers to verify the current holder without performing a lease mutation.",
+        "fence_close": "Chosen by terminal cleanup callers to close the held execution fence after accepted work."
       }
     },
     "effective_action": {
@@ -1038,15 +1023,17 @@
       },
       {
         "name": "task_lease_lifecycle_decision_operation",
-        "superset": "lease_action",
+        "superset": "task_lease_lifecycle_operation",
         "excluded": [
-          "acquire"
+          "terminal_verify",
+          "holder_verify",
+          "fence_close"
         ],
         "owners": {
           "python": null,
           "typescript": "loopx/control_plane/work_items/task_lease_lifecycle_decision.ts::TASK_LEASE_LIFECYCLE_DECISION_OPERATIONS"
         },
-        "note": "TypeScript-only decision operations are the lease verbs minus acquire."
+        "note": "The native mutation decision owner handles renewal, transfer and release. Verification/fence operations remain with the request/transaction owner; acquisition is separate."
       }
     ]
   },
diff --git a/tests/architecture/test_cross_runtime_value_notes.py b/tests/architecture/test_cross_runtime_value_notes.py
index 995b8c9586..52b2e888ff 100644
--- a/tests/architecture/test_cross_runtime_value_notes.py
+++ b/tests/architecture/test_cross_runtime_value_notes.py
@@ -1,10 +1,10 @@
 """Per-value meaning ratchet for the ``cross_runtime`` vocabulary tier.
 
 ``tests/architecture/test_semantic_vocabulary_drift.py`` already requires a
-``value_notes`` entry for every value of the six kernel vocabularies (#4625 for
-the four canonical Turn vocabularies, #4626 for ``effective_action`` and
-``lease_action``). That ratchet stops at the tier boundary, so the 20
-``cross_runtime`` vocabularies could grow a value that no diff ever explains.
+``value_notes`` entry for every value of the live kernel vocabularies (#4625 for
+the four canonical Turn vocabularies, #4626 for ``effective_action``).
+M4 retired the unused Python ``lease_action`` input and registered the live
+native lifecycle request owner; its values carry the same note obligation here.
 
 This file is the same obligation for the other tier, kept separate on purpose:
 the kernel ratchet sits at the end of a file that several open branches already
diff --git a/tests/architecture/test_semantic_production.py b/tests/architecture/test_semantic_production.py
index 6522c04bc0..004d35e88c 100644
--- a/tests/architecture/test_semantic_production.py
+++ b/tests/architecture/test_semantic_production.py
@@ -41,7 +41,7 @@ def test_quota_union_cannot_be_weakened_or_made_ambiguous(mutation):
     if mutation == 'missing':
         registry['relations']['shared_field_names'] = []
     elif mutation == 'widened':
-        registry['relations']['shared_field_names'][0]['slots'][0]['vocabularies'].append('lease_action')
+        registry['relations']['shared_field_names'][0]['slots'][0]['vocabularies'].append('turn_route')
     else:
         registry['vocabularies']['agent_scope_frontier_action']['values'].append('normal_run')
     with pytest.raises(ValueError, match='anchored|disjoint'):
@@ -167,28 +167,6 @@ def defective(value, errors):
         probe_turn_result_input_domain(v)
 
 
-def test_legacy_lease_values_stay_visible_without_claiming_production():
-    import json
-    from loopx.semantics.inventory import load_sources
-    v = json.loads((ROOT / 'loopx/semantics/vocabulary_v0.json').read_text())['vocabularies']['lease_action']
-    assert v['status'] == 'legacy'
-    assert v['producers'] == []
-    assert set(v['compatibility_only']) == {'acquire', 'renew', 'transfer', 'release'}
-    rows = collect_production(ROOT, v, load_sources(ROOT))
-    assert not any(r.values for r in rows)
-    assert validate_production('lease_action', v, rows) == []
-
-
-def test_new_lease_producer_invalidates_compatibility_only_claim():
-    import json
-    from loopx.semantics.inventory import load_sources
-    v = json.loads((ROOT / 'loopx/semantics/vocabulary_v0.json').read_text())['vocabularies']['lease_action']
-    sources = load_sources(ROOT) + [SourceFile('loopx/control_plane/coordination/new_writer.py', '.py',
-        'from .authority_core import LeaseAction\ndef emit():\n return LeaseAction.ACQUIRE\n')]
-    with pytest.raises(ValueError, match='compatibility-only values are produced'):
-        validate_production('lease_action', v, collect_production(ROOT, v, sources))
-
-
 def test_typescript_syntax_failure_reports_only_source_location():
     source = SourceFile('loopx/control_plane/quota/broken.ts', '.ts', 'const secret = "fixture-only";\nfunction invalid( {')
     with pytest.raises(ValueError, match=r'broken.ts:2: invalid TypeScript source') as error:
diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py
index 0bf3574e3d..6ae9f47385 100644
--- a/tests/architecture/test_semantic_vocabulary_drift.py
+++ b/tests/architecture/test_semantic_vocabulary_drift.py
@@ -475,16 +475,9 @@ def test_live_inventory_ignores_missing_or_stale_reports(tmp_path, monkeypatch,
         smoke["check_inventory"](registry, sources + duplicate)
 
 
-@pytest.mark.parametrize('name', ['effective_action', 'lease_action'])
+@pytest.mark.parametrize('name', ['effective_action'])
 def test_remaining_kernel_values_each_carry_a_note(name):
-    """The two kernel vocabularies that are not Turn control flow still need notes.
-
-    ``effective_action`` is the overloaded should-run slot M1 is due to split, so
-    a value here is only legible once the registry says which condition produces
-    it; ``lease_action`` is legacy and every value is compatibility-only, which
-    is exactly the kind of disposition a reader cannot infer from the name. The
-    note is required in the diff that adds a value, not afterwards.
-    """
+    """The should-run slot still needs its producing condition after M4."""
     smoke = runpy.run_path(str(SMOKE))
     vocabulary = smoke['load_registry']()['vocabularies'][name]
     notes = vocabulary.get('value_notes', {})
@@ -581,7 +574,9 @@ def test_generated_domain_accepts_true_kernel_comparison() -> None:
     domain = smoke["ProducerDomain"].from_registry(registry)
     assert domain.kernel < domain.walked
     assert domain.walked - domain.kernel == {"settlement_binding_kind"}
-    assert domain.outside_by_tier == (("cross_runtime", 19),)
+    # M4 preserves the native lifecycle owner and relation, without claiming
+    # its production liveness from the retired Python compatibility-only set.
+    assert domain.outside_by_tier == (("cross_runtime", 20),)
 
 
 def test_canonical_domain_rejects_old_kernel_only_universe() -> None:
@@ -601,12 +596,12 @@ def test_domain_membership_change_requires_regenerated_prose() -> None:
     # even if the independent numeric domain entries were already updated.
     registry["vocabularies"]["settlement_binding_kind"].pop("producers")
     for invariant_id in ("F1_producer_closedness", "F2_canonical_value_liveness"):
-        _invariant(registry, invariant_id)["domain"]["verified"] = 6
+        _invariant(registry, invariant_id)["domain"]["verified"] = 5
     with pytest.raises(smoke["Drift"], match="canonical producer-domain projection"):
         smoke["check_formal_model"](registry["formal_model"], registry)
     projected = smoke["producer_domain_prose"](registry)
-    assert "20 cross_runtime" in projected["F1_producer_closedness.statement"]
-    assert "6 kernel and 0 outside" in projected["universes.vocabularies"]
+    assert "21 cross_runtime" in projected["F1_producer_closedness.statement"]
+    assert "5 kernel and 0 outside" in projected["universes.vocabularies"]
 
 
 @pytest.mark.parametrize("invariant_id", sorted({
@@ -942,3 +937,48 @@ def test_every_executed_projection_must_be_registered() -> None:
     del registry["projections"]["turn_route_to_loop_disposition"]
     with pytest.raises(smoke["Drift"], match="is not registered"):
         smoke["check_projections"](registry)
+
+
+@pytest.mark.parametrize('symbol', ['LeaseAction', 'LeaseModeGateCommand', 'CoordinationCommand'])
+@pytest.mark.parametrize('form', ['definition', 'absolute_import', 'relative_import'])
+def test_retired_lease_input_cannot_regrow_a_definition_or_producer(symbol, form):
+    smoke = runpy.run_path(str(SMOKE))
+    owner = 'loopx/control_plane/coordination/authority_core.py'
+    if form == 'definition':
+        text = f'{symbol} = object\n' if symbol == 'CoordinationCommand' else f'class {symbol}:\n pass\n'
+        source = smoke['SourceFile'](owner, '.py', text)
+    else:
+        module = 'loopx.control_plane.coordination.authority_core' if form == 'absolute_import' else '.authority_core'
+        text = f'from {module} import {symbol} as Restored\ndef emit():\n return Restored\n'
+        source = smoke['SourceFile']('loopx/control_plane/coordination/new_writer.py', '.py', text)
+    with pytest.raises(smoke['Drift'], match='retired lease input'):
+        smoke['check_retired_lease_input'](smoke['load_registry'](), [source])
+
+
+def test_retired_lease_registry_entry_cannot_return_as_fake_compatibility():
+    smoke = runpy.run_path(str(SMOKE))
+    registry = copy.deepcopy(smoke['load_registry']())
+    registry['vocabularies']['lease_action'] = {'producers': [], 'compatibility_only': {}}
+    with pytest.raises(smoke['Drift'], match='retired lease input'):
+        smoke['check_retired_lease_input'](registry, [])
+
+
+def test_native_lifecycle_relation_keeps_the_live_owner_and_verification_boundary():
+    smoke = runpy.run_path(str(SMOKE))
+    registry = smoke['load_registry']()
+    assert registry['coverage_floor']['vocabularies'] == 26
+    assert registry['coverage_floor']['owner_symbols'] == 51
+    assert registry['coverage_floor']['relations'] == 9
+    relation = next(row for row in registry['relations']['subsets']
+                    if row['name'] == 'task_lease_lifecycle_decision_operation')
+    assert relation['superset'] == 'task_lease_lifecycle_operation'
+    assert set(relation['excluded']) == {'terminal_verify', 'holder_verify', 'fence_close'}
+    smoke['check_relations'](registry)
+    mutated = copy.deepcopy(registry)
+    mutated['relations']['subsets'][-1]['excluded'] = ['holder_verify', 'fence_close']
+    with pytest.raises(smoke['Drift'], match='drifted from the registry'):
+        smoke['check_relations'](mutated)
+    mutated = copy.deepcopy(registry)
+    mutated['vocabularies']['task_lease_lifecycle_operation']['owners']['typescript'] = None
+    with pytest.raises(smoke['Drift'], match='actual owner'):
+        smoke['check_retired_lease_input'](mutated, [])
diff --git a/tests/control_plane/test_coordination_authority_core.py b/tests/control_plane/test_coordination_authority_core.py
index 3a8ee49f6e..409a74d913 100644
--- a/tests/control_plane/test_coordination_authority_core.py
+++ b/tests/control_plane/test_coordination_authority_core.py
@@ -8,9 +8,7 @@
     CoordinationSnapshot,
     DecisionOutcome,
     HandoffMode,
-    LeaseAction,
     LeaseFence,
-    LeaseModeGateCommand,
     LeaseSnapshot,
     LifecycleGrant,
     OwnershipGate,
@@ -357,15 +355,19 @@ def test_exact_user_gate_can_plan_auto_acquire_but_never_displaces_a_live_lease(
     assert foreign_live.code == "lease_fence_required"
 
 
-def test_mode_gate_is_explicit_instead_of_a_synthetic_lease_command() -> None:
-    state = snapshot(handoff_mode=HandoffMode.SOFT_CLAIM)
-    for action in (LeaseAction.ACQUIRE, LeaseAction.RENEW, LeaseAction.TRANSFER):
-        plan = decide(state, LeaseModeGateCommand(action=action))
-        assert plan.outcome is DecisionOutcome.REJECTED
-        assert plan.code == "handoff_mode_forbids_lease"
+@pytest.mark.parametrize("symbol", ["LeaseAction", "LeaseModeGateCommand", "CoordinationCommand"])
+def test_retired_private_lease_input_is_absent(symbol) -> None:
+    import importlib
 
-    release = decide(state, LeaseModeGateCommand(action=LeaseAction.RELEASE))
-    assert release.outcome is DecisionOutcome.APPLY
+    module = "loopx.control_plane.coordination.authority_core"
+    assert not hasattr(importlib.import_module(module), symbol)
+    with pytest.raises(ImportError):
+        exec(f"from {module} import {symbol}")
+
+
+def test_todo_bridge_rejects_commands_outside_its_live_boundary() -> None:
+    with pytest.raises(TypeError, match="unsupported coordination command"):
+        decide(snapshot(), object())
 
 
 def test_core_has_no_storage_or_receipt_version_domain() -> None: