:root {
  --bg: #fdfdfb;
  --fg: #1f2328;
  --muted: #646b76;
  --line: #dfdfd8;
  --panel: #f1f1ec;
  --link: #1d58b0;
  --ref: #e4eff6;
  --ref-edge: #7fb1cf;
  --note: #ecece6;
  --note-edge: #b5b5aa;
  --sans: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
  --serif: Charter, "Bitstream Charter", "Iowan Old Style", "Palatino Linotype", Georgia, serif;
  --mono: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
}
@media (prefers-color-scheme: dark) {
  :root {
    --bg: #17191d;
    --fg: #e3e5e8;
    --muted: #9aa2ae;
    --line: #30343b;
    --panel: #1f2228;
    --link: #86b3ff;
    --ref: #1c2a35;
    --ref-edge: #3f6f8c;
    --note: #23262c;
    --note-edge: #555b66;
  }
}

* { box-sizing: border-box; }
html { -webkit-text-size-adjust: 100%; }
body {
  margin: 0;
  background: var(--bg);
  color: var(--fg);
  font: 16px/1.5 var(--sans);
  min-height: 100vh;
  display: flex;
  flex-direction: column;
}
a { color: var(--link); text-decoration: none; }
a:hover { text-decoration: underline; }
code, pre { font-family: var(--mono); font-size: 0.88em; }
pre { background: var(--panel); padding: 0.7rem 0.9rem; border-radius: 6px; overflow-x: auto; }
.small { font-size: 0.85rem; color: var(--muted); }

/* Header */
.top {
  display: flex; flex-wrap: wrap; align-items: center; gap: 0.5rem 1.5rem;
  padding: 0.7rem 1.5rem;
  background: var(--panel);
  border-bottom: 1px solid var(--line);
}
.brand { font-size: 1.3rem; font-weight: 600; color: var(--fg); letter-spacing: -0.01em; }
.brand:hover { text-decoration: none; }
.menu { display: flex; gap: 1.2rem; margin-left: auto; font-size: 0.92rem; }
.lookup input, .searchform input {
  font: inherit; color: inherit;
  background: var(--bg);
  border: 1px solid var(--line); border-radius: 6px;
  padding: 0.35rem 0.7rem;
}
.lookup input { width: 12rem; font-size: 0.9rem; }
.searchform input { width: 100%; font-size: 1.05rem; padding: 0.6rem 0.9rem; }
input:focus-visible, a:focus-visible, summary:focus-visible { outline: 2px solid var(--link); outline-offset: 2px; }

.crumbs {
  padding: 0.5rem 1.5rem;
  font-size: 0.88rem; color: var(--muted);
  border-bottom: 1px solid var(--line);
}
.crumbs .sep { margin: 0 0.5rem; opacity: 0.6; }

/* Layout */
.layout {
  flex: 1;
  width: 100%; max-width: 70rem;
  margin: 0 auto; padding: 1.8rem 1.5rem 3rem;
  display: grid; grid-template-columns: minmax(0, 1fr) 17rem; gap: 2.5rem;
  align-items: start;
}
.layout.wide { grid-template-columns: minmax(0, 1fr); max-width: 52rem; }
@media (max-width: 820px) {
  .layout { grid-template-columns: minmax(0, 1fr); gap: 1.5rem; }
  .menu { margin-left: 0; }
  .lookup { flex: 1 1 100%; }
  .lookup input { width: 100%; }
}

footer {
  display: flex; flex-wrap: wrap; justify-content: space-between; gap: 0.3rem 2rem;
  padding: 0.9rem 1.5rem;
  border-top: 1px solid var(--line);
  font-size: 0.8rem; color: var(--muted);
}

/* Text */
.content { font-family: var(--serif); font-size: 1.06rem; line-height: 1.6; }
.content h1 { font: 600 1.6rem/1.25 var(--sans); margin: 0 0 1.2rem; letter-spacing: -0.01em; }
.content h2 { font: 600 1.2rem/1.3 var(--sans); margin: 2rem 0 0.7rem; }
.content h3 { font: 600 1.05rem/1.3 var(--sans); margin: 1.8rem 0 0.6rem; }
.content h1 .num, .content h2 .num { color: var(--muted); font-weight: 500; margin-right: 0.35em; }
.content p { margin: 0 0 0.8rem; }
.lead { font-size: 1.15rem; color: var(--muted); font-style: italic; margin-bottom: 1.6rem; }
.math.display { display: block; overflow-x: auto; overflow-y: hidden; padding: 0.15rem 0; }
.broken { color: #c0392b; font-weight: 600; }

/* Statements */
.env { margin: 1.3rem 0; }
.env.plain .env-body { font-style: italic; }
.env.plain .env-body em { font-style: normal; }
.env-head { font-weight: 700; font-style: normal; color: inherit; }
.env-name, .env-dot { font-style: normal; }
.env-body > :last-child, .proof > :last-child, .env-meta > :last-child { margin-bottom: 0; }
.proof { margin-top: 0.7rem; }
.qed { float: right; margin-left: 1rem; }
.env-meta {
  font-size: 0.93em;
  margin: 0 0 0.6rem; padding: 0.5rem 0.9rem;
  background: var(--note); border-left: 3px solid var(--note-edge);
  border-radius: 0 4px 4px 0;
}
.env-meta.reference { background: var(--ref); border-left-color: var(--ref-edge); }
.sub-num { color: var(--muted); }

.fn { position: relative; cursor: help; }
.fn sup { color: var(--link); }
.fn-body {
  display: none; position: absolute; left: 0; top: 1.5em; z-index: 5;
  width: min(22rem, 80vw); padding: 0.6rem 0.8rem;
  background: var(--panel); border: 1px solid var(--line); border-radius: 6px;
  font-size: 0.9rem; font-style: normal;
}
.fn:hover .fn-body, .fn:focus .fn-body { display: block; }

/* Lists of contents */
.toc { list-style: none; padding: 0; margin: 0; }
.toc li { padding: 0.28rem 0; }
.toc .toc { padding: 0.2rem 0 0.4rem 1.6rem; font-size: 0.97em; }
.toc summary { cursor: pointer; }
.toc summary::marker { color: var(--muted); }

/* Home */
.tiles { display: grid; grid-template-columns: repeat(auto-fill, minmax(13.5rem, 1fr)); gap: 0.8rem; }
.tile {
  display: flex; align-items: center; gap: 0.8rem;
  padding: 0.95rem 1.1rem;
  font: 500 1rem var(--sans); color: var(--fg);
  border: 1px solid var(--line); border-radius: 8px;
  transition: border-color 0.12s, background 0.12s;
}
.tile:hover { text-decoration: none; border-color: var(--link); background: var(--panel); }
.tile svg {
  width: 1.5rem; height: 1.5rem; flex: none;
  fill: none; stroke: var(--link); stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round;
}

/* Sidebar */
aside { font-size: 0.9rem; }
.box { background: var(--panel); border-radius: 8px; padding: 0.9rem 1.1rem; margin-bottom: 1rem; }
.box h2 { font-size: 0.95rem; margin: 0 0 0.5rem; }
.box p { margin: 0 0 0.5rem; }
.box ul { margin: 0.4rem 0 0; padding-left: 1.1rem; }
.box details { margin-top: 0.6rem; }
.box summary { cursor: pointer; color: var(--link); }
.box pre { background: var(--bg); font-size: 0.72rem; white-space: pre-wrap; word-break: break-all; }
.stats, .pagemenu { list-style: none; padding: 0 !important; }
.stats li, .pagemenu li { padding: 0.15rem 0; }
.pagemenu .current { color: var(--fg); font-weight: 600; }
.prevnext { display: flex; justify-content: space-between; gap: 1rem; margin-bottom: 1rem; }
.prevnext .next { text-align: right; }
.tagbox .tagline { font-size: 1.05rem; margin-bottom: 0.5rem; }
.tag {
  font-weight: 700; letter-spacing: 0.04em;
  background: var(--bg); border: 1px solid var(--line); border-radius: 4px; padding: 0.08rem 0.4rem;
}
.tagbox dl { margin: 0; display: grid; grid-template-columns: auto 1fr; gap: 0.15rem 0.7rem; }
.tagbox dt { color: var(--muted); }
.tagbox dd { margin: 0; overflow-wrap: anywhere; }

/* Bibliography */
.bib { list-style: none; padding: 0; margin: 0; }
.bib li { display: grid; grid-template-columns: 7.5rem minmax(0, 1fr); gap: 0.8rem; padding: 0.55rem 0.4rem; border-radius: 4px; }
.bib li:target { background: var(--ref); }
.bib .key { font-family: var(--sans); font-size: 0.9rem; font-weight: 600; overflow-wrap: anywhere; }
@media (max-width: 560px) { .bib li { grid-template-columns: 1fr; gap: 0.1rem; } }

/* Search */
#results { margin-top: 1.2rem; }
.result { padding: 0.8rem 0; border-top: 1px solid var(--line); }
.result .head { font-family: var(--sans); font-weight: 600; }
.result .where { font-family: var(--sans); font-size: 0.82rem; color: var(--muted); margin-left: 0.5rem; }
.result p { margin: 0.25rem 0 0; font-size: 0.97rem; }
.count { font-family: var(--sans); font-size: 0.88rem; color: var(--muted); margin: 0 0 0.6rem; }