:root {
  --bg: #fdfdfb; --fg: #1f2328; --muted: #6b7280; --line: #d9dce1;
  --accent: #2f5fa7; --lemma-bg: #f3f6fb; --fold-bg: #f6f7f9;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #17191c; --fg: #e6e6e6; --muted: #9aa0a6; --line: #34383e;
    --accent: #8fb4ec; --lemma-bg: #1e242d; --fold-bg: #1f2226;
  }
}
:root[data-theme="dark"] {
  --bg: #17191c; --fg: #e6e6e6; --muted: #9aa0a6; --line: #34383e;
  --accent: #8fb4ec; --lemma-bg: #1e242d; --fold-bg: #1f2226;
}
body {
  background: var(--bg); color: var(--fg);
  font-family: "Hiragino Sans", "Yu Gothic UI", "Meiryo", sans-serif;
  line-height: 1.8; margin: 0; padding: 24px 16px 80px;
}
a { color: var(--accent); }

.layout {
  display: grid; grid-template-columns: 210px minmax(0, 980px) 270px;
  gap: 36px; justify-content: center; align-items: start;
}
.side { position: sticky; top: 16px; max-height: calc(100vh - 32px); overflow-y: auto; font-size: .85rem; line-height: 1.6; }
.side h4 { font-size: .8rem; color: var(--muted); margin: 0 0 .6em; letter-spacing: .05em; }
.toc ul { list-style: none; padding: 0; margin: 0; }
.toc li { margin: .25em 0; }
.toc li.page { margin-top: .7em; font-weight: bold; }
.toc li.page.current > a { color: var(--accent); }
.toc li.sub { padding-left: 1em; }
.toc li.sub2 { padding-left: 2em; }
.toc a { color: var(--fg); text-decoration: none; }
.toc a:hover { color: var(--accent); text-decoration: underline; }
.defs dl { margin: 0; }
.defs dt { font-weight: bold; color: var(--accent); margin-top: .9em; }
.defs dd { margin: .2em 0 0; }
.defs dd .katex { font-size: 1em; }
.defs dt:target, .defs dt:target + dd { background: var(--lemma-bg); }
@media (max-width: 1250px) {
  .layout { grid-template-columns: minmax(0, 1fr); }
  .side { position: static; max-height: none; }
  .toc { order: -1; }
}

h1 { font-size: 1.6rem; border-bottom: 2px solid var(--line); padding-bottom: .3em; margin-top: 0; }
h2 { font-size: 1.3rem; margin-top: 2em; }
h3 { font-size: 1.1rem; margin: 0 0 .3em; color: var(--accent); }
.src { color: var(--muted); font-size: .9rem; }

.problem { margin-top: 2.5em; scroll-margin-top: 16px; }
.problem .goal { margin: .2em 0; }
.problem .ask { margin: 0 0 .2em; }
.problem .setup { margin: .2em 0; }
.problem .remark { margin: 0; color: var(--muted); font-size: .92rem; }
details.fold { margin-top: .7em; border: 1px solid var(--line); border-radius: 6px; }
details.fold > summary { cursor: pointer; padding: .45em .9em; font-weight: bold; background: var(--fold-bg); border-radius: 6px; }
details.fold[open] > summary { border-bottom: 1px solid var(--line); border-radius: 6px 6px 0 0; }
details.fold > .fold-body { padding: .3em .9em .8em; }
details.used dl { margin: .3em 0 0; display: grid; grid-template-columns: max-content 1fr; gap: .5em 1.5em; align-items: baseline; }
details.used dt { font-weight: bold; color: var(--accent); font-size: .92rem; }
details.used dd { margin: 0; }

.deriv { border-collapse: collapse; margin: .5em 0; width: 100%; table-layout: fixed; }
.deriv td { padding: .5em .4em; vertical-align: middle; border: none; }
.deriv td.lhs { text-align: right; white-space: nowrap; width: 5em; }
.deriv td.eq  { text-align: center; width: 2em; }
.deriv td.rhs { text-align: left; white-space: nowrap; width: 18em; padding-right: 1.5em; }
.deriv td.why { text-align: left; font-size: .92rem; line-height: 1.7; }
.deriv tr.uses-lemma > td { vertical-align: top; }
.deriv.therefore { margin-top: 1.2em; }
.deriv.wide-lhs td.lhs { width: 11.5em; }

details.lemma { margin-top: .4em; background: var(--lemma-bg); border-left: 3px solid var(--accent); border-radius: 4px; }
details.lemma > summary { cursor: pointer; padding: .3em .7em; color: var(--accent); font-weight: bold; }

tr.lemma-proof > td { padding-top: 0; }
.lemma-body { background: var(--lemma-bg); border-left: 3px solid var(--accent); border-radius: 4px; padding: .3em .6em .6em; overflow-x: auto; }
.lemma-body .deriv td.lhs { width: auto; }
.lemma-body .deriv td.rhs { width: auto; padding-right: .8em; }
.lemma-body .deriv { table-layout: auto; font-size: .9rem; }
.lemma-body .deriv td.why { min-width: 14em; }
.qed { text-align: right; margin: .2em 0 0; }

.scroll { overflow-x: auto; }

.index-list { list-style: none; padding: 0; }
.index-list > li { margin: 1em 0; }
.index-list > li > a { font-size: 1.1rem; font-weight: bold; }
.index-list ul { margin: .3em 0 0; padding-left: 1.4em; }

.ref { color: var(--accent); border-bottom: 1px dotted var(--accent); cursor: help; }
.ref:focus { outline: 2px solid var(--accent); outline-offset: 1px; border-radius: 2px; }
.ref > .pop { display: none; }
.ref-pop {
  position: absolute; z-index: 100; max-width: min(28em, calc(100vw - 32px));
  background: var(--bg); color: var(--fg); border: 1px solid var(--line); border-left: 3px solid var(--accent);
  border-radius: 6px; box-shadow: 0 4px 16px rgba(0,0,0,.15); padding: .5em .9em; font-size: .9rem; line-height: 1.6;
}
.ref-pop .katex-display { margin: .4em 0; }

.pt-overlay {
  position: fixed; inset: 0; z-index: 1000; display: flex; align-items: center; justify-content: center;
  background: var(--bg); opacity: 0; transition: opacity .35s ease; pointer-events: none;
}
.pt-overlay.pt-show { opacity: 1; pointer-events: auto; }
.pt-card { text-align: center; line-height: 1.5; }
.pt-from { color: var(--muted); font-size: .95rem; }
.pt-to { color: var(--accent); font-size: 1.3rem; font-weight: bold; }
.pt-label { color: var(--muted); font-size: .9rem; margin-top: .3em; }
.pt-arrow { width: 2px; height: 3em; margin: .5em auto; background: var(--line); position: relative; overflow: hidden; }
.pt-arrow span { position: absolute; left: 0; top: -100%; width: 100%; height: 100%; background: var(--accent); }
.pt-show .pt-arrow span { animation: pt-flow .5s ease forwards; }
@keyframes pt-flow { to { top: 0; } }
@media (prefers-reduced-motion: reduce) {
  .pt-overlay { transition: none; }
  .pt-show .pt-arrow span { animation: none; top: 0; }
}

main.home { max-width: 760px; margin: 0 auto; }

.dev-note { display: inline-block; margin-left: .3em; padding: 0 .4em; font-size: .8rem; color: #8a5a00; background: #fff4d6; border-radius: 3px; }