feat: add org admin project onboarding foundation

spec/Spec/Prelude.lean

@@ -17,6 +17,8 @@ structure Identifiers where
   OrganizationId : Type
   /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
   TeamId : Type
+  /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/
+  FolderId : Type
   /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
   ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
   RunId : Type

spec/Spec/System.lean

@@ -1,5 +1,6 @@
 import Spec.System.ProjectGroup
 import Spec.System.Organization
+import Spec.System.ProjectWorkspace
 import Spec.System.Run
 import Spec.System.Lock
 import Spec.System.Memory
@@ -16,6 +17,8 @@ import Spec.System.Audit
 
 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
 - `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org。
+- `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
+  (ADR-0021)。
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
 - `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
@@ -26,5 +29,5 @@ import Spec.System.Audit
   (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
 - `Audit` —— 有意从简(内容多为 plumbing,OPEN)。
 
-标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020。
+标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020, 0021。
 -/

spec/Spec/System/ProjectGroup.lean

@@ -6,14 +6,12 @@ import Spec.Prelude
 ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
 owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
 处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
-project↔group 的一对一绑定——likec4 画得出"project has group",画不出"恰好一个、且群
-不持锁"。
+project↔group 的**active**一对一绑定——likec4 画得出"project has group",画不出"恰好一个、
+且群不持锁"。
 
-**群失效态与绑定快照(`OPEN`, ADR-0001 Consequences):** 群解散/归档/不可达时,
-`GroupBinding` 快照应变为 `none`(解绑、允许 rebind)还是保持 `some` 但指向失效 chat
-(悬挂、待管理员干预)未决策。ADR-0001 已点名 "rebinding or group archival needs
-explicit product rules";本模块只刻画健康态 1:1 不变式,不臆造失效态语义。实现遇到
-群解散必须 surface,不得默认任一方。
+**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可以保留 archived
+historical binding rows 供审计/纠错,但 `GroupBinding` 谓词只刻画当前 active 快照。
+群解散/不可达的自动化处理仍为 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
 -/
 
 namespace Spec.System
@@ -27,13 +25,14 @@ structure ProjectGroup where
   group";chat 标识见 `Identifiers.ChatId`)。 -/
   chat : I.ChatId
 
-/-- 项目↔群绑定表(`PINNED` 每项目至多一个群, ADR-0001)。`ProjectId → Option ChatId` 的
-结构本身即"一个 project 至多绑一个群"(由 `Option` 自带);良构补另一半——单射。 -/
+/-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
+`ProjectId → Option ChatId` 的结构本身即"一个 project 至多绑一个 active 群"(由 `Option`
+自带);良构补另一半——单射。 -/
 def GroupBinding := I.ProjectId → Option I.ChatId
 
-/-- 绑定良构:**单射**——不同 project 不绑同一 chat(`PINNED` 1:1 的另一半, ADR-0001)。
-"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个 project"。群
-rebinding/archival 是生命周期事件(ADR-0001 Consequences),不在本快照不变式内。 -/
+/-- Active 绑定良构:**单射**——不同 project 不绑同一 active chat(`PINNED` 1:1 的另一半,
+ADR-0001/0021)。"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个
+project"。archived historical bindings 不在本快照不变式内。 -/
 def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
   ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
 

spec/Spec/System/ProjectWorkspace.lean

@@ -0,0 +1,54 @@
+import Spec.Prelude
+
+/-!
+# ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)
+
+ADR-0021 把 org 后台里的"文件管理器式"项目管理收口为透明 folder + project:
+folder 只负责导航、排序、层级与用量聚合,当前不是权限资源。project 仍是授权边界。
+
+本模块只钉死会影响实现分歧的不变量:folder/project 同 org、folder 不参与权限、普通成员
+从飞书群创建 project 必须受 org policy 控制。folder visibility/team policy/继承授权仍为
+未来扩展,不得在当前实现中半隐式加入。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- Project explorer folder 的租户归属(`PINNED`, ADR-0021):folder 是 org 内透明节点。 -/
+structure FolderTenancy where
+  /-- 被归属的 folder(`PINNED`, ADR-0021)。 -/
+  folder : I.FolderId
+  /-- folder 所属 organization(`PINNED`, ADR-0021)。 -/
+  organization : I.OrganizationId
+
+/-- Project 放入 folder 的作用域(`PINNED`, ADR-0021):project 可以位于某个 folder,
+但二者必须同 org。folder 不改变 project 权限。 -/
+structure ProjectFolderPlacement where
+  /-- 被放置的 project(`PINNED`, ADR-0021)。 -/
+  project : I.ProjectId
+  /-- project 所在 folder(`PINNED`, ADR-0021)。 -/
+  folder : I.FolderId
+
+/-- Project-folder placement 是良构的 iff project 与 folder 解析到同一 organization
+(`PINNED`, ADR-0021)。 -/
+def ProjectFolderPlacement.WellScoped
+    (placement : ProjectFolderPlacement I)
+    (projectOrg : I.ProjectId → Option I.OrganizationId)
+    (folderOrg : I.FolderId → Option I.OrganizationId) : Prop :=
+  ∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o
+
+/-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
+不改变 project 自身授权。未来 folder policy 若出现,必须新增显式语义而不是复用本谓词。 -/
+structure FolderTransparent where
+  /-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
+  current : True
+
+/-- 普通 org member 是否可从 Feishu 群自助创建 project 的 org policy(`PINNED`, ADR-0021)。 -/
+structure MemberProjectCreationPolicy where
+  /-- policy 所属 organization(`PINNED`, ADR-0021)。 -/
+  organization : I.OrganizationId
+  /-- 为 true 时普通成员可从未绑定飞书群创建 project;owner/admin 可走后台入口。 -/
+  membersCanCreateProjects : Bool
+
+end Spec.System