refactor(coordination): retire unused Python lease mode input

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,

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 已验收。

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.
 

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 仍未完成。

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.

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")
     )

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,38 +366,14 @@ 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."""
 
     if _invalid_lease_snapshot(snapshot.lease):
         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__}")