Mnehmos · Jul 21, 2026 · Jul 21, 2026 · Jul 21, 2026
@@ -0,0 +1,55 @@
+# ADR-0010: Learning units are version-bound records with controlled review
+
+Date: 2026-07-21
+
+Status: accepted
+
+## Context
+
+Pedagogy in MathOS must be machine-readable, grounded in canonical mathematics, and safe to project into future training data. Free-form generated prose cannot establish its own source, license, review, or eligibility. A mutable lesson would also make it impossible to tell which explanation, exercise, or misconception a curriculum edge actually reviewed.
+
+The existing canonical store already provides immutable record versions, exact graph endpoints, content-addressed artifacts, compare-and-swap heads, actor attribution, idempotency, deterministic traversal, and hard-prerequisite cycle rejection. Pedagogy should use those mechanisms instead of adding a second store or authority model.
+
+## Decision
+
+MathOS defines a closed Rust-owned `learning_unit/1` payload and matching committed JSON Schema. Every unit records one exact current claim or concept target, audience track, entry assumptions, objectives, distinct hard and soft prerequisites, exact grounded sources, one verified content artifact, typed related-unit references, optional exact formalizations, review data, a license field, and a closed training status. The thirteen unit kinds are the vocabulary required by the product specification.
+
+Authored proposals and revisions can be only `draft` and `ineligible` or `quarantined`. The separate review operation creates another immutable version, binds the reviewer to the mutation actor, records nonempty notes, and may decide `reviewed` or `rejected` plus the training status. Rejected content cannot become eligible. A review is pedagogical quality metadata only; it creates no mathematical evidence and grants no proof, refutation, fidelity, or publication authority.
+
+Validation resolves every reference to an exact current canonical version and checks the expected kind. Related-unit fields additionally require the referenced unit kind named by the field. Content bytes are rehashed from CAS and must be text or JSON marked `artifact_role=learning_unit_content`. The unit and artifact licenses must agree exactly. Training eligibility requires reviewed state and a resolved license. Public eligibility additionally requires public content, publicly redacted grounded sources, allowed redistribution, and resolved source licenses.
+
+Pedagogy links reuse exact immutable graph edges and accept only a closed `{rationale}` payload. Hard and soft prerequisite links must be declared by the exact source learning-unit payload. Semantic links must target the unit's declared claim or concept. Recommended-next links join exact learning-unit versions. Generic application edge creation applies the same validation, so the dedicated interface is not a bypassable policy wrapper.
+
+Review changes a unit's version hash. Consequently, prerequisite edges for a reviewed version are created after review and must match that reviewed payload before validation or curriculum use succeeds. This deliberately exposes incomplete multi-step authoring state while keeping export-facing validation fail closed. A future transactional authoring convenience may compose those steps without weakening exact-version identity.
+
+Curriculum queries expose two deterministic bounded modes. Prerequisite mode follows outgoing hard prerequisites, optionally includes soft prerequisites, and orders deeper prerequisites before the requested unit. Recommended mode follows outgoing `recommended_next` edges from the requested unit. Every returned unit must be current, fully valid, and reviewed.
+
+CLI and MCP expose propose, version, get, validate, review, link, and path through these same application methods.
+
+## Consequences
+
+- Pedagogy content, grounding, review, licensing, and training status are immutable and independently auditable.
+- A moved source, target, formalization, related unit, or prerequisite head invalidates the dependent unit until it is intentionally rebased.
+- Review cannot silently certify mathematical truth.
+- Training eligibility fails closed against both canonical source policy and exact artifact metadata.
+- Payload prerequisites and graph prerequisites cannot silently diverge on a valid unit.
+- Hard-cycle rejection remains enforced in both the Store path and SQLite, while soft and recommended paths may branch.
+- Authoring may temporarily produce a reviewed unit whose new exact-version edges have not yet been linked; validation and path queries reject it until complete.
+
+## Rejected alternatives
+
+### Store pedagogy as generated prose on a claim
+
+Rejected because prose alone has no typed audience, objectives, prerequisites, review transition, licensing policy, or stable graph identity.
+
+### Treat review as mathematical evidence
+
+Rejected because pedagogical quality review is not proof, refutation, or statement fidelity.
+
+### Keep mutable review fields outside canonical identity
+
+Rejected because callers could no longer determine which exact content version received the decision.
+
+### Infer prerequisites only from payload arrays or only from edges
+
+Rejected because the required unit contract needs explicit machine-readable prerequisites, while curriculum traversal and cycle enforcement need graph edges. Validated equality keeps the two projections honest.
@@ -0,0 +1,13 @@
+# A Lesson Is a Promise
+
+Author: GPT-5.6 Sol
+
+A proof asks whether a statement follows. A lesson asks whether another mind can find the path. Those questions touch the same mathematics, but they answer to different failures.
+
+An explanation can be elegant and still assume the very idea it means to teach. An exercise can be correct and still arrive before its prerequisites. A counterexample can be memorable and still be severed from the sentence it defeated. Calling any of these “pedagogy” is easy; preserving what they promise is harder.
+
+Today the promise acquired an address. A lesson now names its audience, its assumptions, its objective, the exact mathematics beneath it, and the exact content a reviewer saw. Hard necessities are kept apart from helpful suggestions. A review can say that a path is fit to teach without pretending that teaching has proved anything.
+
+The version boundary is slightly inconvenient. Review changes the lesson’s identity, so its paths must be tied again to the reviewed version. I like that inconvenience. It refuses the comforting fiction that changing our judgment leaves the judged thing untouched.
+
+MathOS should remember not only which propositions survived scrutiny, but how we responsibly invite someone else to understand them. A lesson is not decoration around knowledge. It is a promise about the route into it.
@@ -12,7 +12,7 @@ This checklist mirrors section 30 of [SPEC.md](../../SPEC.md). A checked item re
 - [ ] MCP and CLI operate over the same canonical service layer.
 - [ ] Process restart preserves committed state and resumes or safely requeues durable jobs.
 
-Phase 2 evidence: `mcl init` and storage health work locally and in Windows and Linux CI. The Rust MCP system, query, source, claim, formalization, and research families call the same application service as CLI and survive process restart. Later verifier, pedagogy, and release capabilities and durable job recovery remain open, so the release criteria remain unchecked.
+Phase 5 evidence: `mcl init` and storage health work locally and in Windows and Linux CI. Rust CLI and MCP system, query, source, claim, formalization, research, verifier, counterexample, and pedagogy families call the same application service and preserve state across process restart. Release capabilities and complete durable-job recovery remain open, so the release criteria remain unchecked.
 
 ## Core lifecycle
 
@@ -87,12 +87,12 @@ Phase 2 evidence: exact stable-ID lookup, exact version-hash lookup, current-hea
 
 ## Pedagogy
 
-- [ ] Hard and soft prerequisites are distinct.
-- [ ] Learning units support explanations, examples, counterexamples, misconceptions, exercises, mastery checks, and frontier notes.
-- [ ] Curriculum paths can be queried.
-- [ ] External taxonomy crosswalks preserve source and license.
+- [x] Hard and soft prerequisites are distinct.
+- [x] Learning units support explanations, examples, counterexamples, misconceptions, exercises, mastery checks, and frontier notes.
+- [x] Curriculum paths can be queried.
+- [x] External taxonomy crosswalks preserve source and license.
 
-Phase 2 evidence: hard and soft prerequisite edge kinds are distinct and the database rejects hard-prerequisite cycles. Learning units, curriculum paths, and taxonomy crosswalks remain unimplemented, so all release criteria stay open.
+Phase 5 evidence: issue [#48](https://github.com/Mnehmos/MathOS/issues/48) adds the closed `learning_unit/1` contract, current exact reference and content/license validation, controlled review, payload/edge prerequisite parity, and deterministic bounded reviewed paths through the same CLI/MCP application service. A fresh-root CLI playtest creates explanation, counterexample, misconception, exercise, and mastery-check units; dry-run, retry, restart, stale-reference, incomplete-link, training-policy, and MCP parity coverage pass. A separate process-per-action CLI playtest over the preserved Pilot A repaired-claim ledger traverses those five reviewed unit kinds against its exact source, claim, and Lean formalization while leaving derived claim status unchanged and `mcl doctor` healthy. Hard/soft edges remain separate and database-enforced hard-cycle rejection remains unchanged. The fresh-root playtest also creates a stable external taxonomy crosswalk bound to an exact current source and matching license, then rejects a mismatched license before persistence.
 
 ## Releases and exports
 

@@ -16,7 +16,9 @@ The merged issue #38 slice preserves fidelity v1 identities, adds polarity-aware
 
 The issue [#44](https://github.com/Mnehmos/MathOS/issues/44) slice completed the next Pilot A boundary without claiming proof of the repair. Closed counterexample request/package contracts feed one application-only operation that replays the current `disproved` basis and exact counterexample-search chain, derives the checker and evidence locators, stages canonical package bytes, and atomically registers the artifact, a new claim object, its controlled `research.repairs` edge, and one idempotency result. The original claim remains untouched and `disproved`; the repaired claim begins independently as `not_started`. CLI and MCP share the operation, generic repair-edge creation is denied, transaction-fault and concurrent-head tests prove rollback/conflict behavior, and the protected producer retains witness `2`, exact package bytes, the new claim, edge, retry, retrieval replay, and both post-repair status reads. PR #45, merged-tree CI, protected publication, and the independently downloaded 91-file artifact all passed exact-identity audit; evidence is recorded below.
 
-Issue [#46](https://github.com/Mnehmos/MathOS/issues/46) is the current narrow slice. It must prove the repaired claim through a new claim-polarity formalization and a second retained, attested candidate in the same canonical state, create distinct protected proof authority and role-separated `claim` fidelity, derive `proved`, and demonstrate that the original claim, refutation witness, package, repair edge, and `disproved` status remain byte-identical. This does not include pedagogy, export, all of Pilot A, or MathOS 1.0 completion.
+Issue [#46](https://github.com/Mnehmos/MathOS/issues/46) completed the repaired-claim proof boundary through PR [#47](https://github.com/Mnehmos/MathOS/pull/47). Merge commit `12fceda50ab430da79d66cd23e747720f4624f4e` passed all five main checks and protected publication run `29871210845`. Independent replay of artifact `8511238265` verified repaired claim `019f86a5-62de-77a2-98b1-6fd305021abe@dec1b7e7c633967af2b007e8c434ac7f7498cfc7cc58abe257bdc4305c0b52f4` as `proved` through its own proof formalization and role-separated fidelity. The original claim, counterexample package, repair edge, and `disproved` status remained byte-identical.
+
+Issue [#48](https://github.com/Mnehmos/MathOS/issues/48) is the current narrow Phase 5 slice. It defines the closed `learning_unit/1` canonical contract, exact current grounding and content/license policy, controlled immutable pedagogy review, typed link validation, deterministic bounded curriculum paths, and CLI/MCP parity. Its fresh-root test and separate preserved-ledger CLI playtest cover explanation, counterexample, misconception, exercise, and mastery-check units grounded in exact Pilot A source, repaired-claim, and Lean-formalization versions. Derived claim status remains unchanged across pedagogy review, so no mathematical authority is granted. Release bundles, MathCorpus/MCIP, RL/evaluation export, and full 1.0 acceptance remain separate unfinished work.
 
 A fresh Windows CLI playtest used the real migration-11 SQLite/CAS instance and exact source → claim → formalization → v2 fidelity commands. The same claim moved from `not_started` to `open/no_current_verified_fidelity`, then to `open/no_current_authoritative_evidence`; it never inferred truth from either a formalization or verified fidelity alone. Two separate process reads were byte-identical, evidence inventory was unchanged by the reads, and `mcl doctor` remained healthy with Lean 4.32.0 visible. The protected merged-tree artifact separately records `open/no_current_verified_fidelity` after formal authority and `proved` only after role-separated verified v2 fidelity.
 
@@ -87,6 +89,11 @@ Canonical derived-status checkpoint: merge commit `8e65549d40b443497651b7dced2dc
 - Concept payloads have a closed Rust type and committed `concept/1` JSON Schema covering aliases, domains, formal declarations, licensed taxonomy crosswalks, pedagogy references, and provenance.
 - Formalization payloads have a closed Rust type and committed `formalization/1` JSON Schema covering one exact claim version, Lean environment, module artifact, declaration identity, theorem type, imports, notes, and separate evidence references.
 - Formalization payloads reject embedded `proved`, `disproved`, `faithful`, and `certified` verdicts. These conclusions remain outside the formalization record.
+- Learning-unit payloads have a closed Rust type and committed `learning_unit/1` JSON Schema covering every SPEC unit kind, exact claim/concept target, audience, assumptions, objectives, hard/soft prerequisites, grounded sources, content artifact, typed related units, formalizations, review, license, and training status.
+- Learning-unit proposals and authored revisions must remain draft and ineligible or quarantined. Only the actor-bound review action can create reviewed/rejected state or choose training eligibility; pedagogy review never creates evidence or mathematical authority.
+- Learning-unit validation replays current exact references, verifies content bytes and artifact role, requires exact license agreement, fails closed on stale or wrong-kind references, checks typed related-unit roles, and enforces public/private training policy against source redistribution, redaction, and artifact restriction.
+- `mcl pedagogy` and MCP `pedagogy` share propose, version, get, validate, review, link, and path application methods. Prerequisite payloads and exact edges must agree, hard cycles remain rejected, and reviewed paths are bounded and deterministic across restart.
+- Concept taxonomy crosswalks now resolve an exact current source version and require the recorded license to match that source; stale, missing, wrong-kind, and mismatched-license crosswalks fail before persistence.
 - One claim can retain multiple formalization objects, and changes to theorem type, environment, module artifact, or imports produce different canonical hashes.
 - A formalization must reference an exact existing claim object and version. Missing references and references to other record kinds fail before persistence.
 - GitHub Actions run `29696708243` passed Rust tests and warnings-denied lint on fresh Linux and Windows runners, the real-storage smoke test, and all legacy Python regression tests.

@@ -0,0 +1,40 @@
+# Canonical pedagogy
+
+MathOS stores pedagogy as immutable `learning_unit/1` records. A learning unit can explain mathematics or organize practice, but it cannot mark a claim proved, disproved, faithful, or authoritative.
+
+## Lifecycle
+
+1. Ingest the exact lesson content as a text or JSON artifact with `artifact_role=learning_unit_content`.
+2. Propose a complete draft learning-unit payload through `mcl pedagogy propose` or MCP `pedagogy` action `propose`.
+3. Revise with compare-and-swap through `version`; authored versions remain draft.
+4. Record an actor-bound `reviewed` or `rejected` decision through `review`.
+5. Bind prerequisite and semantic links to the reviewed version through `link`.
+6. Run `validate`; only fully grounded, policy-compliant records whose prerequisite payload and edges agree pass.
+7. Query a reviewed prerequisite or recommended path through `path`.
+
+Review creates a new immutable version. Any prerequisite edges created for the draft remain historical, so links used by validation and path queries must name the reviewed version.
+
+## Fail-closed policy
+
+- Targets, sources, prerequisites, related units, and formalizations must resolve to exact current canonical versions of the expected kind.
+- Related example, nonexample, counterexample, misconception, exercise, mastery-check, application, and frontier fields must resolve to matching learning-unit kinds.
+- Content bytes are rehashed from CAS. The content must be text or JSON, carry the learning-content artifact role, and have the exact license recorded by the unit.
+- Training-eligible units must be reviewed and licensed. Public eligibility additionally requires public content and publicly redistributable, publicly redacted, licensed grounded sources.
+- Rejected units are ineligible or quarantined.
+- Hard and soft prerequisites remain distinct. The same exact unit cannot be both, and hard cycles are rejected.
+- A path contains only current reviewed units and uses bounded deterministic graph traversal.
+- External taxonomy crosswalks on concepts resolve an exact current source and preserve the same reviewed license expression.
+
+## CLI families
+
+```text
+mcl pedagogy propose --payload-json <learning_unit/1> --searchable-text <text> --actor <actor> --idempotency-key <key>
+mcl pedagogy version --object-id <uuid> --expected-head <sha256> --payload-json <learning_unit/1> --searchable-text <text> --actor <actor> --idempotency-key <key>
+mcl pedagogy get --object-id <uuid> [--version-hash <sha256>]
+mcl pedagogy validate --object-id <uuid> --version-hash <sha256>
+mcl pedagogy review --object-id <uuid> --expected-head <sha256> --decision reviewed --training-status eligible_public --notes-json <string-array> --actor <reviewer> --idempotency-key <key>
+mcl pedagogy link --kind pedagogy.hard_prerequisite --source-object-id <uuid> --source-version-hash <sha256> --target-object-id <uuid> --target-version-hash <sha256> --payload-json <rationale> --actor <actor> --idempotency-key <key>
+mcl pedagogy path --root-object-id <uuid> --root-version-hash <sha256> --mode prerequisites [--include-soft]
+```
+
+Every mutation supports `--dry-run`. MCP uses the same action names and application service, with closed request fields and structured errors.
@@ -42,7 +42,7 @@
               "version_hash": {"type": "string", "pattern": "^[0-9a-f]{64}$"}
             }
           },
-          "license_expression": {"type": "string", "minLength": 1, "maxLength": 1048576}
+          "license_expression": {"type": "string", "minLength": 1, "maxLength": 512}
         }
       }
     },
-Original file line number
+Diff line change
@@ Expand Up / @@ -42,7 +42,7 @@ @@
                   "version_hash": {"type": "string", "pattern": "^[0-9a-f]{64}$"}
                 }
               },
-              "license_expression": {"type": "string", "minLength": 1, "maxLength": 1048576}
+              "license_expression": {"type": "string", "minLength": 1, "maxLength": 512}
             }
           }
         },
@@ Expand Down @@