feat(spec): add lesson model contract (ADR-0005)

First product-core concept in the semantic master spec: a curriculum
engineering file is one lesson, modeled as an ordered sequence of typed
element instances over an open kind universe.

- docs/adr/0005: lesson model decision narrative + deferred OPEN items
- spec/Spec/Courseware/Lesson.lean: Primitives carrier (KindId/ElementData/
  TargetId/RenderRule kept abstract), Element, Lesson, RenderConfig, and the
  first checker seed (WarnsIgnored: used-kind-with-no-render-rule => warning)
- wire Spec.lean -> Spec.Courseware; drop placeholder Basic.lean

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

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.