(() => {
  "use strict";
  const data = JSON.parse(document.getElementById("graph-data").textContent);
  if (data.schemaVersion !== 7) throw new Error("Stale semantic graph schema; regenerate the review page.");
  const nodes = new Map(data.nodes.map(node => [node.name, node]));
  const external = new Map(data.externalNodes.map(node => [node.name, node]));
  const get = name => nodes.get(name) || external.get(name);
  const element = id => document.getElementById(id);
  let root = data.roots[0], selected = root.root, mode = "meaning", explicit = false;
  const comparison = globalThis.PhysicsLogicComparison;
  const notebook = globalThis.PhysicsLogicNotebook;
  let notes = [], noteMessage = "", storageUncertain = false, noteUploadSequence = 0;
  const drafts = new Map();
  let baseline = null, baselineName = "", comparisonError = "", uploadSequence = 0;
  let currentInspection;
  const history = [];
  const edges = [];
  const nameLabel = name => name.split(".").at(-1).replaceAll("_", " ");
  const kindLabel = node => node.isClass ? "class" : node.isStructure ? "structure" :
    node.isInstance ? "instance" : node.kind;
  const text = (node, key) => node[explicit ? "explicit" + key[0].toUpperCase() + key.slice(1) : key] || node[key] || "";
  const make = (tag, content, className) => {
    const item = document.createElement(tag);
    if (content !== undefined) item.textContent = content;
    if (className) item.className = className;
    return item;
  };
  const code = (content, className) => make("pre", content, className);
  function synchronizeNotes(incoming = []) {
    let stored = { entries: [], errors: [] }, storage;
    try { storage = localStorage; stored = notebook.load(storage); }
    catch (error) { stored.errors.push(error.message); }
    const merged = notebook.merge(notes, stored.entries, incoming);
    notebook.encode(merged);
    notes = merged;
    let errors = stored.errors;
    if (storage) {
      try { errors = errors.concat(notebook.persist(storage, notes)); }
      catch (error) { errors.push(error.message); }
    }
    storageUncertain = errors.length > 0;
  }
  function openNotebook(name) {
    if (mode === "specification") mode = "meaning";
    navigate(name);
    const panel = element("inspection-panel"); panel.open = true;
    panel.scrollIntoView({ block: "start" }); element("note-text").focus({ preventScroll: true });
  }
  function renderNotebook() {
    element("note-declaration").textContent = selected;
    element("note-scope").textContent = external.has(selected) ?
      "External declaration: type only." : "";
    element("note-scope").hidden = !external.has(selected);
    const draft = drafts.get(root.root + "\0" + selected);
    element("note-text").value = draft?.text || "";
    element("note-kind").value = draft?.kind || "observation";
    element("notebook-storage").textContent = storageUncertain ?
      "Browser storage could not be fully read or written. Keep this tab open and export the notebook. Existing stored entries have not been replaced." :
      "Saved in this browser. Export to keep a portable copy.";
    element("notebook-storage").className = storageUncertain ? "notice" : "muted";
    element("notebook-message").textContent = noteMessage;
    const counts = { matching: 0, stale: 0, outside: 0 };
    const list = element("notebook-entries"); list.replaceChildren();
    for (const item of notes.toReversed()) {
      const attachment = notebook.attachment(item, data); counts[attachment]++;
      const entry = make("details", undefined, "notebook-entry");
      entry.dataset.noteId = item.id; entry.dataset.attachment = attachment;
      const label = { matching: "Version matches this extraction", stale: "Needs reinspection", outside: "Outside this extraction" }[attachment];
      entry.append(make("summary", notebook.kinds[item.kind] + " | " + label + " | " + item.declaration),
        make("p", item.text, "note-content"), make("p", "Recorded " + item.createdAt, "muted"),
        make("p", "Argument: " + item.argument, "muted"));
      if (attachment !== "outside") {
        const button = make("button", "Inspect current declaration"); button.type = "button";
        button.onclick = () => {
          const context = data.roots.find(candidate => candidate.root === item.argument) || root;
          inspectExercise(context.root, item.declaration);
        };
        entry.append(button);
      }
      list.append(entry);
    }
    element("notebook-count").textContent = notes.length + " entries: " + counts.matching +
      " version-matching, " + counts.stale + " needing reinspection, " + counts.outside +
      " outside this extraction.";
    element("export-notebook").disabled = notes.length === 0;
  }
  function downloadJSON(contents, filename) {
    const url = URL.createObjectURL(new Blob([contents], { type: "application/json" })), link = make("a");
    link.href = url; link.download = filename; link.click();
    setTimeout(() => URL.revokeObjectURL(url), 1000);
  }
  function renderComparison() {
    const results = element("comparison-results"), status = element("comparison-status");
    results.replaceChildren();
    element("clear-comparison").disabled = !baseline && !comparisonError;
    status.setAttribute("role", comparisonError ? "alert" : "status");
    if (comparisonError || !baseline) {
      status.textContent = comparisonError || "No earlier extraction selected.";
      return;
    }
    try {
      currentInspection ||= comparison.index(data);
      const changes = comparison.compare(baseline, currentInspection, root.root);
      status.textContent = "Compared with " + baselineName + ": " + changes.changed.length +
        " changed specifications, " + changes.readableOnly.length + " readable-form-only, " +
        changes.added.length + " added to scope, " + changes.removed.length +
        " removed from scope; " + changes.unchanged + " unchanged displayed specifications.";
      if (!changes.changed.length && !changes.readableOnly.length && !changes.added.length && !changes.removed.length) {
        results.append(make("p", "No displayed specification differences."));
      }
      results.append(make("p", "Added and removed entries compare the statement's dependencies. Readable-form-only differences leave explicit forms unchanged.", "muted"));
      if (changes.schemaChanged) results.append(make("p",
        "Extraction schema changed from " + baseline.report.schemaVersion + " to " + data.schemaVersion +
        ".", "comparison-schema"));
      if (changes.interpretationChanges.length) {
        const context = make("details", undefined, "comparison-interpretation");
        context.append(make("summary", "Interpretation changed"));
        for (const difference of changes.interpretationChanges) {
          const block = make("section"); block.dataset.path = difference.path.join(".");
          block.append(make("h3", difference.path.join(" / ") || "Complete review interpretation"));
          const pair = make("div", undefined, "comparison-pair");
          for (const [label, value] of [["Earlier", difference.before], ["Current", difference.after]]) {
            const side = make("div");
            side.append(make("h4", label), code(value === undefined ? "Absent" :
              typeof value === "string" ? value : JSON.stringify(value, null, 2)));
            pair.append(side);
          }
          block.append(pair); context.append(block);
        }
        results.append(context);
      }
      if (changes.changedSources.length) {
        const sources = make("details", undefined, "comparison-sources");
        sources.append(make("summary", changes.changedSources.length + " source, linked-edition or configuration files changed"));
        const list = make("ul");
        changes.changedSources.forEach(path => list.append(make("li", path))); sources.append(list); results.append(sources);
      }
      for (const [kind, names] of [["changed", changes.changed], ["readable-form-only", changes.readableOnly],
        ["added", changes.added], ["removed", changes.removed]]) {
        for (const name of names) {
          const old = kind !== "added" ? baseline.all.get(name) : undefined;
          const now = kind !== "removed" ? get(name) : undefined;
          const entry = make("details", undefined, "comparison-change");
          entry.dataset.declaration = name; entry.dataset.change = kind;
          entry.append(make("summary", kind + ": " + name));
          entry.append(make("p", "Earlier: " + (old ? baseline.external.has(name) ? "external boundary (type only)" : "expanded project declaration" : "outside selected scope") +
            "; current: " + (now ? external.has(name) ? "external boundary (type only)" : "expanded project declaration" : "outside selected scope")));
          if (now) {
            const button = make("button", "Inspect current declaration"); button.type = "button";
            button.onclick = () => inspectExercise(root.root, name); entry.append(button);
          }
          const before = old ? comparison.specification(old) : undefined;
          const after = now ? comparison.specification(now) : undefined;
          for (const difference of comparison.differences(before, after)) {
            const block = make("section");
            block.dataset.path = difference.path.join(".");
            block.append(make("h3", difference.path.join(" / ") || "Complete extracted specification", "comparison-path"));
            const pair = make("div", undefined, "comparison-pair");
            for (const [label, value] of [["Earlier", difference.before], ["Current", difference.after]]) {
              const side = make("div");
              side.append(make("h4", label), code(value === undefined ? "Absent" :
                typeof value === "string" ? value : JSON.stringify(value, null, 2)));
              pair.append(side);
            }
            block.append(pair); entry.append(block);
          }
          results.append(entry);
        }
      }
    } catch (error) {
      status.setAttribute("role", "alert"); status.textContent = error.message;
    }
  }
  function renderArgumentComparison() {
    const results = element("argument-comparison-results"), status = element("argument-comparison-status");
    const target = element("argument-comparison-target").value;
    results.replaceChildren(); status.setAttribute("role", "status");
    if (!target) { status.textContent = "No comparison argument selected."; return; }
    try {
      currentInspection ||= comparison.index(data);
      const scopes = comparison.compareScopes(currentInspection, root.root, target);
      status.textContent = scopes.project.shared.length + " shared project declarations; " +
        scopes.project.leftOnly.length + " only in the current argument; " +
        scopes.project.rightOnly.length + " only in the compared argument.";
      const statements = make("div", undefined, "comparison-pair");
      for (const [label, name] of [["Current argument", scopes.left], ["Compared argument", scopes.right]]) {
        const side = make("section", undefined, "argument-comparison-statement"); side.dataset.root = name;
        side.append(make("h3", label), make("code", name, "full-name"), code(text(get(name), "type")));
        const button = make("button", "Inspect this complete statement"); button.type = "button";
        button.onclick = () => inspectExercise(name); side.append(button); statements.append(side);
      }
      results.append(statements);
      for (const [role, label] of [["project", "Project declarations"], ["boundary", "External boundaries (types only)"]]) {
        for (const [part, title] of [["shared", "Shared by both"], ["leftOnly", "Only in current"], ["rightOnly", "Only in compared"]]) {
          const names = scopes[role][part], group = make("details", undefined, "argument-partition");
          group.dataset.role = role; group.dataset.part = part;
          group.append(make("summary", label + ": " + title + " (" + names.length + ")"));
          const list = make("ul");
          for (const name of names) {
            const item = make("li"), button = make("button", name);
            button.type = "button"; button.dataset.declaration = name;
            button.dataset.root = part === "rightOnly" ? scopes.right : scopes.left;
            button.onclick = () => inspectExercise(button.dataset.root, name);
            item.append(button); list.append(item);
          }
          if (!names.length) group.append(make("p", "None."));
          group.append(list); results.append(group);
        }
      }
    } catch (error) { status.setAttribute("role", "alert"); status.textContent = error.message; }
  }
  function navigate(name, nextRoot = root) {
    if (!get(name)) throw new Error("Missing declaration: " + name);
    if (name !== selected || nextRoot !== root) history.push({ selected, root });
    root = nextRoot;
    selected = name;
    render();
  }
  function chooseRoot(name, declaration = name) {
    const nextRoot = data.roots.find(item => item.root === name);
    if (!nextRoot) throw new Error("Missing selected argument: " + name);
    navigate(declaration, nextRoot);
  }
  function inspectExercise(name, declaration = name) {
    if (mode === "specification") mode = "meaning";
    chooseRoot(name, declaration);
    const diagram = element("diagram");
    diagram.tabIndex = -1;
    diagram.scrollIntoView({ block: "start" });
    diagram.focus({ preventScroll: true });
  }
  function card(name, selectedCard = false) {
    const node = get(name);
    const item = make(selectedCard ? "div" : "button", undefined,
      "node " + (external.has(name) ? "external" : "") + (selectedCard ? " selected" : ""));
    if (!selectedCard) { item.type = "button"; item.onclick = () => navigate(name); }
    item.dataset.declaration = name;
    item.title = name;
    item.append(make("small", external.has(name) ? "External boundary" : kindLabel(node)));
    item.append(make("strong", nameLabel(name)));
    item.append(make("span", node.statement ? text(node.statement, "conclusion") : text(node, "body") || text(node, "type"), "preview"));
    return item;
  }
  function column(title) {
    const item = make("div", undefined, "column");
    item.append(make("h3", title));
    return item;
  }
  function addNeighbors(names, parent, connect, label) {
    if (!names.length) parent.append(make("p", "None in this scope.", "muted"));
    const add = name => {
      const item = card(name);
      parent.append(item);
      connect(item, name);
    };
    names.slice(0, 12).forEach(add);
    if (names.length > 12) {
      const more = make("button", "Show " + (names.length - 12) + " more " + label, "more");
      more.type = "button";
      more.onclick = () => { more.remove(); names.slice(12).forEach(add); drawEdges(); };
      parent.append(more);
    }
  }
  function drawEdges() {
    const diagram = element("diagram"), svg = diagram.querySelector("svg");
    if (!svg || diagram.hidden) return;
    svg.replaceChildren();
    const defs = document.createElementNS("http://www.w3.org/2000/svg", "defs");
    const marker = document.createElementNS("http://www.w3.org/2000/svg", "marker");
    for (const [key, value] of Object.entries({id:"dependency-arrow", viewBox:"0 0 10 10", refX:"9", refY:"5", markerWidth:"6", markerHeight:"6", orient:"auto-start-reverse"})) marker.setAttribute(key, value);
    const tip = document.createElementNS("http://www.w3.org/2000/svg", "path");
    tip.setAttribute("d", "M 0 0 L 10 5 L 0 10 z"); tip.setAttribute("class", "arrow-tip");
    marker.append(tip); defs.append(marker); svg.append(defs);
    const bounds = diagram.getBoundingClientRect();
    svg.setAttribute("viewBox", "0 0 " + bounds.width + " " + bounds.height);
    for (const [from, to] of edges) {
      const a = from.getBoundingClientRect(), b = to.getBoundingClientRect();
      const x1 = a.right - bounds.left, y1 = (a.top + a.bottom) / 2 - bounds.top;
      const x2 = b.left - bounds.left, y2 = (b.top + b.bottom) / 2 - bounds.top;
      const mid = (x1 + x2) / 2;
      const path = document.createElementNS("http://www.w3.org/2000/svg", "path");
      path.setAttribute("d", "M " + x1 + " " + y1 + " C " + mid + " " + y1 + ", " + mid + " " + y2 + ", " + x2 + " " + y2);
      path.setAttribute("marker-end", "url(#dependency-arrow)");
      svg.append(path);
    }
  }
  function renderMeaning(grid, node) {
    element("graph-explanation").textContent =
      "Arrows point from a meaning dependency to its user. Click a declaration to inspect it.";
    const left = column("Meaning depends on"), center = column("Inspecting"), right = column("Used in meanings of");
    const focus = card(selected, true);
    center.append(focus);
    const dependencies = node.dependencies || [];
    addNeighbors(dependencies.filter(name => name !== selected && nodes.has(name)), left, item => edges.push([item, focus]), "project dependencies");
    const externalDependencies = dependencies.filter(name => external.has(name));
    if (externalDependencies.length) {
      const group = make("details", undefined, "external-group");
      group.append(make("summary", externalDependencies.length + " external mathematical dependencies"));
      group.append(make("p", "Their types are inspectable; their bodies remain unexpanded.", "muted"));
      const list = make("div", undefined, "column");
      addNeighbors(externalDependencies, list, () => {}, "external dependencies");
      group.append(list); left.append(group); edges.push([group, focus]);
    }
    if (dependencies.includes(selected)) center.append(make("p", "Self-reference retained in the declaration.", "muted"));
    const allowed = new Set(root.proofDeclarations);
    const users = data.nodes.filter(other => allowed.has(other.name) && other.name !== selected &&
      other.dependencies.includes(selected)).map(other => other.name);
    addNeighbors(users, right, item => edges.push([focus, item]), "users");
    if (external.has(selected)) center.append(make("p", "External declaration: type only.", "muted"));
    grid.append(left, center, right);
  }
  function renderInference(grid, node) {
    element("graph-explanation").textContent =
      "Hypotheses apply jointly. Supporting declarations are proof references.";
    if (!node.statement) {
      grid.append(make("p", "This node is data, a definition, or an unexpanded external declaration. Its meaning is available in the other view.", "notice"));
      return;
    }
    const left = column("Hypotheses, jointly"), center = column("Checked Lean inference"), right = column("Conclusion");
    const focus = card(selected, true);
    center.append(focus);
    const local = node.localStatementContext;
    const binders = local ? local.entries.map(entry => ({ ...entry,
      hypothesis: !entry.defined && entry.propositionValued })) : node.statement.binders;
    const hypotheses = binders.map((binder, index) => ({ ...binder, index }))
      .filter(binder => binder.hypothesis);
    for (const hypothesis of hypotheses) {
      const item = make("div", undefined, "node hypothesis");
      item.append(make("strong", hypothesis.name), code(text(hypothesis, "type")));
      item.append(local ? localEntryButton(hypothesis.index, "Inspect this hypothesis in its local scope") :
        partButton(String(hypothesis.index), "Inspect this hypothesis's dependencies"));
      left.append(item);
      edges.push([item, focus]);
    }
    if (!hypotheses.length) left.append(make("p", "No independent proposition-valued hypotheses in this outer scope. Inspect the complete statement for nested quantifiers.", "muted"));
    if (local) center.append(make("p", "This inference uses the displayed local definitions and ordered parameter scope.", "muted"),
      localEntryButton(local.entries.findIndex(entry => entry.defined), "Inspect the local definitions"));
    const conclusion = make("div", undefined, "node conclusion");
    conclusion.append(code(text(local || node.statement, "conclusion")));
    conclusion.append(local ? localEntryButton("conclusion", "Inspect the conclusion in its local scope") :
      partButton("conclusion", "Inspect the conclusion's dependencies"));
    right.append(conclusion);
    edges.push([focus, conclusion]);
    grid.append(left, center, right);
  }
  function section(parent, title, content) {
    parent.append(make("h3", title), code(content));
  }
  function focusStatementPart(detail, part) {
    const disclosure = detail.querySelector(".statement-dependencies");
    disclosure.open = true;
    const entry = [...disclosure.querySelectorAll(".statement-part")].find(item => item.dataset.part === part);
    entry.scrollIntoView({ block: "center" });
    entry.focus({ preventScroll: true });
  }
  function partButton(part, label) {
    const button = make("button", label, "inspect-statement-part");
    button.type = "button"; button.dataset.part = part;
    button.onclick = () => focusStatementPart(element("detail"), part);
    return button;
  }
  function renderStatementReferences(detail, node) {
    const disclosure = make("details", undefined, "statement-dependencies");
    disclosure.append(make("summary", "Meaning used by each parameter, hypothesis and conclusion"),
      make("p", "Direct references from the statement's types. Proof-use references are shown separately.", "muted"));
    const parts = node.statement.binders.map((binder, index) => ({
      part: String(index), label: "Binder " + (index + 1) + " (" +
        (binder.hypothesis ? "hypothesis" : "parameter") + "): " + binder.name,
      expression: text(binder, "type"), references: binder.references,
    }));
    parts.push({ part: "conclusion", label: "Conclusion under all the binders",
      expression: text(node.statement, "conclusion"), references: node.statement.conclusionReferences });
    for (const part of parts) {
      const entry = make("section", undefined, "statement-part");
      entry.dataset.part = part.part; entry.tabIndex = -1;
      entry.append(make("h4", part.label), code(part.expression));
      const binders = make("div", undefined, "part-binders");
      for (const index of part.references.binders) {
        const button = make("button", (index + 1) + ": " + node.statement.binders[index].name);
        button.type = "button"; button.dataset.binder = String(index);
        button.onclick = () => focusStatementPart(detail, String(index));
        binders.append(button);
      }
      entry.append(make("p", part.references.binders.length ? "Earlier binders referenced:" : "No earlier binders referenced.", "muted"), binders);
      const declarations = make("div", undefined, "part-declarations");
      for (const name of part.references.declarations) {
        const button = make("button", name);
        button.type = "button"; button.dataset.declaration = name;
        button.dataset.boundary = String(external.has(name));
        button.title = external.has(name) ? "External boundary: type only" : "Inspect meaning and all fields";
        button.onclick = () => { mode = "meaning"; inspectExercise(root.root, name); };
        declarations.append(button);
      }
      entry.append(make("p", part.references.declarations.length ? "Direct declaration references (dashed buttons are external boundaries):" : "No direct declaration references.", "muted"), declarations);
      disclosure.append(entry);
    }
    detail.append(disclosure);
  }
  function focusLocalEntry(detail, index) {
    const context = detail.querySelector(".local-statement-context");
    context.open = true;
    const entry = [...context.querySelectorAll("[data-local-entry]")].find(item => item.dataset.localEntry === String(index));
    entry.scrollIntoView({ block: "center" }); entry.focus({ preventScroll: true });
  }
  function localEntryButton(index, label) {
    const button = make("button", label, "inspect-local-entry");
    button.type = "button"; button.dataset.localEntryTarget = String(index);
    button.onclick = () => focusLocalEntry(element("detail"), index);
    return button;
  }
  function renderLocalStatementContext(detail, node) {
    const context = node.localStatementContext;
    if (!context) return;
    const panel = make("details", undefined, "local-statement-context");
    panel.append(make("summary", "Local definitions and their full parameter scope"),
      make("p", "Entries follow forall/let order. Assigned values are definitions; later types and values may depend on earlier entries.", "muted"));
    function references(part, value) {
      const disclosure = make("details", undefined, "local-references");
      disclosure.dataset.localPart = part;
      disclosure.append(make("summary", "Direct references in this " + (part.endsWith(":value") ? "assigned value" : "type or conclusion")));
      const locals = make("div", undefined, "part-binders");
      for (const index of value.binders) {
        const button = make("button", (index + 1) + ": " + context.entries[index].name);
        button.type = "button"; button.dataset.binder = String(index);
        button.onclick = () => focusLocalEntry(detail, index); locals.append(button);
      }
      disclosure.append(make("p", value.binders.length ? "Earlier entries referenced:" : "No earlier entries referenced.", "muted"), locals);
      const declarations = make("div", undefined, "part-declarations");
      for (const name of value.declarations) {
        const button = make("button", name); button.type = "button";
        button.dataset.declaration = name; button.dataset.boundary = String(external.has(name));
        button.onclick = () => { mode = "meaning"; inspectExercise(root.root, name); };
        declarations.append(button);
      }
      disclosure.append(make("p", value.declarations.length ? "Direct declarations (external boundaries have types only):" : "No direct declarations.", "muted"), declarations);
      return disclosure;
    }
    context.entries.forEach((entry, index) => {
      const block = make("section", undefined, "local-statement-entry");
      block.dataset.localEntry = String(index); block.tabIndex = -1;
      block.append(make("h4", (index + 1) + ": " + entry.name, "local-name"),
        make("p", entry.defined ? (entry.propositionValued ? "Defined proof, not an independent hypothesis" : "Local data definition") :
          entry.binding + (entry.propositionValued ? " hypothesis" : " parameter"), "local-kind"),
        code(text(entry, "type"), "local-type"), references(index + ":type", entry.references));
      if (entry.defined) block.append(make("h5", "Assigned value"), code(text(entry, "value"), "local-value"),
        references(index + ":value", entry.valueReferences));
      panel.append(block);
    });
    const conclusion = make("section", undefined, "local-statement-conclusion");
    conclusion.dataset.localEntry = "conclusion"; conclusion.tabIndex = -1;
    conclusion.append(make("h4", "Conclusion in this exact local context"), code(text(context, "conclusion"), "local-conclusion"),
      references("conclusion", context.conclusionReferences));
    panel.append(conclusion); detail.append(panel);
  }
  function renderStructureContext(detail, node) {
    const context = node.structureContext, fields = node.fields;
    const container = make("section", undefined, "structure-context");
    const binders = [...context.parameters, ...fields.map(field => field.context)];
    function references(part, index) {
      const disclosure = make("details", undefined, "context-references");
      disclosure.dataset.contextPart = String(index);
      disclosure.append(make("summary", "Dependencies"));
      const locals = make("div", undefined, "context-locals");
      for (const position of part.binders) {
        const binder = binders[position];
        const button = make("button", (position < context.parameters.length ? "Parameter: " : "Earlier field: ") + binder.name);
        button.type = "button"; button.dataset.binder = String(position);
        button.onclick = () => {
          const target = container.querySelector('[data-context-binder="' + position + '"]');
          if (!target) throw new Error("Missing constructor context binder");
          target.tabIndex = -1; target.scrollIntoView({ block: "center" }); target.focus({ preventScroll: true });
        };
        locals.append(button);
      }
      disclosure.append(make("p", part.binders.length ? "Earlier context entries referenced:" : "No earlier context entries referenced.", "muted"), locals);
      const declarations = make("div", undefined, "context-declarations");
      for (const name of part.declarations) {
        const button = make("button", name);
        button.type = "button"; button.dataset.declaration = name;
        button.dataset.boundary = String(external.has(name));
        button.onclick = () => mode === "specification" ? inspectExercise(root.root, name) : navigate(name);
        declarations.append(button);
      }
      disclosure.append(make("p", part.declarations.length ? "Direct declaration references:" : "No direct declaration references.", "muted"), declarations);
      return disclosure;
    }
    container.append(make("h3", "Shared constructor parameters"), make("p",
      "Read each field type under these parameters and the preceding fields.", "muted"));
    const constructor = make("button", context.constructor, "context-constructor");
    constructor.type = "button";
    constructor.onclick = () => mode === "specification" ? inspectExercise(root.root, context.constructor) : navigate(context.constructor);
    container.append(constructor);
    if (context.parameters.length) {
      const table = make("table", undefined, "structure-parameters");
      const header = make("tr"), columns = ["Parameter", "Kind", "Type in context"];
      columns.forEach(label => { const cell = make("th", label); cell.scope = "col"; header.append(cell); });
      table.append(header);
      context.parameters.forEach((binder, index) => {
        const row = make("tr"); row.dataset.contextBinder = String(index);
        row.append(make("td", binder.name), make("td", binder.binding + (binder.hypothesis ? " hypothesis" : " parameter")));
        const type = make("td"); type.append(code(text(binder, "type"), "context-type"), references(binder.references, index));
        row.append(type); [...row.children].forEach((cell, i) => { cell.dataset.label = columns[i]; }); table.append(row);
      });
      container.append(table);
    } else container.append(make("p", "No shared constructor parameters."));
    container.append(make("h3", "Structure fields in elaborated declaration order"), make("p",
      "Local field names are scoped by this constructor. Every field type is visible below; full qualified names and projection signatures are available in each row.", "muted"));
    const fieldTable = make("table", undefined, "structure-fields");
    const fieldHeader = make("tr"), fieldColumns = ["Field and binding", "Exact type in context"];
    fieldColumns.forEach(label => { const cell = make("th", label); cell.scope = "col"; fieldHeader.append(cell); });
    fieldTable.append(fieldHeader);
    fields.forEach(field => {
      const entry = make("tr", undefined, "structure-field");
      entry.dataset.contextBinder = String(context.parameters.length + field.position);
      const identity = make("td"), type = make("td");
      identity.dataset.label = fieldColumns[0]; type.dataset.label = fieldColumns[1];
      const button = make("button", field.context.name, "field-link context-name"); button.type = "button";
      button.dataset.declaration = field.name;
      button.setAttribute("aria-label", "Inspect field " + field.name);
      button.onclick = () => mode === "specification" ? inspectExercise(root.root, field.name) : navigate(field.name);
      identity.append(button, make("p", "Field " + (field.position + 1) + ": " + field.binding +
        (field.subobject ? "; embedded parent " + field.subobject : ""), "field-metadata"));
      if (field.context.hypothesis) identity.append(make("p", "Proposition-valued field", "context-restriction"));
      type.append(code(text(field.context, "type"), "context-type"));
      const tools = make("div", undefined, "field-tools");
      tools.append(references(field.context.references, context.parameters.length + field.position));
      const full = make("details", undefined, "field-projection");
      full.append(make("summary", "Full projection type"), make("code", field.name, "projection-name"), code(text(field, "type")));
      tools.append(full); type.append(tools); entry.append(identity, type); fieldTable.append(entry);
    });
    container.append(fieldTable);
    container.append(make("h3", "Constructor result under this context"), code(text(context, "result"), "context-result"),
      references(context.resultReferences, "result"));
    detail.append(container);
  }
  function renderMeaningPath(detail, node) {
    currentInspection ||= comparison.index(data);
    const path = comparison.meaningPath(currentInspection, root.root, node.name);
    const disclosure = make("details", undefined, "meaning-path");
    disclosure.dataset.root = root.root; disclosure.dataset.target = node.name;
    disclosure.dataset.reachable = String(path !== null);
    disclosure.append(make("summary", "Connection to selected statement"));
    if (path === null) {
      disclosure.append(make("p", "Outside this statement's meaning dependencies.", "muted"));
    } else {
      disclosure.append(make("p", path.length === 1 ? "This is the selected statement itself." :
        "One shortest meaning-reference path, starting at the selected statement. Each next declaration is a direct specification dependency of the preceding one.", "muted"));
      disclosure.append(make("p", "These are type and definition references, not proof steps. External bodies are not traversed.", "muted"));
      const list = make("ol");
      for (const [position, name] of path.entries()) {
        const item = make("li"); item.dataset.declaration = name;
        item.dataset.boundary = String(external.has(name));
        item.append(make("p", position === 0 ? "Selected statement" :
          external.has(name) ? "External boundary: type only" : "Project meaning dependency", "muted"));
        const button = make("button", name, "meaning-path-link");
        button.type = "button"; button.dataset.declaration = name;
        button.setAttribute("aria-label", "Inspect meaning-path declaration " + name);
        button.onclick = () => { mode = "meaning"; inspectExercise(root.root, name); };
        item.append(button); list.append(item);
      }
      disclosure.append(list);
    }
    detail.append(disclosure);
  }
  function renderAppliedPredicates(detail, node) {
    const expansions = node.appliedPredicates;
    if (!expansions?.entries.length) return;
    const local = expansions.scope === "local", context = local ? node.localStatementContext : node.statement;
    const binders = context[local ? "entries" : "binders"];
    const panel = make("details", undefined, "applied-predicates");
    panel.append(make("summary", "One-step predicate expansions in this scope"),
      make("p", "Actual arguments substituted into one definition, without recursive or external unfolding.", "muted"));
    for (const entry of expansions.entries) {
      const conclusion = entry.part === "conclusion", position = Number(entry.part);
      const block = make("section", undefined, "applied-predicate");
      block.dataset.part = entry.part; block.dataset.scope = expansions.scope;
      block.append(make("h4", conclusion ? "Conclusion in this scope" :
        "Type of entry " + (position + 1) + ": " + binders[position].name));
      const original = conclusion ? text(context, "conclusion") : text(binders[position], "type");
      block.append(make("h5", "Original application"), code(original, "predicate-original"));
      const source = make("button", entry.definition, "predicate-definition");
      source.type = "button"; source.dataset.declaration = entry.definition;
      source.onclick = () => { mode = "meaning"; inspectExercise(root.root, entry.definition); };
      block.append(make("p", "Definition expanded once:", "muted"), source,
        make("h5", "After substituting these arguments"), code(text(entry, "expression"), "predicate-expansion"));
      const references = make("div", undefined, "part-binders");
      for (const index of entry.references.binders) {
        const button = make("button", (index + 1) + ": " + binders[index].name);
        button.type = "button"; button.dataset.binder = String(index);
        button.onclick = () => local ? focusLocalEntry(detail, index) : focusStatementPart(detail, String(index));
        references.append(button);
      }
      block.append(make("p", "Earlier entries referenced by the expansion:", "muted"), references);
      const declarations = make("div", undefined, "part-declarations");
      for (const name of entry.references.declarations) {
        const button = make("button", name); button.type = "button";
        button.dataset.declaration = name; button.dataset.boundary = String(external.has(name));
        button.onclick = () => { mode = "meaning"; inspectExercise(root.root, name); };
        declarations.append(button);
      }
      block.append(make("p", "Remaining direct declarations (external boundaries have types only):", "muted"), declarations);
      panel.append(block);
    }
    detail.append(panel);
  }
  function renderDetailContents(detail, node, proofReferences = true) {
    detail.replaceChildren(make("h2", nameLabel(node.name)), make("code", node.name, "full-name"));
    if (external.has(node.name)) {
      detail.append(make("p", "External declaration: type only.", "muted"));
    } else if (node.review?.status === "reviewed" || node.review?.status === "stale") {
      const review = node.review;
      const status = review.status === "reviewed" ? "Recorded review" : "Recorded review is stale";
      const disclosure = make("details", undefined, "review-record");
      disclosure.append(make("summary", status, "review-status " + review.status),
        make("code", review.fingerprint, "fingerprint"));
      if (review.record) disclosure.append(make("p", review.record.reviewer + " | " + review.record.reviewedAt),
        make("p", review.record.evidence));
      detail.append(disclosure);
    }
    const declarationType = code(text(node, "type"), "declaration-type");
    if (node.structureContext) {
      const full = make("details", undefined, "full-structure-type");
      full.append(make("summary", "Full elaborated structure type"), declarationType); detail.append(full);
    } else detail.append(make("h3", "Exact elaborated type"), declarationType);
    if (node.body !== undefined) section(detail, "Definition body", text(node, "body"));
    renderMeaningPath(detail, node);
    const noteButton = make("button", "Write an inspection note", "write-inspection-note");
    noteButton.type = "button"; noteButton.onclick = () => openNotebook(node.name);
    detail.append(noteButton);
    detail.append(make("p", "Declaration kind: " + kindLabel(node), "declaration-kind"));
    detail.append(make("p", "Module: " + node.module, "muted"));
    const nameContext = make("details", undefined, "name-context");
    nameContext.append(make("summary", "Lean name context"));
    for (const command of ["namespace " + (data.displayNamespace || data.module),
      ...(data.displayOpenNamespaces || []).map(namespace => "open " + namespace)]) {
      const line = make("p");
      line.append(make("code", command, "full-name"));
      nameContext.append(line);
    }
    detail.append(nameContext);
    if (node.statement) {
      const breakdown = make("details", undefined, "statement-breakdown");
      breakdown.append(make("summary", "Statement breakdown: all " + node.statement.binders.length +
        " parameters and hypotheses, then the conclusion"));
      const table = make("table", undefined, "statement-binders");
      const header = make("tr");
      const columns = ["Binder", "Kind", "Exact type"];
      columns.forEach(label => {
        const cell = make("th", label); cell.scope = "col"; header.append(cell);
      });
      table.append(header);
      for (const binder of node.statement.binders) {
        const row = make("tr");
        row.append(make("td", binder.name), make("td", binder.binding + (binder.hypothesis ? " hypothesis" : " parameter")));
        const type = make("td"); type.append(code(text(binder, "type"))); row.append(type); table.append(row);
        [...row.children].forEach((cell, index) => { cell.dataset.label = columns[index]; });
      }
      breakdown.append(make("h3", "All parameters and hypotheses"), table,
        make("h3", "Conclusion under these binders"), code(text(node.statement, "conclusion"), "statement-conclusion"));
      detail.append(breakdown);
      renderStatementReferences(detail, node);
      renderLocalStatementContext(detail, node);
      renderAppliedPredicates(detail, node);
    }
    if (node.structureContext) renderStructureContext(detail, node);
    if (node.parents?.length) {
      detail.append(make("h3", "All direct parents in extends order"));
      for (const parent of node.parents) {
        const entry = make("div", undefined, "parent-entry");
        entry.dataset.position = String(parent.position);
        entry.dataset.embedded = String(parent.embedded);
        entry.append(make("p", "Parent " + (parent.position + 1) + ": " +
          (parent.embedded ? "embedded subobject" : "reconstructed from shared fields"), "parent-kind"));
        for (const [name, role] of [[parent.structure, "structure"], [parent.projection, "projection"]]) {
          const button = make("button", name, "parent-link");
          button.type = "button"; button.dataset.role = role;
          button.onclick = () => mode === "specification" ? inspectExercise(root.root, name) : navigate(name);
          entry.append(button);
        }
        entry.append(code(text(parent, "type")));
        detail.append(entry);
      }
    }
    for (const rule of node.recursorRules || []) section(detail, "Recursor rule: " + rule.constructor, text(rule, "rhs"));
    if (proofReferences && node.proofReferences?.length) {
      const references = make("details");
      references.append(make("summary", "Proof references (" + node.proofReferences.length + "), separate from meaning dependencies"));
      const list = make("div", undefined, "reference-list");
      addNeighbors(node.proofReferences, list, () => {}, "references");
      references.append(list); detail.append(references);
    }
  }
  function renderSpecification() {
    const specification = element("specification");
    specification.replaceChildren(make("h2", "Complete project specification"));
    const names = [...root.meaningGroups.flatMap(group => group.declarations), ...root.externalBoundaries];
    const anchors = new Map(names.map((name, index) => [name, "specification-declaration-" + index]));
    const contents = make("details", undefined, "specification-contents");
    contents.append(make("summary", "Contents: every declaration in this specification"));
    const links = make("ol");
    for (const name of names) {
      const item = make("li"), link = make("a", name);
      link.href = "#" + anchors.get(name); item.append(link); links.append(item);
    }
    contents.append(links); specification.append(contents);
    const entry = (name, parent) => {
      const node = get(name), article = make("article", undefined, "specification-declaration");
      article.id = anchors.get(name); article.dataset.declaration = name;
      article.dataset.boundary = String(external.has(name));
      renderDetailContents(article, node, false);
      if (!external.has(name)) {
        article.append(make("h3", "Direct meaning dependencies"));
        const dependencies = make("ul", undefined, "specification-dependencies");
        for (const dependency of node.dependencies) {
          if (!anchors.has(dependency)) throw new Error("Incomplete specification: " + dependency);
          const item = make("li"), link = make("a", dependency);
          link.href = "#" + anchors.get(dependency); item.append(link); dependencies.append(item);
        }
        article.append(dependencies);
        if (!node.dependencies.length) article.append(make("p", "None in this scope.", "muted"));
      }
      const button = make("button", "Inspect focused neighborhood", "specification-inspect");
      button.type = "button"; button.onclick = () => inspectExercise(root.root, name);
      article.append(button); parent.append(article);
    };
    for (const [index, group] of root.meaningGroups.entries()) {
      const section = make("section", undefined, "specification-group");
      section.dataset.recursive = String(group.recursive);
      section.append(make("h2", "Group " + (index + 1) + ": " + (group.recursive ?
        "mutually referencing declarations" : "one declaration")));
      for (const name of group.declarations) entry(name, section);
      specification.append(section);
    }
    const boundaries = make("section", undefined, "specification-boundaries");
    boundaries.append(make("h2", "External declarations (types only)"));
    for (const name of root.externalBoundaries) entry(name, boundaries);
    specification.append(boundaries);
  }
  function renderInventory() {
    const query = element("search").value.toLowerCase();
    const names = [...root.proofDeclarations, ...root.proofExternalBoundaries].filter(name => name.toLowerCase().includes(query));
    const list = element("inventory-list"); list.replaceChildren();
    element("inventory-count").textContent = names.length + " matches";
    addNeighbors(names, list, () => {}, "declarations");
  }
  function renderExercises() {
    const list = element("exercise-list");
    const open = new Set([...list.querySelectorAll("details[open]")].map(item => item.dataset.exercise));
    list.replaceChildren();
    for (const exercise of data.reviewExercises || []) {
      const section = make("section", undefined, "review-exercise");
      section.dataset.exercise = exercise.id;
      section.append(make("h3", exercise.title), make("p", exercise.question));
      const comparisons = make("div", undefined, "exercise-controls");
      for (const name of exercise.inspect) {
        const button = make("button", "Inspect " + nameLabel(name));
        button.type = "button"; button.dataset.declaration = name;
        button.onclick = () => inspectExercise(exercise.roots[0], name);
        comparisons.append(button);
      }
      const result = make("details");
      result.dataset.exercise = exercise.id; result.open = open.has(exercise.id);
      result.append(make("summary", "Reveal the Lean-checked distinction"));
      for (const name of exercise.roots) {
        const node = get(name);
        result.append(code(text(node, "type")));
        const button = make("button", "Inspect " + nameLabel(name));
        button.type = "button"; button.dataset.root = name;
        button.onclick = () => inspectExercise(name);
        result.append(button);
      }
      section.append(comparisons, result); list.append(section);
    }
  }
  function render() {
    const node = get(selected);
    element("scope").textContent = "";
    element("scope").hidden = true;
    element("root-picker").value = root.root;
    const additional = data.primaryRoot && root.root !== data.primaryRoot;
    element("argument-kind").hidden = !additional;
    element("argument-kind").textContent = additional ?
      "Additional statement." : "";
    if (additional) {
      const back = make("a", "Return to review exercises"); back.href = "#exercises";
      element("argument-kind").append(make("br"), back);
    }
    element("back").disabled = history.length === 0;
    element("meaning-view").setAttribute("aria-pressed", String(mode === "meaning"));
    element("inference-view").setAttribute("aria-pressed", String(mode === "inference"));
    const complete = mode === "specification";
    element("specification-view").setAttribute("aria-pressed", String(complete));
    for (const id of ["diagram", "detail", "inventory"]) element(id).hidden = complete;
    element("specification").hidden = !complete;
    const diagram = element("diagram"); diagram.replaceChildren(); edges.length = 0;
    const svg = document.createElementNS("http://www.w3.org/2000/svg", "svg");
    svg.setAttribute("aria-hidden", "true"); diagram.append(svg);
    const grid = make("div", undefined, "graph-grid"); diagram.append(grid);
    if (complete) {
      element("graph-explanation").textContent = "All meaning dependencies of the selected statement.";
      renderSpecification();
    } else {
      if (mode === "meaning") renderMeaning(grid, node); else renderInference(grid, node);
      renderDetailContents(element("detail"), node);
      requestAnimationFrame(drawEdges);
    }
    renderInventory(); renderExercises(); renderComparison(); renderArgumentComparison(); renderNotebook();
  }
  for (const item of data.roots) {
    const additional = data.primaryRoot && item.root !== data.primaryRoot;
    const option = make("option", (additional ? "Additional statement: " : "Main review statement: ") + nameLabel(item.root));
    option.value = item.root; element("root-picker").append(option);
    const compared = make("option", item.root);
    compared.value = item.root; element("argument-comparison-target").append(compared);
  }
  element("root-picker").onchange = event => chooseRoot(event.target.value);
  element("argument-comparison-target").onchange = renderArgumentComparison;
  element("home").textContent = "Return to main statement";
  element("home").onclick = () => chooseRoot(data.primaryRoot || data.roots[0].root);
  element("back").onclick = () => {
    if (history.length) { const previous = history.pop(); selected = previous.selected; root = previous.root; render(); }
  };
  element("meaning-view").onclick = () => { mode = "meaning"; render(); };
  element("inference-view").onclick = () => { mode = "inference"; render(); };
  element("specification-view").onclick = () => { mode = "specification"; render(); };
  element("explicit").onchange = event => { explicit = event.target.checked; render(); };
  element("search").oninput = renderInventory;
  element("export-extraction").onclick = () => {
    try {
      const blob = new Blob([comparison.encode(data)], { type: "application/json" });
      const url = URL.createObjectURL(blob), link = make("a");
      const pageName = location.pathname.split("/").at(-1).replace(/\.html$/i, "").replace(/[^A-Za-z0-9_-]/g, "_");
      link.href = url; link.download = "physicslogic-" + pageName + "-" + data.sourceSnapshot.slice(0, 12) + ".json";
      link.click(); setTimeout(() => URL.revokeObjectURL(url), 1000);
    } catch (error) { comparisonError = error.message; renderComparison(); }
  };
  element("baseline-file").onchange = async event => {
    const sequence = ++uploadSequence, file = event.target.files[0];
    baseline = null; baselineName = ""; comparisonError = ""; renderComparison();
    if (!file) return;
    try {
      if (file.size > comparison.limit) throw new Error("Extraction exceeds the 16 MiB comparison limit.");
      const contents = await file.text();
      if (sequence !== uploadSequence) return;
      baseline = comparison.decode(contents); baselineName = file.name;
    } catch (error) {
      if (sequence !== uploadSequence) return;
      comparisonError = "Comparison rejected: " + error.message;
    }
    renderComparison();
  };
  element("clear-comparison").onclick = () => {
    ++uploadSequence; baseline = null; baselineName = ""; comparisonError = "";
    element("baseline-file").value = ""; renderComparison();
  };
  const updateDraft = () => drafts.set(root.root + "\0" + selected,
    { text: element("note-text").value, kind: element("note-kind").value });
  element("note-text").oninput = updateDraft;
  element("note-kind").onchange = updateDraft;
  element("note-form").onsubmit = event => {
    event.preventDefault();
    try {
      synchronizeNotes([notebook.create(data, selected, root.root, element("note-kind").value, element("note-text").value)]);
      drafts.delete(root.root + "\0" + selected);
      noteMessage = "Entry added to the notebook.";
    } catch (error) { noteMessage = "Note not added: " + error.message; }
    renderNotebook();
  };
  element("export-notebook").onclick = () => {
    let warning = "";
    try { synchronizeNotes(); }
    catch (error) { storageUncertain = true; warning = " Storage merge failed; exporting the entries retained in this tab. " + error.message; }
    try {
      downloadJSON(notebook.encode(notes), "physicslogic-inspection-notebook-" + new Date().toISOString().slice(0, 10) + ".json");
      noteMessage = "Notebook export requested." + warning;
    } catch (error) { noteMessage = "Export failed: " + error.message; }
    renderNotebook();
  };
  element("notebook-file").onchange = async event => {
    const sequence = ++noteUploadSequence, file = event.target.files[0];
    if (!file) return;
    try {
      if (file.size > notebook.limit) throw new Error("Notebook exceeds the 2 MiB limit.");
      const contents = await file.text();
      if (sequence !== noteUploadSequence) return;
      synchronizeNotes(notebook.decode(contents));
      noteMessage = "Notebook merged without replacing existing entries.";
    } catch (error) {
      if (sequence !== noteUploadSequence) return;
      noteMessage = "Import rejected: " + error.message;
    }
    element("notebook-file").value = ""; renderNotebook();
  };
  window.addEventListener("storage", event => {
    if (event.key !== null && !event.key.startsWith(notebook.prefix)) return;
    try { synchronizeNotes(); }
    catch (error) { noteMessage = "Storage merge failed: " + error.message; storageUncertain = true; }
    renderNotebook();
  });
  window.addEventListener("beforeunload", event => {
    if ((storageUncertain && notes.length) || [...drafts.values()].some(draft => draft.text.trim())) {
      event.preventDefault(); event.returnValue = "";
    }
  });
  try { synchronizeNotes(); }
  catch (error) { noteMessage = "Notebook could not be restored: " + error.message; storageUncertain = true; }
  new ResizeObserver(drawEdges).observe(element("diagram"));
  render();
  document.documentElement.dataset.semanticGraphReady = "true";
})();