feat(spec): add three-tier subject hierarchy and org role lattice

- Hierarchy.lean: Platform/Organization/User struct, 三层主体层级
- User.lean: FeishuProfile, 飞书身份是绑定不是本体
- User struct: id/displayName/passwordHash/feishu
- Organization.lean: OrganizationRole(owner/admin/member) + 成员管理规则
- Prelude.lean: UserId/FeishuOpenId/FeishuConnectionId

实现偏离: spec 钉 User 为独立实体, 实现 User.id 由飞书身份派生

lake build 35/35 全绿

spec/Spec/Prelude.lean

@@ -15,6 +15,12 @@ structure Identifiers where
   ProjectId : Type
   /-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
   OrganizationId : Type
+  /-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
+  UserId : Type
+  /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  FeishuOpenId : Type
+  /-- 组织飞书应用连接标识(`OPEN` 表示;org-scoped)。 -/
+  FeishuConnectionId : Type
   /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
   TeamId : Type
   /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/

spec/Spec/System.lean

@@ -1,5 +1,7 @@
+import Spec.System.Hierarchy
 import Spec.System.ProjectGroup
 import Spec.System.Organization
+import Spec.System.User
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
 import Spec.System.PlatformAdministration
@@ -17,9 +19,12 @@ import Spec.System.Audit
 (`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
 **语义分歧点**:
 
+- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
+- `User` —— 飞书绑定:登录途径,不是用户本体。
 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
 - `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
-  connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024)。
+  connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024);组织级角色格
+  owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
   (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和

spec/Spec/System/Hierarchy.lean

@@ -0,0 +1,50 @@
+import Spec.Prelude
+import Spec.System.User
+
+/-!
+# Hierarchy —— 主体层级
+
+整个服务中的主体: 平台 → 组织(租户)→ 用户。
+
+- **平台**(Platform): SaaS 提供方实体
+
+- **组织**(Organization): SaaS 租户
+
+- **用户**(User): 租户内的独立实体
+
+**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 平台(`PINNED`, SaaS 提供方实体)。平台只有一个，独立于组织（租户）。平台管理
+身份、会话、审计、紧急恢复等由 `PlatformAdministration`(ADR-0023)定义;本 struct 只
+锚定平台在层级中的位置及其飞书应用归属。平台管理员不复用 `User` 或 org membership。 -/
+structure Platform where
+  /-- 平台自有的飞书应用(`PINNED`, ADR-0023),用于平台管理员认证;与各 org 客户应用分离。 -/
+  application : I.PlatformFeishuApplicationId
+
+/-- 组织(`PINNED`, 租户根, ADR-0020)。每个 project/team 必须归属且仅归属一个组织。
+组织级角色格(owner/admin/member)、tenancy 关系、provider connection 凭据模式详见
+`Spec.System.Organization`。 -/
+structure Organization where
+  /-- 组织标识(`OPEN` 表示,ADR-0020 tenant root)。 -/
+  id : I.OrganizationId
+
+/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织(结构钉死)。飞书身份是绑定
+不是本体,详见 `Spec.System.User`。 -/
+structure User where
+  /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
+  id : I.UserId
+  /-- 所属组织(`PINNED`, ADR-0020)。 -/
+  organization : I.OrganizationId
+  /-- 显示名(`PINNED`, 可改)。 -/
+  displayName : String
+  /-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
+  passwordHash : String
+  /-- 飞书绑定(`PINNED`, 可选)。 -/
+  feishu : Option (FeishuProfile I)
+
+end Spec.System

spec/Spec/System/Organization.lean

@@ -3,16 +3,9 @@ import Spec.Prelude
 /-!
 # Organization —— SaaS tenant root (ADR-0020, ADR-0024)
 
-ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
+组织是租户根。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
-`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
+组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
-必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
+`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。
-不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
-
-本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
-不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
-provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
-`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
-writer authority 与 fail-closed resolver 由 ADR-0024 固定。
 -/
 
 namespace Spec.System
@@ -51,9 +44,8 @@ def TeamProjectGrantScope.WellScoped
     (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
   ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
 
-/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
+/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
-管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
+跨 org 共用 process-global key。模式切换 `OPEN`。 -/
-都不允许无关 org 共用 process-global provider key。模式切换过程仍为 `OPEN`。 -/
 inductive ProviderCredentialMode where
   | byok
   | platformManaged
@@ -104,4 +96,34 @@ def OrganizationSecretResolvable
   organizationActive && connectionActive &&
     (binding.organization == requestedOrganization) && authenticatedEnvelope
 
+
+/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
+inductive OrganizationRole where
+  /-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
+  | owner
+  /-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
+  | admin
+  /-- 组织成员(`PINNED`):普通成员。 -/
+  | member
+
+/-- 组织成员关系(`PINNED`)。 -/
+structure OrganizationMembership where
+  /-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
+  user : I.UserId
+  /-- 组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 角色(`PINNED`)。 -/
+  role : OrganizationRole
+
+/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
+def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
+  actorRole = .owner
+
+/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
+def LastOwnerProtected
+    (target : OrganizationMembership I)
+    (otherOwnersInOrg : List I.UserId) : Prop :=
+  target.role ≠ .owner ∨
+    ∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
+
 end Spec.System

spec/Spec/System/User.lean

@@ -0,0 +1,25 @@
+import Spec.Prelude
+
+/-!
+# User —— 飞书绑定
+
+飞书身份是用户的绑定(登录途径),不是用户本体。用户实体见 `Hierarchy.User`。
+用户创建当前只钉管理员直接创建;飞书自助注册→管理员审批未钉死(`OPEN`)。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 飞书用户信息(`PINNED`)。User 上的可选飞书绑定载荷。 -/
+structure FeishuProfile where
+  /-- 飞书 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  openId : I.FeishuOpenId
+  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped,不可跨 org)。 -/
+  connection : I.FeishuConnectionId
+  /-- 飞书显示名(`OPEN`;是否预填 displayName 未定)。 -/
+  name : Option String
+  /-- 飞书头像 URL(`OPEN`)。 -/
+  avatarUrl : Option String
+
+end Spec.System