/* The blueprint's own style, on top of plasTeX's white theme, leanblueprint and the
   dependency graph plugin. System fonts only: the site loads no font files.
   Colours are variables. The site is light only, whatever the reader's system scheme (Carlo, 2026-10-02). */

:root {
  --bg: #faf7f0;            /* warm off-white page */
  --bg-side: #f3eee3;       /* sidebar */
  --bg-raised: #fffdf8;     /* modals, popups */
  --ink: #1f1c17;           /* near-black text */
  --ink-muted: #5c564c;
  --rule: #e2dbcd;
  --hover: #ebe4d6;
  --accent: #0f766e;        /* deep teal */
  --accent-strong: #0b5c55;
  --accent-soft: #e2efe9;
  --card-bg: #eff3ec;       /* page colour tinted with the accent */
  --card-rule: #d9e3d9;
  --chip-bg: #ebe5d9;
  --chip-ink: #2a2620;
  --ok-bg: #dcefe0;
  --ok-ink: #1d5a33;
  --graph-bg: #fdfcf9;      /* the graph's ground */
  --shadow: 0 1px 2px rgba(31, 28, 23, .06), 0 8px 24px rgba(31, 28, 23, .10);
  --serif: ui-serif, "New York", Charter, "Iowan Old Style", Georgia, serif;
  --sans: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
  --mono: ui-monospace, SFMono-Regular, Menlo, Consolas, "Liberation Mono", monospace;
  color-scheme: light;
}

/* --- Page --------------------------------------------------------------------------- */

body {
  background: var(--bg);
  color: var(--ink);
  font-family: var(--serif);
}

::selection { color: var(--bg); background: var(--accent); }

div.wrapper, div.content { background: var(--bg); }

div.content { padding: 2rem 2.5rem 4rem; }

div.content-wrapper {
  width: 100%;
  max-width: 44rem;
  margin-left: auto;
  margin-right: auto;
}

div.main-text {
  font-size: 1.125rem;
  line-height: 1.6;
}

div.main-text p,
div.main-text li,
div.main-text dd { font-size: 1em; }

div.main-text p { margin: 0 0 .9em; }

div.main-text ul,
div.main-text ol { font-size: 1em; padding-left: 1.4em; margin: 0 0 .9em; }

div.main-text li > p { margin: .2em 0; }

a { color: var(--accent); text-decoration-thickness: 1px; text-underline-offset: .15em; }
a:hover { color: var(--accent-strong); }
div.main-text a { text-decoration: none; }
div.main-text a:hover { text-decoration: underline; }

code, kbd, pre, samp, .texttt, .ttfamily, tt {
  font-family: var(--mono);
  font-size: .88em;
  overflow-wrap: anywhere;
}

/* Headings: system sans, in clear weight steps. */
h1, h2, h3, h4, h5, h6,
div.main-text h1, div.main-text h2, div.main-text h3 {
  font-family: var(--sans);
  color: var(--ink);
  line-height: 1.25;
}

/* plasTeX sets the chapter title and its sections all as h1: the first is the chapter. */
div.main-text > h1:first-child {
  font-size: 2rem;
  font-weight: 700;
  letter-spacing: -.015em;
  margin: .25rem 0 1.25rem;
}

div.main-text > h1:not(:first-child),
div.main-text h2 {
  font-size: 1.375rem;
  font-weight: 650;
  letter-spacing: -.005em;
  margin: 3rem 0 1rem;
  padding-top: 1.25rem;
  border-top: 1px solid var(--rule);
}

div.main-text h3 { font-size: 1.125rem; font-weight: 600; margin: 2rem 0 .75rem; }

/* MathJax keeps its own output; long displays scroll instead of widening the page. */
div.displaymath, mjx-container[display="true"] {
  max-width: 100%;
  overflow-x: auto;
  overflow-y: hidden;
}

/* --- Header ------------------------------------------------------------------------- */

body > header {
  position: sticky;
  top: 0;
  z-index: 10;
  flex: none;
  display: flex;
  align-items: center;
  gap: .75rem;
  height: 3.25rem;
  padding: 0 1rem;
  background: var(--bg);
  border-bottom: 1px solid var(--rule);
  color: var(--ink);
  font-family: var(--sans);
}

svg#toc-toggle {
  flex: none;
  width: 1.1rem;
  height: 1.1rem;
  margin: 0;
  color: var(--ink-muted);
  cursor: pointer;
}

h1#doc_title {
  flex: 1 1 auto;
  min-width: 0;
  margin: 0;
  color: var(--ink);
  font-family: var(--sans);
  font-size: 1rem;
  font-weight: 650;
  letter-spacing: -.005em;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}

#doc_title a, #doc_title a:visited { color: var(--ink); text-decoration: none; }

nav.site-links { flex: none; display: flex; gap: .25rem; margin-left: auto; }

nav.site-links a {
  padding: .3rem .65rem;
  border-radius: 6px;
  font-size: .875rem;
  font-weight: 500;
  color: var(--ink-muted);
  text-decoration: none;
}

nav.site-links a:hover { background: var(--hover); color: var(--ink); }

nav.site-links .short { display: none; }

/* --- Sidebar contents ---------------------------------------------------------------- */

nav.toc {
  width: 17.5rem;
  max-width: 17.5rem;
  margin: 0;
  padding: 1.25rem .75rem 4rem;
  background: var(--bg-side);
  border-right: 1px solid var(--rule);
  font-family: var(--sans);
}

.toc ul li,
.toc ul li.current { background: transparent; font-weight: 400; }

.toc ul li { flex-wrap: wrap; border-radius: 6px; }
.toc ul li > a { flex: 1 1 0; min-width: 0; }
/* Entry numbers as a column, so that long titles wrap under the title. */
.toc ul a, .local_toc ul a { display: flex; align-items: baseline; }
.toc span.toc_ref, .local_toc span.toc_ref { flex: none; }
.toc span.toc_entry, .local_toc span.toc_entry { flex: 1 1 auto; min-width: 0; }
.toc ul li > ul { flex: 0 0 100%; }

.toc ul a {
  max-width: none;
  padding: .4rem .6rem;
  border-radius: 6px;
  font-size: .9rem;
  line-height: 1.35;
  color: var(--ink-muted);
}

.toc ul a:hover { background: var(--hover); color: var(--ink); }

.toc span.toc_ref {
  display: inline-block;
  min-width: 1.6rem;
  font-variant-numeric: tabular-nums;
  color: var(--ink-muted);
}

.toc ul li.active > a { color: var(--ink); font-weight: 600; }

.toc ul li.current > a {
  color: var(--accent-strong);
  font-weight: 650;
  background: var(--accent-soft);
  box-shadow: inset 3px 0 0 var(--accent);
}

.toc ul li.current > a span.toc_ref { color: var(--accent-strong); }

.toc .sub-toc-0 a { padding-left: .6rem; }
.toc .sub-toc-1 a { padding-left: 2.2rem; font-size: .84rem; }
.toc .sub-toc-2 a { padding-left: 3rem; font-size: .82rem; }
.toc .sub-toc-1 span.toc_ref { min-width: 2rem; }

span.expand-toc {
  flex: none;
  padding: 0 .35rem 0 0;
  font-size: .7rem;
  color: var(--ink-muted);
}

/* --- Theorems as cards, proofs quieter ---------------------------------------------- */

div[class*="_thmwrapper"] {
  margin: 2rem 0 .6rem;
  padding: .85rem 1.15rem 1rem;
  background: var(--card-bg);
  border: 1px solid var(--card-rule);
  border-left: 4px solid var(--accent);
  border-radius: 10px;
}

div[class*="_thmwrapper"]:target { animation: none; box-shadow: 0 0 0 3px var(--accent-soft); }

div[class*="_thmheading"] {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: .35rem .5rem;
  margin: 0 0 .65rem;
  padding-bottom: .55rem;
  border-bottom: 1px solid var(--card-rule);
  font-family: var(--sans);
  font-size: .95rem;
  font-weight: 600;
  line-height: 1.35;
  font-style: normal;
}

span[class*="_thmcaption"],
span[class*="_thmlabel"] {
  color: var(--accent-strong);
  font-size: .78rem;
  font-weight: 700;
  letter-spacing: .06em;
  text-transform: uppercase;
}

span[class*="_thmlabel"] { margin: 0 .2rem 0 -.2rem; font-variant-numeric: tabular-nums; }

div.theorem-style-plain span[class*="_thmlabel"]::after,
div.theorem-style-definition span[class*="_thmlabel"]::after { content: none; }

span[class*="_thmtitle"] { color: var(--ink); font-weight: 600; }
span[class*="_thmtitle"]::before,
span[class*="_thmtitle"]::after { content: none; }

/* Statements upright: the card already sets them apart. */
div[class*="_thmcontent"],
div.theorem-style-plain div[class*="_thmcontent"] {
  margin: 0;
  padding: 0;
  border: 0;
  font-style: normal;
}

div[class*="_thmcontent"] > p:last-child { margin-bottom: 0; }

/* The attribution under a statement. */
div[class*="_thmcontent"] small.small {
  display: block;
  margin-top: .75rem;
  padding-top: .55rem;
  border-top: 1px dashed var(--card-rule);
  font-size: .82em;
  line-height: 1.5;
  color: var(--ink-muted);
}

div[class*="_thmcontent"] small.small > em:first-child {
  font-family: var(--sans);
  font-style: normal;
  font-size: .78em;
  font-weight: 700;
  letter-spacing: .06em;
  text-transform: uppercase;
  color: var(--ink-muted);
  margin-right: .25em;
}

/* Status and Lean badges, at the end of the heading. */
div.thm_header_extras {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  min-width: 1.45rem;
  height: 1.45rem;
  margin-left: auto;
  padding: 0 .35rem;
  border-radius: 999px;
  background: var(--ok-bg);
  color: var(--ok-ink);
  font-size: .8rem;
  font-weight: 700;
  line-height: 1;
}

div.thm_header_hidden_extras,
div[class*="_thmheading"]:hover div.thm_header_hidden_extras {
  display: inline-flex;
  align-items: center;
  gap: .3rem;
}

div.thm_header_hidden_extras a.icon {
  order: 2;
  opacity: 0;
  padding: 0 .15rem;
  font-weight: 400;
  color: var(--ink-muted);
  transition: opacity .15s ease;
}

div[class*="_thmheading"]:hover a.icon,
div.thm_header_hidden_extras a.icon:focus-visible { opacity: 1; }

div.thm_header_hidden_extras a.icon svg { width: .85rem; height: .85rem; vertical-align: -.1rem; }

button.modal.lean {
  order: 1;
  padding: .18rem .5rem;
  border: 1px solid var(--rule);
  border-radius: 6px;
  background: var(--chip-bg);
  color: var(--chip-ink);
  font-family: var(--mono);
  font-size: .74rem;
  font-weight: 600;
  line-height: 1.2;
  cursor: pointer;
}

button.modal.lean:hover { border-color: var(--accent); color: var(--accent-strong); }

/* Proofs: no card, a small label, indented. */
div.proof_wrapper { margin: .35rem 0 1.75rem 1.25rem; }

div.proof_heading {
  display: inline-flex;
  align-items: center;
  gap: .4rem;
  font-family: var(--sans);
  font-size: .75rem;
  font-weight: 700;
  letter-spacing: .08em;
  text-transform: uppercase;
  color: var(--ink-muted);
  cursor: pointer;
}

div.proof_heading:hover { color: var(--accent-strong); }
span.expand-proof { font-size: .65rem; }

div.proof_content {
  margin: .35rem 0 0;
  padding: 0 0 0 .95rem;
  border-left: 2px solid var(--rule);
  font-size: .97em;
}

div.proof_content > p:last-child { margin-bottom: 0; }
span.qed { color: var(--ink-muted); }

/* The Lean declarations dialog. */
div.modal-container { background: rgba(20, 18, 15, .35); align-items: center; padding: 1rem; }

div.modal-content {
  max-width: 34rem;
  width: 100%;
  overflow: hidden;
  border: 1px solid var(--rule);
  border-radius: 12px;
  background: var(--bg-raised);
  box-shadow: var(--shadow);
  font-family: var(--sans);
}

div.modal-content header {
  min-height: 0;
  padding: .7rem 1rem;
  background: var(--bg-raised);
  border-bottom: 1px solid var(--rule);
  color: var(--ink);
  text-align: left;
}

div.modal-content header h1 { margin: 0; padding: 0; font-size: .95rem; font-weight: 650; color: var(--ink); }
div.modal-content header button.closebtn { color: var(--ink-muted); }
div.modal-content ul { padding: .6rem 1rem 1rem; margin: 0; }
div.modal-content li { padding: .2rem 0; font-size: .9rem; }

div.modal-content a.lean_decl, ul.uses a {
  font-family: var(--mono);
  font-size: .85rem;
  overflow-wrap: anywhere;
}

/* --- Bottom navigation -------------------------------------------------------------- */

nav.prev_up_next {
  right: 1rem;
  bottom: 1rem;
  height: auto;
  padding: .15rem .35rem;
  border: 1px solid var(--rule);
  border-radius: 999px;
  background: var(--bg-raised);
  box-shadow: var(--shadow);
  align-items: center;
}

nav.prev_up_next a {
  display: inline-flex;
  margin: 0;
  padding: .45rem .55rem;
  font-size: 1rem;
  color: var(--ink-muted);
  text-shadow: none;
}

nav.prev_up_next svg.icon { width: 1rem; height: 1rem; min-width: 0; padding: 0; cursor: pointer; }
nav.prev_up_next svg.showmore { width: 1.1rem; height: 1.1rem; margin: 0 .45rem; color: var(--ink-muted); text-shadow: none; }
nav.prev_up_next a:hover, nav.prev_up_next svg.showmore:hover { color: var(--accent-strong); }

/* --- Landing page ------------------------------------------------------------------- */

.titlepage { text-align: left; margin: 1.5rem 0 0; }

.titlepage h1 {
  margin: 0 0 .5rem;
  font-size: clamp(2rem, 1.2rem + 3vw, 2.75rem);
  font-weight: 750;
  letter-spacing: -.025em;
  line-height: 1.1;
}

.titlepage p.authors { margin: 0 0 1.25rem; font-family: var(--sans); font-size: .95rem; color: var(--ink-muted); }

.titlepage + p { font-size: 1.25em; line-height: 1.5; color: var(--ink); margin-bottom: 1.25rem; }

.titlepage + p + ul.itemize {
  display: flex;
  flex-wrap: wrap;
  gap: .5rem;
  margin: 0 0 2.5rem;
  padding: 0;
  list-style: none;
}

.titlepage + p + ul.itemize li {
  padding: .3rem .8rem;
  border: 1px solid var(--card-rule);
  border-radius: 999px;
  background: var(--accent-soft);
  color: var(--accent-strong);
  font-family: var(--sans);
  font-size: .85rem;
  font-weight: 600;
}

.titlepage + p + ul.itemize li > p { margin: 0; }

nav.local_toc {
  max-width: 44rem;
  margin: 0 auto 4rem;
  padding: 1rem 1.25rem;
  border: 1px solid var(--rule);
  border-radius: 12px;
  background: var(--bg-raised);
  font-family: var(--sans);
}

.local_toc ul { padding-left: 0; margin: 0; }
.local_toc ul ul { padding-left: 1.6rem; margin: .15rem 0 .35rem; }
.local_toc ul li { padding: .3rem 0; }
.local_toc ul ul li { padding: .15rem 0; }
.local_toc ul a { color: var(--ink); font-weight: 600; font-size: 1rem; }
.local_toc ul ul a { color: var(--ink-muted); font-weight: 400; font-size: .9rem; }
.local_toc ul a:hover { color: var(--accent-strong); }
.local_toc span.toc_ref { display: inline-block; min-width: 2rem; color: var(--accent-strong); font-variant-numeric: tabular-nums; }

/* --- Citations and references ------------------------------------------------------- */

span.cite { white-space: nowrap; }
dl.bibliography dt { margin-top: 1rem; font-family: var(--sans); font-weight: 650; font-size: .9rem; }
dl.bibliography dd { margin-left: 0; padding-left: 1.25rem; }
dl.bibliography dd p { margin: .2rem 0 0; }

/* --- Dependency graph page ---------------------------------------------------------- */

body > header a.toc {
  flex: none;
  margin-right: 0;
  padding: .3rem .65rem;
  border-radius: 6px;
  font-size: .875rem;
  font-weight: 500;
  color: var(--ink-muted);
  text-decoration: none;
}

body > header a.toc:hover { background: var(--hover); color: var(--ink); }

/* The graph page needs no link to itself. */
body > header a.toc ~ nav.site-links a[href="dep_graph_document.html"] { display: none; }

body > header a.toc + h1#doc_title {
  position: absolute;
  left: 50%;
  transform: translateX(-50%);
  width: auto;
  overflow: visible;
}

#Legend { position: relative; z-index: 3; margin: 0 0 .75rem; font-family: var(--sans); }

#Legend span.title {
  display: inline-flex;
  align-items: center;
  gap: .4rem;
  margin: 0;
  padding: .3rem .7rem;
  border: 1px solid var(--rule);
  border-radius: 999px;
  background: var(--bg-raised);
  font-size: .85rem;
  font-weight: 600;
  color: var(--ink);
}

#Legend div.btn { margin: 0; }
#Legend div.bar { width: 14px; height: 2px; margin: 2px 0; background: var(--ink-muted); }

#Legend dl {
  top: 2.6rem;
  left: 0;
  max-width: min(32rem, 90vw);
  padding: .75rem 1rem;
  border: 1px solid var(--rule);
  border-radius: 12px;
  background: var(--bg-raised);
  box-shadow: var(--shadow);
  font-size: .85rem;
  line-height: 1.5;
  color: var(--ink);
}

#Legend dt { font-weight: 650; }

div#graph {
  height: calc(100vh - 8rem);
  border: 1px solid var(--rule);
  border-radius: 12px;
  background: var(--graph-bg);
  color-scheme: light;
}

div.dep-modal-container { z-index: 20; }

div.dep-modal-content {
  position: relative;
  max-width: 44rem;
  margin: 0 auto;
  padding: 1rem 1.25rem 1rem;
  border: 1px solid var(--rule);
  border-radius: 12px;
  background: var(--bg-raised);
  box-shadow: var(--shadow);
  color: var(--ink);
  font-size: 1.05rem;
  line-height: 1.55;
}

div.dep-modal-content div.thm_thmheading {
  display: flex;
  flex-wrap: wrap;
  gap: .35rem .5rem;
  margin-bottom: .5rem;
  padding-right: 2rem;
  font-family: var(--sans);
  font-size: .95rem;
  font-weight: 600;
}

div.dep-modal-content div.thm_thmcontent { margin: 0 0 .75rem; padding: 0; font-family: var(--serif); }
button.dep-closebtn { top: .75rem; right: .75rem; color: var(--ink-muted); }

a.latex_link, a.lean_link, a.issue_link, .tooltip span.lean_link {
  display: inline-block;
  margin: 0 .35rem 0 0;
  padding: .18rem .55rem;
  border: 1px solid var(--rule);
  border-radius: 6px;
  background: var(--chip-bg);
  color: var(--chip-ink);
  font-family: var(--mono);
  font-size: .78rem;
  font-style: normal;
  font-weight: 600;
}

div.dep-modal-content a.latex_link, div.dep-modal-content a.lean_link { color: var(--chip-ink); }

ul.tooltip_list { border-color: var(--rule); background: var(--bg-raised); }

/* --- Narrow screens ----------------------------------------------------------------- */

@media (max-width: 1023px) {
  nav.toc { width: 100%; max-width: none; padding: 1rem; border-right: 0; }
  div.content { padding: 1.5rem 1rem 5rem; }
}

@media (max-width: 640px) {
  body > header { gap: .5rem; padding: 0 1rem; }
  nav.site-links { gap: 0; }
  nav.site-links a { padding: .3rem .45rem; }
  nav.site-links .long { display: none; }
  nav.site-links .short { display: inline; }
  div.main-text { font-size: 1.0625rem; }
  div.main-text h1 { font-size: 1.6rem; }
  div[class*="_thmwrapper"] { padding: .75rem .85rem .9rem; border-radius: 8px; }
  div.thm_header_extras { margin-left: 0; }
  div.proof_wrapper { margin-left: .5rem; }
  body > header a.toc + h1#doc_title { position: static; transform: none; }
  #Legend dl { max-width: calc(100vw - 2rem); }
}