From e17e03823233ece8f747b7a486dfff8fb5b625d8 Mon Sep 17 00:00:00 2001
From: sjfhsjfh <sjfhsjfh@qq.com>
Date: Sun, 12 Jul 2026 09:26:13 +0800
Subject: [PATCH] feat(spec): add FeishuUserId to FeishuProfile
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

飞书 user_id 是租户内身份,换应用不变;open_id 是应用内身份,换应用即变。
两者都存:user_id 更稳定,open_id 是 API 调用句柄。
---
 spec/Spec/Prelude.lean     | 2 ++
 spec/Spec/System/User.lean | 8 +++++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/spec/Spec/Prelude.lean b/spec/Spec/Prelude.lean
index 8b00fa8..5c5323f 100644
--- a/spec/Spec/Prelude.lean
+++ b/spec/Spec/Prelude.lean
@@ -19,6 +19,8 @@ structure Identifiers where
   UserId : Type
   /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
   FeishuOpenId : Type
+  /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
+  FeishuUserId : Type
   /-- 组织飞书应用连接标识(`OPEN` 表示;org-scoped)。 -/
   FeishuConnectionId : Type
   /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
diff --git a/spec/Spec/System/User.lean b/spec/Spec/System/User.lean
index c0819a4..127fcaa 100644
--- a/spec/Spec/System/User.lean
+++ b/spec/Spec/System/User.lean
@@ -13,11 +13,13 @@ variable (I : Identifiers)
 
 /-- 飞书用户信息(`PINNED`)。User 上的可选飞书绑定载荷。 -/
 structure FeishuProfile where
-  /-- 飞书 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  /-- 应用内身份(`OPEN` 表示);调飞书 API 的直接句柄,换应用即变。 -/
   openId : I.FeishuOpenId
-  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped,不可跨 org)。 -/
+  /-- 租户内身份(`OPEN` 表示);换应用不变,比 open_id 稳定。 -/
+  userId : I.FeishuUserId
+  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped)。 -/
   connection : I.FeishuConnectionId
-  /-- 飞书显示名(`OPEN`;是否预填 displayName 未定)。 -/
+  /-- 飞书显示名(`OPEN`)。 -/
   name : Option String
   /-- 飞书头像 URL(`OPEN`)。 -/
   avatarUrl : Option String