diff --git a/components/graph-view.tsx b/components/graph-view.tsx
index 65d5c1f..60a6d1e 100644
--- a/components/graph-view.tsx
+++ b/components/graph-view.tsx
@@ -104,7 +104,7 @@ export function GraphView() {
 			// frozen layout stable for a given node set across remounts.
 			const rand = seededRandom(node.id);
 			graph.addNode(node.id, {
-				label: node.statement,
+				label: node.name,
 				size: STATE_TOKENS[state].size,
 				color: stateColors.get(state) ?? edgeColor,
 				x: (rand() - 0.5) * 100,
@@ -190,7 +190,8 @@ export function GraphView() {
 						className="absolute left-1/2 top-6 w-80 max-w-[90%] -translate-x-1/2 rounded-xl border bg-card p-4 text-left shadow-lg"
 						onClick={(e) => e.stopPropagation()}
 					>
-						<div className="text-sm font-medium leading-snug">{selected.node.statement}</div>
+						<div className="text-sm font-medium leading-snug">{selected.node.name}</div>
+						<div className="mt-1 text-xs leading-relaxed text-muted-foreground">{selected.node.statement}</div>
 						<div className="mt-1 text-xs uppercase tracking-wide text-muted-foreground">
 							{STATE_LABELS[selected.state]}
 						</div>
diff --git a/next-env.d.ts b/next-env.d.ts
index a419cbe..ce4e94a 100644
--- a/next-env.d.ts
+++ b/next-env.d.ts
@@ -1,7 +1,7 @@
 /// <reference types="next" />
 /// <reference types="next/image-types/global" />
-import "./.next/dev/types/routes.d.ts";
-import "./.next/dev/types/root-params.d.ts";
+import "./.next/types/routes.d.ts";
+import "./.next/types/root-params.d.ts";
 
 // NOTE: This file should not be edited
 // see https://nextjs.org/docs/app/api-reference/config/typescript for more information.
diff --git a/src/agent/subagents/extraction.ts b/src/agent/subagents/extraction.ts
index 6b9b30b..dc9edaf 100644
--- a/src/agent/subagents/extraction.ts
+++ b/src/agent/subagents/extraction.ts
@@ -99,7 +99,18 @@ const findingsSchema = z.object({
 		.array(
 			z.object({
 				id: z.string().describe("Local id: \"p1\", \"p2\", … — referenced by edges and attribution."),
-				statement: z.string().describe("The proposition as one reasoning step — a node statement."),
+				name: z.string().describe(
+					"A short 2-6 word name for the fact — its header, used for rendering. Not a sentence.",
+				),
+				statement: z
+					.string()
+					.describe(
+						"The proposition as one reasoning step — an OBJECTIVE, world-facing fact. " +
+							"Never reference the learner, the teacher, or the session: not \"the learner " +
+							'understands X\" but \"X\"; not \"the learner thinks Y\" but the wrong idea itself, ' +
+							'stated as a claim (\"Reading: Nietzsche endorsed might-makes-right social Darwinism\"), ' +
+							"with kind \"misconception\" carrying that it is wrong.",
+					),
 				aliases: z.array(z.string()).describe("Verbatim alternate phrasings from this session, if any."),
 				kind: z.enum(["truth", "misconception"]).describe("misconception = a wrong idea the learner holds or was warned about."),
 				treeNodeId: z.string().optional().describe("The plan-tree node id this came from, when it did."),
@@ -134,7 +145,17 @@ verbatim (LEARNER / TEACHER), and structured events (QUIZ lines with the learner
 
 Report, with verbatim evidence quotes for everything:
 
+NODE THEORY — the graph is a set of objective facts, full stop. A node is what is true (or falsely
+believed) about the world, never anything about the learner or the session. The learner's
+relationship to a fact — whether they know it, missed it, or hold it as a misconception — is
+expressed ENTIRELY by the quiz-outcome events you attribute; it never leaks into the node itself.
+So no "the learner understands X", no "discussed in this session": the node is just X. A
+misconception node states the wrong idea itself as a claim, with kind "misconception" marking it
+wrong — never "the learner believes Y".
+
 1. PROPOSITIONS — every distinct reasoning-step-sized proposition the session touched:
+   - Each carries a "name": a short 2-6 word header (the rendering handle), and a "statement": the
+     full fact as one objective reasoning step.
    - Plan-tree nodes become propositions (pass their treeNodeId) — statement from the node title, enriched to a
      complete proposition if the prose elaborates it.
    - Propositions that appeared only in prose (teacher explanations, learner questions) get fresh ids.
@@ -201,7 +222,9 @@ verified subset.
 
 Verify:
 - PROPOSITIONS: every evidence quote must appear (near-)verbatim in the transcript view, and the statement must
-  be a faithful reading of it. Drop invented or bloated statements. Conservative: when two proposed propositions
+  be a faithful reading of it. The node theory applies: a statement must be an OBJECTIVE, world-facing fact —
+  reword learner- or session-relative statements ("the learner understands X" → "X") or drop them when the
+  objective fact is not actually backed. Drop invented or bloated statements. Conservative: when two proposed propositions
   are really one, keep the better-stated one and drop the other.
 - EDGES: the evidence must actually articulate the relation, in the direction claimed (from = prerequisite).
   Drop direction-swapped or speculative edges.
diff --git a/src/core/contracts.ts b/src/core/contracts.ts
index 0f31e72..2f2a1ed 100644
--- a/src/core/contracts.ts
+++ b/src/core/contracts.ts
@@ -66,7 +66,15 @@ export type EdgeType = "requires" | "supports";
 export interface GraphNode {
 	/** Opaque stable id, store-assigned: "n_" + nanoid-like. */
 	id: string;
-	/** Canonical proposition statement. */
+	/** Short name / header for the fact (2-6 words) — the rendering handle.
+	 *  NODE THEORY: a node is an OBJECTIVE fact, never learner- or
+	 *  session-relative. No "the learner understands…", no "this session
+	 *  covered…" — just the fact, world-facing. The learner's relationship
+	 *  to the fact lives ENTIRELY in the event ledger: state labels are
+	 *  derived from quiz outcomes, never written into the node. */
+	name: string;
+	/** Canonical proposition statement — the full fact, one reasoning step,
+	 *  also objective (no learner / teacher / session references). */
 	statement: string;
 	/** Verbatim alternate statements from sessions (merge target audit trail). */
 	aliases: string[];
@@ -146,7 +154,11 @@ export interface LedgerEvent {
 export interface ExtractedProposition {
 	/** Extractor-local id ("p1", …) referenced by edges + attribution. */
 	id: string;
-	/** Canonical one-reasoning-step statement. */
+	/** Short name / header for the fact (2-6 words) — the rendering handle. */
+	name: string;
+	/** Canonical one-reasoning-step statement — an objective, world-facing
+	 *  fact (no learner / teacher / session references; the learner's
+	 *  relationship to it is carried only by the event attribution). */
 	statement: string;
 	/** Verbatim alternate phrasings from the session (merge aliases). */
 	aliases: string[];
diff --git a/src/core/graph.ts b/src/core/graph.ts
index c4c6616..dc21609 100644
--- a/src/core/graph.ts
+++ b/src/core/graph.ts
@@ -160,6 +160,7 @@ export function mergeFindings(chatId: string, findings: SessionFindings, deps: G
 		} else {
 			const graphNode: GraphNode = {
 				id: newGraphNodeId(),
+				name: p.name,
 				statement: p.statement,
 				aliases: [...p.aliases],
 				kind: p.kind,
diff --git a/src/store/graph.ts b/src/store/graph.ts
index 69b3ca5..064e9c0 100644
--- a/src/store/graph.ts
+++ b/src/store/graph.ts
@@ -69,13 +69,24 @@ function readValid<T>(file: string, isValid: (v: unknown) => v is T): T[] {
 	return readRawLines(file).filter(isValid);
 }
 
-const isGraphNode = (v: unknown): v is GraphNode =>
+/** Pre-name ledger line (the first extraction runs) — read tolerantly. */
+type StoredGraphNode = Omit<GraphNode, "name"> & { name?: string };
+
+const isStoredGraphNode = (v: unknown): v is StoredGraphNode =>
 	isRecord(v) &&
 	isString(v.id) &&
 	isString(v.statement) &&
 	Array.isArray(v.aliases) &&
 	(v.kind === "truth" || v.kind === "misconception") &&
-	isString(v.createdAt);
+	isString(v.createdAt) &&
+	(v.name === undefined || isString(v.name));
+
+/** Derived header for legacy node lines written before `name` existed:
+ *  the first clause of the statement, capped — good enough to render. */
+function nameFromStatement(statement: string): string {
+	const clause = statement.split(/[.;:—]/)[0]!.trim();
+	return clause.length > 60 ? `${clause.slice(0, 57)}…` : clause || statement;
+}
 
 const EDGE_TYPES = ["requires", "supports"] as const;
 
@@ -116,9 +127,13 @@ export const graphStore: GraphStore = {
 	appendNode(node: GraphNode): void {
 		appendLine(LEDGER_FILES.nodes, node);
 	},
-	/** Raw node lines in append order (ids are unique — no merging needed). */
+	/** Raw node lines in append order (ids are unique — no merging needed).
+	 *  Legacy lines without a `name` get one derived from the statement. */
 	readNodes(): GraphNode[] {
-		return readValid(LEDGER_FILES.nodes, isGraphNode);
+		return readValid(LEDGER_FILES.nodes, isStoredGraphNode).map((n) => ({
+			...n,
+			name: n.name ?? nameFromStatement(n.statement),
+		}));
 	},
 
 	/** Append one edge ASSERTION; readers merge lines by (from,to,type). */
diff --git a/tests/extraction.test.ts b/tests/extraction.test.ts
index fbdd3f7..8fa812e 100644
--- a/tests/extraction.test.ts
+++ b/tests/extraction.test.ts
@@ -135,6 +135,7 @@ const FINDINGS: SessionFindings = {
 	propositions: [
 		{
 			id: "p1",
+			name: "Chain rule",
 			statement: "Chain rule intuition",
 			aliases: [],
 			kind: "truth",
@@ -143,6 +144,7 @@ const FINDINGS: SessionFindings = {
 		},
 		{
 			id: "p2",
+			name: "Applying chain rule",
 			statement: "Applying the chain rule",
 			aliases: [],
 			kind: "truth",
diff --git a/tests/graph-context.test.ts b/tests/graph-context.test.ts
index ab845ec..7156dc5 100644
--- a/tests/graph-context.test.ts
+++ b/tests/graph-context.test.ts
@@ -43,7 +43,7 @@ import { PATHS } from "../config.ts";
 // ─── fixtures ────────────────────────────────────────────────────────────────
 
 function node(id: string, statement: string, over: Partial<GraphNode> = {}): GraphNode {
-	return { id, statement, aliases: [], kind: "truth", createdAt: "2026-08-22T00:00:00.000Z", ...over };
+	return { id, name: statement.split(";")[0]!, statement, aliases: [], kind: "truth", createdAt: "2026-08-22T00:00:00.000Z", ...over };
 }
 
 function edge(from: string, to: string): GraphEdge {
@@ -329,6 +329,7 @@ function treeFindings(tree: ReturnType<typeof createTree>): SessionFindings {
 	return {
 		propositions: tree.nodes.map((n, i) => ({
 			id: `p${i + 1}`,
+			name: n.title,
 			statement: n.title,
 			aliases: [],
 			kind: "truth" as const,
@@ -380,6 +381,7 @@ describe("exact-match merge (merger identity resolution)", () => {
 		const ledgers = memoryLedgers();
 		ledgers.appendNode({
 			id: "n_alias",
+			name: "Differentiation",
 			statement: "Differentiation basics",
 			aliases: ["the derivative"],
 			kind: "truth",
diff --git a/tests/graph.test.ts b/tests/graph.test.ts
index 7e74a1a..7759530 100644
--- a/tests/graph.test.ts
+++ b/tests/graph.test.ts
@@ -136,6 +136,7 @@ function treeFindings(tree: PlanTree): SessionFindings {
 	return {
 		propositions: tree.nodes.map((n, i) => ({
 			id: `p${i + 1}`,
+			name: n.title,
 			statement: n.title,
 			aliases: [],
 			kind: "truth" as const,
@@ -428,7 +429,7 @@ describe("the trigger helper (pendingQuizAnswers)", () => {
 
 describe("graph ledger store", () => {
 	it("round-trips lines and skips corrupt / foreign-shaped lines (strict reads)", () => {
-		const node = { id: "n_storetest", statement: "Store test", aliases: [], kind: "truth" as const, createdAt: "2026-08-22T00:00:00.000Z" };
+		const node = { id: "n_storetest", name: "Store test", statement: "Store test", aliases: [], kind: "truth" as const, createdAt: "2026-08-22T00:00:00.000Z" };
 		graphStore.appendNode(node);
 		// A torn append and a legacy V0-shaped node (different schema) — both skipped.
 		fs.appendFileSync(
@@ -439,5 +440,18 @@ describe("graph ledger store", () => {
 		const nodes = graphStore.readNodes().filter((n) => n.id === "n_storetest" || n.id === "legacy");
 		assert.equal(nodes.length, 1);
 		assert.equal(nodes[0]!.statement, "Store test");
+		assert.equal(nodes[0]!.name, "Store test");
+	});
+
+	it("derives a name for pre-name ledger lines (legacy reads)", () => {
+		// A full, valid node line written before `name` existed.
+		fs.appendFileSync(
+			LEDGER_FILES.nodes,
+			`${JSON.stringify({ id: "n_prename", statement: "Derivatives measure instantaneous change; they are limits.", aliases: [], kind: "truth", createdAt: "2026-08-22T00:00:00.000Z" })}\n`,
+			"utf-8",
+		);
+		const node = graphStore.readNodes().find((n) => n.id === "n_prename");
+		assert.ok(node);
+		assert.equal(node.name, "Derivatives measure instantaneous change");
 	});
 });