diff --git a/docs/adr/0005-lesson-as-ordered-composition-of-typed-elements.md b/docs/adr/0005-lesson-as-ordered-composition-of-typed-elements.md
new file mode 100644
index 0000000..5cb5756
--- /dev/null
+++ b/docs/adr/0005-lesson-as-ordered-composition-of-typed-elements.md
@@ -0,0 +1,131 @@
+# ADR 0005: Lesson Is An Ordered Composition Of Typed Elements
+
+## Status
+
+Accepted — for the skeleton decisions below. Several sub-decisions are
+deliberately left open; see *Open Questions / Deferred*.
+
+This is the first ADR describing the **product core** (the curriculum
+"engineering file"). ADR 0001–0004 cover only the platform side (Feishu group,
+AgentRun, lock, permissions, on-demand context).
+
+## Context
+
+We are building a digitalization solution for curriculum production. The central
+artifact is a structured "engineering file" for a course — edited with the help
+of a coding agent, validated by a compiler-like rule-based checker that emits
+helpful fix hints. The domain is new; we do not assume LLM pretraining priors
+about its shape. This ADR fixes the shape of that engineering file so that the
+developer and the agent stop making divergent assumptions about it.
+
+What the file is *not*: it is not presentation. The same content drives multiple
+export targets (student handout, teacher lesson plan, PPT, third-party platform
+archive, an HTML interactive-courseware platform). The engineering file is the
+target-agnostic content master; typst, markdown dialects, etc. are downstream.
+
+## Decision
+
+### Granularity: the engineering file is one lesson
+
+One engineering file = one single lesson. A course / unit is *not* an
+engineering file; it is an arrangement (编排) of lessons, modeled elsewhere (see
+*Deferred*).
+
+### A lesson is an ordered sequence of element instances
+
+A lesson is an **ordered** sequence of elements. Order is significant; duration
+is **not** modeled (the file is content-oriented, like a lecture note / handout
+/ slide content flow, not a time-driven timeline). Content is formula-heavy.
+
+### An element instance = a kind tag + data conforming to that kind's schema
+
+Every element carries a **kind** tag plus **data** that conforms to that kind's
+schema. Examples of kinds: worked example (例题), theorem/lemma (定理),
+exposition (讲述/阐述).
+
+### Element kinds form an open, extensible universe
+
+Element kinds are **not** a closed enumeration. They form an open universe — like
+a language standard library: the framework ships a good set of defaults (stdlib),
+and (longer-term) third parties may contribute kinds (like crates). The model
+must therefore never encode kinds as a fixed/closed type.
+
+### A kind's minimal contract to the framework is its data schema only
+
+The single thing a kind must declare to the framework is its **data schema**.
+Rendering is explicitly **not** part of the kind contract.
+
+### Export targets project/render the lesson
+
+An export target (student handout, teacher plan, PPT, third-party archive, HTML
+courseware platform, …) is a projection/rendering of the one lesson. One lesson
+feeds many targets.
+
+### Rendering is a per-(kind, target) configuration matrix that lives in the file
+
+How a given kind appears in a given target is a **configuration matrix**
+indexed by (kind, target). This matrix lives **inside the engineering file**;
+the framework provides good **defaults**, and the file may **override** them.
+(This corresponds to the prototype's `exports/{target}.typ`.)
+
+When a lesson uses a kind for which the current target has **no** render rule,
+the checker emits a **WARNING** (the element is ignored for that target) — **not
+an error**. Missing rendering does not block.
+
+### Target-specific information splits into two categories (a / b)
+
+- **(a) semantic-but-target-specific** — information that genuinely belongs to an
+  element's meaning and only *surfaces* in some targets (e.g. a verbatim script
+  本质上是某 exposition 的口播版本, shown only in the teacher plan; key-point
+  highlighting shown only in the student handout). This **moves up onto the
+  element** as nullable fields.
+- **(b) medium-only** — information that exists only because of a target's medium
+  (HTML interactive behavior, build script, npm dependencies). This does **not**
+  go on the element; it belongs to the target / external artifacts.
+
+### Interactive courseware is an inline heavyweight element
+
+A clickable "teaching apparatus" (教具) that a student plays with on the HTML
+platform is an **inline element** in the content flow (bound to this lesson),
+**not** a whole-lesson render target and **not** (for now) an externally
+referenced artifact. In the model it carries only the apparatus's **problem /
+configuration data**; the heavy implementation (e.g. an npm package such as a
+KenKen-Sudoku renderer) lives **outside** this model, and reuse of such
+implementations is out of scope for this model.
+
+### Typst is a rendering backend, not the definition language
+
+Typst is one rendering backend among several. It is **not** the language in
+which kinds, schemas, or rules are defined (typst's typing is too weak for the
+upper-layer design we want).
+
+## Consequences
+
+- Because kinds are an open universe, the formal model must be parameterized over
+  kinds — no closed `inductive`/enum of element kinds anywhere.
+- Because missing rendering is a warning, not an error, a lesson stays valid and
+  exportable even when some (kind, target) pair has no rule yet.
+- Because the content master is decoupled from presentation, the same lesson
+  projects to many targets; adding a target does not change the lesson.
+- Because a kind's contract is "schema only", rendering and kind-definition can
+  evolve independently of the kind set.
+- The checker (the thing that will "stand in Lean's position" at product runtime)
+  gets its first concrete rule from this ADR: *used-kind-with-no-render-rule ⇒
+  warning*.
+
+## Open Questions / Deferred
+
+Deliberately unspecified. Neither developer nor agent should assume a resolution;
+surface them when they become relevant rather than picking one.
+
+- **Schema representation** — how a kind's data schema is itself expressed (the
+  schema language).
+- **Kind-definition mechanism** — the language/mechanism used to define an element
+  kind (typst scripting is rejected; the replacement is TBD).
+- **Render-rule payload** — the concrete representation of a render rule.
+- **Full lesson legality** — the complete definition of a "legal lesson"; this ADR
+  fixes only the one seed rule (missing render rule ⇒ warning).
+- **Question bank (题库)** — its relationship to elements (reference vs inline) is
+  undecided; a pure-reference model may not be adequate.
+- **Course = arrangement of lessons** — the concrete rules for composing lessons
+  into a course.
diff --git a/spec/Spec.lean b/spec/Spec.lean
index 9cdeec1..9f7d538 100644
--- a/spec/Spec.lean
+++ b/spec/Spec.lean
@@ -1,3 +1,3 @@
 -- This module serves as the root of the `Spec` library.
 -- Import modules here that should be built as part of the library.
-import Spec.Basic
+import Spec.Courseware
diff --git a/spec/Spec/Basic.lean b/spec/Spec/Basic.lean
deleted file mode 100644
index 99415d9..0000000
--- a/spec/Spec/Basic.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
diff --git a/spec/Spec/Courseware.lean b/spec/Spec/Courseware.lean
new file mode 100644
index 0000000..866e466
--- /dev/null
+++ b/spec/Spec/Courseware.lean
@@ -0,0 +1,9 @@
+import Spec.Courseware.Lesson
+
+/-!
+# Courseware —— 产品层契约(课程工程文件)
+
+本层是护城河:课程"工程文件"的语义母本与合法性规则。当前只有 lesson 骨架
+(见 `Spec.Courseware.Lesson`,ADR-0005);题库、course 编排、完整合法性判定
+等仍 `OPEN`,待各自 ADR 落定后逐个加入。
+-/
diff --git a/spec/Spec/Courseware/Lesson.lean b/spec/Spec/Courseware/Lesson.lean
new file mode 100644
index 0000000..99d2330
--- /dev/null
+++ b/spec/Spec/Courseware/Lesson.lean
@@ -0,0 +1,115 @@
+/-!
+# Lesson —— 课程工程文件的母本模型(单节课)
+
+本文件固定 ADR-0005 的骨架共识:一个**工程文件 = 一节课(lesson)**,
+lesson 是**有类型 element 实例的有序序列**;element 实例 = kind 标签 + 符合该
+kind schema 的数据;export target 是对 lesson 的投影;渲染由一份
+**(kind × target) 配置矩阵**承载。
+
+本轮**只承诺关系结构**。所有尚未决定的基元(schema 怎么表示、kind 怎么定义、
+render rule 的载荷长什么样)都收口进 `Primitives`,以抽象类型留白(`OPEN`),
+契约因此对未定之物**零承诺**,同时仍 type-check 通过。完整的"合法 lesson"判定
+亦未定;本轮只落 checker 的第一颗种子(缺渲染 ⇒ warning)。
+-/
+
+namespace Spec.Courseware
+
+/--
+契约基元载体(`PINNED` 关系结构 / `OPEN` 基元留白,`ADR-0005`)。
+
+把本轮**尚未决定**的基元收口到一处,使 lesson 模型在其上参数化。每个字段都是
+一个 `OPEN` 点:契约只声明它**存在**、以及它在关系中扮演的角色,绝不假设其内部
+表示。具体表示待后续各自的 ADR 落定后再 refine。
+-/
+structure Primitives where
+  /--
+  element 的**种类标识**(`PINNED` 开放宇宙 / `OPEN` 表示,`ADR-0005`)。
+
+  kind 构成一个**开放、可扩展的宇宙**(stdlib default + 远期第三方),因此**刻意
+  用一个抽象类型,而非封闭 `inductive`/枚举**——把"kind 集合不封闭"这条 PINNED
+  直接编码进类型。`KindId` 的具体表示是 `OPEN`。
+  -/
+  KindId : Type
+  /--
+  某 kind 的**合法数据**类型(`PINNED` 依赖关系 / `OPEN` schema 表示,`ADR-0005`)。
+
+  以 `KindId` 为索引的**依赖类型**,精确表达"element 数据必须**符合该 kind 的
+  schema**":不同 kind 的合法数据类型不同。kind 对框架的最小契约**就是**这份
+  schema(渲染不在其中)。schema 自身**怎么表示**是 `OPEN`,故此处只给出
+  `KindId → Type` 这一依赖,不触碰其内部。
+  -/
+  ElementData : KindId → Type
+  /--
+  **导出目标标识**(`PINNED` 角色 / `OPEN` 表示,`ADR-0005`)。
+
+  一个 target(学生讲义 / 教师教案 / PPT / 第三方平台 archive / html 教具平台…)
+  是对同一 lesson 的一种投影。target 同样是开放集合;其具体表示 `OPEN`。
+  -/
+  TargetId : Type
+  /--
+  **渲染规则的载荷**(`OPEN` 表示,`ADR-0005`)。
+
+  "某 kind 在某 target 下如何呈现"的那条规则的**内容**。其表示完全 `OPEN`(typst
+  只是渲染后端之一,不是定义语言)——本轮只关心规则**在不在**(见 `RenderConfig`),
+  不关心它**是什么**。
+  -/
+  RenderRule : Type
+
+variable (P : Primitives)
+
+/--
+**element 实例**:一个 kind 标签 + 符合该 kind schema 的数据(`PINNED`,`ADR-0005`)。
+
+`data` 的类型由 `kind` 决定(`P.ElementData kind`),从类型上保证"数据符合该 kind
+的 schema"——构造一个 `Element` 时不可能给出与其 kind 不匹配的数据。
+
+注:ADR-0005 的 (a) 类信息(逐字稿、重点圈划等"语义性但 target-specific"的字段)
+属于具体 kind 的 schema 范畴,故落在 `P.ElementData` 内,不在此通用结构上出现;
+(b) 类信息(html 交互、build/npm)不进 element。
+-/
+structure Element where
+  /-- 该 element 的种类(`PINNED`,`ADR-0005`)。 -/
+  kind : P.KindId
+  /-- 符合 `kind` schema 的数据(`PINNED`,`ADR-0005`)。 -/
+  data : P.ElementData kind
+
+/--
+**lesson = element 实例的有序序列**(`PINNED`,`ADR-0005`)。
+
+用 `List` 编码"有序":**次序是有意义的**。**时长不建模**——lesson 是内容编排
+(讲义/PPT 式的内容流),不是时间轴。课程/单元不是 lesson,而是 lesson 的编排
+(`OPEN`,见 ADR-0005 Deferred),不在本文件。
+-/
+abbrev Lesson := List (Element P)
+
+/--
+**渲染配置矩阵**:(kind × target) → 可选的渲染规则(`PINNED`,`ADR-0005`)。
+
+这份矩阵**住在工程文件里**:框架给好 default,文件可逐项 override。`rule k t = none`
+表示该 (kind, target) 对**尚无渲染规则**(此处只建模规则的**有无**,不建模其内容)。
+-/
+structure RenderConfig where
+  /-- (kind, target) ↦ 该对是否配了渲染规则及其载荷(`PINNED`,`ADR-0005`)。 -/
+  rule : P.KindId → P.TargetId → Option P.RenderRule
+
+/--
+kind `k` 在 target `t` 下**已配渲染规则**(`PINNED`,`ADR-0005`)。
+
+即矩阵在该 (kind, target) 处非空。"覆盖"= 有规则可用;`covers` 为假即"缺渲染"。
+-/
+def RenderConfig.covers {P : Primitives} (c : RenderConfig P) (k : P.KindId) (t : P.TargetId) : Prop :=
+  (c.rule k t).isSome
+
+/--
+**checker 种子规则**:lesson 在 target `t` 下**存在被忽略的 element**(`PINNED`,`ADR-0005`)。
+
+成立 ⟺ lesson 里**存在**某 element,其 kind 在 `t` 下没有渲染规则。
+
+ADR-0005 PIN 住该情形的**严重级别 = warning,而非 error**:它**不阻断**导出,只提示
+"这些 element 在该 target 下被忽略了"。这是 checker(产品里"站在 Lean 位置"的那个
+东西)的第一颗诊断种子;完整的"合法 lesson"判定仍 `OPEN`。
+-/
+def WarnsIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
+  ∃ e ∈ l, ¬ c.covers e.kind t
+
+end Spec.Courseware