feat: add organization tenant model

spec/Spec/Prelude.lean

@@ -13,6 +13,10 @@ namespace Spec.System
 structure Identifiers where
   /-- 课程项目标识(`OPEN` 表示;聚合根,likec4 `Project`)。 -/
   ProjectId : Type
+  /-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
+  OrganizationId : Type
+  /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
+  TeamId : Type
   /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
   ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
   RunId : Type

spec/Spec/System.lean

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

spec/Spec/System/Organization.lean

@@ -0,0 +1,51 @@
+import Spec.Prelude
+
+/-!
+# Organization —— SaaS tenant root (ADR-0020)
+
+ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
+`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
+必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
+不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
+
+本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
+不得跨 org。用户身份、外部目录 provider 细节、平台控制面角色集合仍为 `OPEN`。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 课程项目的租户归属(`PINNED`, ADR-0020):每个 project 必须有一个 organization。 -/
+structure ProjectTenancy where
+  /-- 被归属的课程项目(`PINNED`, ADR-0020)。 -/
+  project : I.ProjectId
+  /-- project 所属 organization(`PINNED`, ADR-0020)。 -/
+  organization : I.OrganizationId
+
+/-- Hub team 的租户归属(`PINNED`, ADR-0020):team 是 org-scoped principal。 -/
+structure TeamTenancy where
+  /-- 被归属的 Hub team(`PINNED`, ADR-0020)。 -/
+  team : I.TeamId
+  /-- team 所属 organization(`PINNED`, ADR-0020)。 -/
+  organization : I.OrganizationId
+
+/-- Team 对 project 的授权作用域(`PINNED`, ADR-0020):`PermissionGrant` 可以把
+TEAM principal 授给 PROJECT resource,但该 grant 必须同 org。role 本身仍由
+`PermissionGrant`/`Permission` 定义,这里仅刻画 tenant well-scopedness。 -/
+structure TeamProjectGrantScope where
+  /-- 被授权的 project(`PINNED`, ADR-0020)。 -/
+  project : I.ProjectId
+  /-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
+  team : I.TeamId
+
+/-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
+(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);本谓词钉死
+跨 org team grant 必须被拒绝。 -/
+def TeamProjectGrantScope.WellScoped
+    (grant : TeamProjectGrantScope I)
+    (projectOrg : I.ProjectId → Option I.OrganizationId)
+    (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
+  ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
+
+end Spec.System

spec/Spec/System/PermissionGrant.lean

@@ -12,7 +12,8 @@ ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`
 principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
 层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
 ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
-须 surface,不得默认。
+须 surface,不得默认。ADR-0020 另行钉死 TEAM principal 授权 PROJECT resource 时必须
+同 organization;该 tenant well-scopedness 见 `Spec.System.Organization`。
 -/
 
 namespace Spec.System