/* Generated by autoform render. Edits are overwritten. */
/* Material requests 300/400/700 only, and the display sizes here are set in
   600 and 800. Without this the browser synthesises them, which on a
   geometric face reads as smeared rather than bold. */
@import url("https://fonts.googleapis.com/css2?family=Plus+Jakarta+Sans:wght@400;500;600;700;800&display=swap");

/* Facebook's product surfaces, not Material's defaults: the greys are the
   ones Facebook ships in dark mode and the blue is Meta blue, which light
   mode's links share with the status strokes. The brand gradient stays off
   the figures, the progress bar and the header. Dark mode's link blue is
   lighter than its status blue, so links keep 4.5:1 on every surface.
   A blueprint should look like it came from here rather than from any
   documentation generator. */
:root {
  --bp-fg: #050505;
  --bp-muted: #65676B;
  --bp-rule: #CED0D4;
  --bp-surface: #FFFFFF;
  --bp-sunken: #F0F2F5;
  --bp-page: #FFFFFF;
  --bp-scroll-shade: rgba(5, 5, 5, 0.22);
  --bp-link: #0064E0;
  --bp-link-hover: #0082FB;
  --bp-blue: #0064E0;
  --bp-radius: 12px;
}
[data-md-color-scheme=slate] {
  --bp-fg: #E4E6EB;
  --bp-muted: #B0B3B8;
  --bp-rule: #3E4042;
  --bp-surface: #242526;
  --bp-sunken: #1C1D1F;
  --bp-page: #18191A;
  --bp-scroll-shade: rgba(228, 230, 235, 0.3);
  --bp-link: #4A9AFF;
  --bp-link-hover: #7FB8FF;
  --bp-blue: #2D88FF;
}
/* Material's own tokens take the same blue, so its links and breadcrumbs
   match the explorer instead of the theme's default indigo.
   The theme sets them on body through data-md-color-primary, and the slate
   link colour through two attributes, so this selector carries two
   attributes and wins by coming later. The bp tokens already switch with
   the scheme, so one rule covers both. The darker and lighter shades follow,
   or the drawer's repository strip and hover tints stay indigo. */
[data-md-color-scheme][data-md-color-primary] {
  --md-primary-fg-color: var(--bp-blue);
  --md-primary-fg-color--light: color-mix(in srgb, var(--bp-blue) 80%, #FFFFFF);
  --md-primary-fg-color--dark: color-mix(in srgb, var(--bp-blue) 80%, #000000);
  --md-accent-fg-color: var(--bp-link-hover);
  --md-accent-fg-color--transparent: color-mix(in srgb, var(--bp-link-hover) 10%, transparent);
  --md-typeset-a-color: var(--bp-link);
}
/* White on the accent is 2.1:1 in slate and 3.8:1 in light, and the
   back-to-top button shows focus only by that fill. Slate's accent takes the
   page's near-black text; light's button fills with the link blue. */
[data-md-color-scheme=slate][data-md-color-accent] { --md-accent-bg-color: #18191A; }
[data-md-color-scheme=default] .md-top:is(:hover, :focus) { background-color: var(--bp-link); }

body { font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; color: var(--bp-fg); }
.md-typeset {
  max-width: 72ch;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  line-height: 1.7;
  font-size: 0.8rem;
}
/* One family throughout, separated by weight rather than by a second face.
   Optimistic, Meta's own, is not public; Plus Jakarta Sans is the nearest
   geometric humanist with the range to carry both display and body. */
h1, h2, h3, h4, h5, h6 { font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; font-weight: 700; letter-spacing: -0.021em; }
.md-typeset h1 { font-weight: 800; letter-spacing: -0.032em; }
code, kbd, pre, samp { font-family: "JetBrains Mono", ui-monospace, SFMono-Regular, Menlo, monospace; }
code, pre { background: var(--bp-sunken); border-radius: 6px; }
a, a:visited { color: var(--bp-link); }
a:hover, a:visited:hover { color: var(--bp-link-hover); text-decoration: underline; }

[data-md-color-scheme=slate] body { background-color: #18191A; }
[data-md-color-scheme=slate] .md-main,
[data-md-color-scheme=slate] .md-container { background-color: #18191A; }
/* A book page shows only its background until its boot script hands it to the book's frame, which takes the place of
   Material's header and sidebars: without this they show for a moment first. A page without the book shows once its
   content starts, and a book page whose script never runs shows after three seconds. */
@media screen and (scripting: enabled) {
  body:not(.bp-book, :has(.md-content))::before,
  body:not(.bp-book):has(.bp-book-frame)::before {
    content: ""; position: fixed; z-index: 39; inset: 0; background: var(--bp-surface);
    animation: bp-book-uncover 0s 3s forwards;
  }
}
@keyframes bp-book-uncover { to { visibility: hidden; } }
[data-md-color-scheme=slate] pre, [data-md-color-scheme=slate] code { color: var(--bp-fg); }

.md-header { box-shadow: 0 2px 6px rgba(0, 0, 0, 0.35); border-bottom: 1px solid var(--bp-rule); }
/* The mobile drawer's title bar and repository strip match the header:
   white on slate's brighter blue is 3.5:1. */
[data-md-color-scheme=slate] .md-header,
[data-md-color-scheme=slate] .md-tabs,
[data-md-color-scheme=slate] .md-nav--primary .md-nav__title[for=__drawer],
[data-md-color-scheme=slate] .md-nav__source { background-color: #242526; }
.md-tabs { border-bottom: 1px solid var(--bp-rule); }
.md-tabs__link { font-size: 0.72rem; font-weight: 600; opacity: 0.9; margin-top: 0; }
.md-tabs__link--active, .md-tabs__link:hover { opacity: 1; }

/* The landing page is a dashboard, not a chapter, so it drops the reading
   column the rest of the book keeps. :has() is how a single generated
   stylesheet can tell the two apart without a second page template; where it
   is unsupported the page simply stays at reading width. */
.md-typeset:has(.bp-landing) { max-width: 62rem; }
/* The explorer's reading pane sets its own width. Only running text keeps the
   reading measure, so tables, code and cards use the pane's width, up to the
   880px column a wide reader keeps (blueprint-dag.css). The pane's article
   holds the page's reading source, whose children are the text. */
.bp-reading-body.md-typeset { max-width: none; }
.bp-reading-body > .bp-reading-source > :is(p, ul, ol, dl, blockquote) { max-width: 72ch; }

.bp-hero { margin: 0 0 2.5rem; }
.bp-hero-kicker {
  margin-top: 1.1rem;
  font-size: 0.68rem;
  font-weight: 600;
  color: var(--bp-muted);
}
.md-typeset .bp-hero-title {
  margin: 0.35rem 0 0;
  font-size: 2.6rem;
  line-height: 1.08;
  font-weight: 800;
  letter-spacing: -0.035em;
}
.md-typeset .bp-hero-lead {
  margin: 0.9rem 0 0;
  max-width: 54ch;
  font-size: 1.05rem;
  line-height: 1.55;
  color: var(--bp-muted);
}

/* Counts set as figures. The reader should get "how far along?" from the
   shape of the numbers before reading any of the words around them. */
.bp-hero-figures {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(160px, 1fr));
  gap: 1px;
  margin-top: 2rem;
  background: var(--bp-rule);
  border: 1px solid var(--bp-rule);
  border-radius: var(--bp-radius);
  overflow: hidden;
}
.bp-figure { padding: 1.1rem 1.25rem; background: var(--bp-surface); }
.bp-figure-value {
  font-size: 2.1rem;
  font-weight: 800;
  line-height: 1;
  letter-spacing: -0.04em;
  color: var(--bp-fg);
}
.bp-figure-neutral .bp-figure-value { color: var(--bp-muted); }
.bp-figure-label {
  margin-top: 0.45rem;
  font-size: 0.78rem;
  font-weight: 700;
  letter-spacing: 0.01em;
}
.bp-figure-note { margin-top: 0.15rem; font-size: 0.7rem; color: var(--bp-muted); }
/* The ready figure opens the list of what it counts; it keeps the figure's
   colours, and an arrow after its label shows it is a link, as on
   "Start reading". Hover or focus underlines the label. */
.md-typeset a.bp-figure-link,
.md-typeset a.bp-figure-link:is(:visited, :hover, :focus-visible) { color: var(--bp-fg); text-decoration: none; }
.bp-figure-link > span { display: block; }
.md-typeset a.bp-figure-link:is(:hover, :focus-visible) .bp-figure-label { text-decoration: underline; }
/* The arrow is decoration, so it stays out of the link's accessible name where
   the browser supports alt text. The figures clip overflow, so the focus ring
   is drawn inside the cell. */
.bp-figure-link .bp-figure-label::after { content: " →"; content: " →" / ""; }
.md-typeset a.bp-figure-link:focus-visible { outline-offset: -2px; }
/* With no figures, or all statements fully proved, this one sentence is the
   hero's status, so it is set at the claim's size. */
.md-typeset .bp-hero-status { margin: 1rem 0 0; color: var(--bp-fg); font-size: 1.05rem; font-weight: 600; }

.bp-hero-bar {
  margin-top: 1rem;
  height: 6px;
  border-radius: 6px;
  background: var(--bp-sunken);
  border: 1px solid var(--bp-rule);
  overflow: hidden;
}
.bp-hero-bar > span { display: block; height: 100%; }

.bp-hero-coverage {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.2rem 0.65rem;
  margin-top: 0.75rem;
  font-size: 0.72rem;
  color: var(--bp-muted);
}
.bp-hero-coverage-links { margin-left: auto; }
.bp-hero-coverage-link,
.bp-hero-sources-link {
  font-weight: 600;
  text-decoration: underline;
  text-underline-offset: 0.15em;
}
.bp-hero-sources-link { margin-left: 0.65rem; }

/* On the landing page the hero sits in the explorer's reading pane, or its
   sheet on phones, so it is set, like the pane's chapters, in px rather
   than Material's growing rem. Material's typeset rules
   reach the hero's heading, paragraph and links there, so these rules carry
   a doubled class; the explorer's own rules stay in its script. The narrow
   hero keeps two plain figures, the share fully proved and what is ready
   to work on, each with its one-line note; module inventories become one
   muted line under them. */
.bp-landing-intro.bp-landing-intro { margin: 0 6px 18px; font-size: 13px; }
.bp-landing-intro.bp-landing-intro .bp-hero { margin: 0; }
.bp-landing-intro.bp-landing-intro .bp-next-kicker {
  font-size: 12px;
  font-weight: 500;
  letter-spacing: normal;
  text-transform: none;
}
.bp-landing-intro.bp-landing-intro .bp-hero-title {
  margin: 12px 0 0;
  color: var(--bp-fg);
  font-size: 22px;
  font-weight: 700;
  letter-spacing: -0.02em;
  line-height: 1.2;
}
.bp-landing-intro.bp-landing-intro .bp-hero-lead {
  max-width: none;
  margin: 10px 0 0;
  color: var(--bp-fg);
  font-size: 16px;
  line-height: 1.5;
}
.bp-landing-intro.bp-landing-intro .bp-hero-status {
  margin: 14px 0 0;
  color: var(--bp-fg);
  font-size: 16px;
  font-weight: 600;
}
.bp-landing-intro.bp-landing-intro .bp-hero-figures {
  grid-template-columns: repeat(2, minmax(0, 1fr));
  margin-top: 14px;
}
.bp-landing-intro.bp-landing-intro .bp-figure { padding: 9px 10px; }
.bp-landing-intro.bp-landing-intro .bp-figure-value {
  font-size: 17px;
  font-weight: 700;
}
.bp-landing-intro.bp-landing-intro .bp-figure-label { margin-top: 5px; font-size: 12px; font-weight: 600; }
.bp-landing-intro.bp-landing-intro .bp-figure-note { margin-top: 2px; font-size: 12px; }
.bp-landing-intro.bp-landing-intro .bp-hero-counts {
  margin: 8px 0 0;
  color: var(--bp-muted);
  font-size: 12px;
  font-variant-numeric: tabular-nums;
}
.bp-landing-intro.bp-landing-intro .bp-hero-coverage { margin-top: 6px; font-size: 12px; }
.bp-landing-intro.bp-landing-intro .bp-hero-coverage-links { margin-left: 0; }
.bp-landing-intro.bp-landing-intro .bp-intro-book {
  display: inline-block;
  margin-top: 10px;
  color: var(--bp-link);
  font-size: 15px;
  font-weight: 600;
  text-decoration: none;
}
.bp-intro-book::after { content: " →"; }
.bp-landing-intro.bp-landing-intro .bp-next-target { margin: 14px 0 0; padding: 10px 12px; }
.bp-landing-intro.bp-landing-intro .bp-next-title { font-size: 14px; font-weight: 600; }
.bp-landing-intro.bp-landing-intro .bp-next-why,
.bp-landing-intro.bp-landing-intro .bp-next-rests,
.bp-landing-intro.bp-landing-intro .bp-next-actions { font-size: 12px; }
.bp-landing-intro.bp-landing-intro .bp-live-activity { margin: 14px 0 0; padding: 10px 12px; }
.bp-landing-intro.bp-landing-intro .bp-live-row { font-size: 12px; }

/* One grid for the whole legend. The cells are emitted in reading order with
   no row wrapper, so every swatch, label and count sits on the same axis
   however long the text beside it runs. */
.bp-legend-grid {
  display: grid;
  grid-template-columns: auto auto auto minmax(0, 1fr);
  align-items: baseline;
  gap: 0.5rem 0.9rem;
  font-size: 0.72rem;
}
.bp-legend-label { font-weight: 700; white-space: nowrap; }
.bp-legend-count {
  justify-self: end;
  font-variant-numeric: tabular-nums;
  font-weight: 700;
  color: var(--bp-muted);
}
.bp-legend-meaning { color: var(--bp-muted); }
.md-typeset .bp-legend-grid .bp-swatch { align-self: center; }

/* The book opens with a compact progress summary. It reports only decomposed
   blueprint items, leaving source-wide coverage to the dedicated page. */
.bp-progress-overview {
  margin: 1.5rem 0 2rem;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  padding: 1rem 1.15rem;
  border: 1px solid var(--bp-rule);
  border-radius: 6px;
  background: var(--bp-surface);
}
.bp-progress-kicker {
  font-size: 0.72rem;
  font-weight: 600;
  color: var(--bp-muted);
}
.bp-progress-total { margin-top: 0.2rem; font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; font-size: 1.05rem; }
.bp-progress-states {
  display: flex;
  flex-wrap: wrap;
  gap: 0.35rem 1rem;
  margin-top: 0.55rem;
  font-size: 0.85rem;
}
.bp-progress-state { display: inline-flex; align-items: center; gap: 0.35rem; }

/* Theorem environments, following leanblueprint's amsthm markup. */
.bp-thmwrapper { margin: 2rem 0 2.25rem; }

.bp-thmheading {
  display: flex;
  align-items: baseline;
  flex-wrap: wrap;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-weight: 700;
  line-height: 150%;
  color: var(--bp-fg);
}
/* The heading row is an h4, so search gives each card a record of its own;
   it keeps the look of the div it was, under Material's and the site's h4 rules. */
.bp-thmwrapper > .bp-thmheading { margin: 0; font-size: inherit; letter-spacing: inherit; }
/* The kind sits on a line of its own above the name, as on the map's reader. */
.bp-thmcaption { flex-basis: 100%; font-size: 0.72rem; font-weight: 400; line-height: 1.4; color: var(--bp-muted); }

/* With sticky tabs Material renders them inside <header>, so the title, the
   repository link and the tabs are one bar. These rules only remove the seam
   between the two rows of that bar. */
.md-tabs { background-color: transparent; box-shadow: none; }
.md-tabs__list { padding-left: 0.2rem; }
.md-tabs__item { height: 1.9rem; }

/* "Next up" is the one card a visitor reads first, so it gets real hierarchy
   and a way into the mathematics rather than three stacked words. */
.bp-next-target {
  border: 1px solid var(--bp-rule);
  border-left: 3px solid var(--bp-link);
  border-radius: 6px;
  padding: 0.75rem 1rem;
  margin: 1rem 0 1.5rem;
  background: var(--bp-surface);
}
.bp-next-kicker {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.68rem;
  font-weight: 600;
  color: var(--bp-muted);
}
.bp-next-title { font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; font-size: 1.15rem; margin-top: 0.15rem; }
.bp-next-why, .bp-next-rests {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.85rem;
  color: var(--bp-muted);
  margin-top: 0.2rem;
}
.bp-next-actions { font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; font-size: 0.85rem; margin-top: 0.5rem; }

.bp-live-claimed { outline: 2px solid #2D88FF; outline-offset: 2px; }
.bp-live-badge {
  margin-left: 0.55rem;
  padding: 0.15rem 0.45rem;
  border: 1px solid #2D88FF;
  border-radius: 999px;
  color: #2D88FF;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.68rem;
  font-weight: 700;
}
.bp-live-activity {
  margin: 1rem 0 1.5rem;
  padding: 0.9rem 1rem;
  border: 1px solid var(--bp-rule);
  border-radius: 0.6rem;
  background: var(--bp-surface);
}
.bp-live-activity-title { font-weight: 700; margin-bottom: 0.35rem; }
.bp-live-row, .bp-live-empty, .bp-live-error { font-size: 0.85rem; color: var(--bp-muted); }
.bp-live-error { color: #D93025; }

/* On a graph page the legend hangs off an icon at the end of the lead. It
   opens on hover and on focus, so the button is reachable by keyboard; there
   is no script behind it. */
.bp-legend-tip { position: relative; display: inline-block; }
.bp-legend-icon {
  display: inline-flex;
  padding: 0;
  border: 0;
  background: none;
  color: var(--bp-muted);
  cursor: help;
  vertical-align: -0.14em;
}
.bp-legend-icon svg {
  width: 1em;
  height: 1em;
  fill: none;
  stroke: currentColor;
  stroke-width: 1.4;
  stroke-linecap: round;
}
.bp-legend-icon .bp-legend-dot { fill: currentColor; stroke: none; }
.bp-legend-icon:hover, .bp-legend-icon:focus-visible { color: var(--bp-link); }
.bp-legend-note {
  position: absolute;
  z-index: 5;
  left: 0;
  top: calc(100% + 0.5rem);
  width: max-content;
  max-width: min(30rem, 78vw);
  padding: 0.85rem 1rem;
  border: 1px solid var(--bp-rule);
  border-radius: var(--bp-radius);
  background: var(--bp-surface);
  box-shadow: 0 8px 28px rgb(0 0 0 / 22%);
  /* Hidden without display:none, so the description stays announceable. */
  opacity: 0;
  visibility: hidden;
  transition: opacity 90ms ease;
}
.bp-legend-tip:hover .bp-legend-note,
.bp-legend-tip:focus-within .bp-legend-note { opacity: 1; visibility: visible; }

.bp-visually-hidden {
  position: absolute;
  width: 1px;
  height: 1px;
  margin: -1px;
  padding: 0;
  overflow: hidden;
  clip-path: inset(50%);
  white-space: nowrap;
}

.bp-source-link { color: var(--bp-muted); margin-left: 0.3rem; }
.bp-source-link:hover { color: var(--bp-link-hover); text-decoration: none; }
.bp-source-icon { width: 0.95em; height: 0.95em; fill: none; stroke: currentColor;
  stroke-width: 1.8; stroke-linecap: round; stroke-linejoin: round; vertical-align: -0.12em; }
.bp-code-links { display: inline-flex; flex-wrap: wrap; align-items: center; gap: 0.2rem; margin-left: 0.45rem; }
.bp-code-link {
  display: inline-flex;
  align-items: center;
  color: var(--bp-muted);
  text-decoration: none;
}
.bp-code-link:visited { color: var(--bp-muted); }
.bp-code-link:hover, .bp-code-link:visited:hover { color: var(--bp-link-hover); text-decoration: none; }
.bp-code-icon {
  width: 1rem;
  height: 1rem;
  fill: none;
  stroke: currentColor;
  stroke-width: 1.8;
  stroke-linecap: round;
  stroke-linejoin: round;
}
.bp-permalink {
  margin-left: 0.5rem;
  font-family: "JetBrains Mono", ui-monospace, SFMono-Regular, Menlo, monospace;
  font-weight: 400;
  text-decoration: none;
  color: var(--bp-muted);
  opacity: 0;
  transition: opacity 0.1s ease;
}
/* A keyboard reaches the permalink too, so focus shows it as hover does. */
.bp-thmwrapper:hover .bp-permalink, .bp-permalink:focus-visible { opacity: 1; }

/* The status is a pill on its own line under the title, a dot and a word
   tinted with the status colour, as in the explorer's drawer. An empty item
   the full width of the heading breaks the line before it, so the pill sits
   at the left however long the title runs. */
.bp-thmheading::after { content: ""; order: 1; flex-basis: 100%; }
.bp-mark {
  order: 2;
  display: inline-flex;
  align-items: center;
  gap: 0.35em;
  margin-top: 0.3rem;
  padding: 0.1em 0.6em;
  border-radius: 999px;
  background: color-mix(in srgb, currentColor 12%, transparent);
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.72rem;
  font-weight: 600;
  line-height: 1.5;
}
.bp-mark-label { color: var(--bp-fg); }

.bp-thmcontent {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-weight: 400;
  line-height: 1.75;
  margin-left: 0.5rem;
  padding: 0.15rem 0 0.15rem 1rem;
  border-left: 3px solid var(--bp-rule);
}
.theorem-style-plain > .bp-thmcontent { font-style: italic; }
.theorem-style-definition > .bp-thmcontent { font-style: normal; }
.bp-thmcontent > p:first-child { margin-top: 0; }
.bp-thmcontent > p:last-child { margin-bottom: 0; }

.bp-thmnotes {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.85rem;
  line-height: 1.7;
  margin: 0.6rem 0 0 2rem;
  color: var(--bp-muted);
}
.bp-thmnotes h6 {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.72rem;
  font-weight: 600;
  letter-spacing: normal;
  color: var(--bp-muted);
  margin: 0.5rem 0 0.15rem;
}
.bp-thmnotes ul { margin: 0; padding-left: 1.1rem; }

.bp-meta {
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.85rem;
  line-height: 1.8;
  margin: 0.6rem 0 0 2rem;
}
/* Material styles every details element as a collapsible admonition: a
   bordered box, a tinted summary and a pencil icon. These are quiet lines
   under each statement, so the selectors outrank Material's and take that
   chrome off, keeping only its chevron, which turns when the line opens. */
.md-typeset :is(details.bp-dependencies, details.bp-lean-fold) {
  margin: 0.65rem 0 0 2rem;
  padding: 0;
  border: 0;
  border-radius: 0;
  box-shadow: none;
  background: none;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.72rem;
  color: var(--bp-muted);
}
.md-typeset :is(details.bp-dependencies, details.bp-lean-fold) > summary {
  display: flex;
  align-items: center;
  width: fit-content;
  margin: 0;
  padding: 0.2rem 0;
  border: 0;
  background: none;
  font-weight: 600;
  cursor: pointer;
  user-select: none;
}
.md-typeset :is(details.bp-dependencies, details.bp-lean-fold) > summary::before { display: none; }
.md-typeset :is(details.bp-dependencies, details.bp-lean-fold) > summary::after {
  position: static;
  flex: none;
  width: 1em;
  height: 1em;
  margin-left: 0.25em;
}
.md-typeset :is(details.bp-dependencies, details.bp-lean-fold) > summary:hover { color: var(--bp-link-hover); text-decoration: underline; }
@media (pointer: coarse) {
  .md-typeset :is(details.bp-dependencies, details.bp-lean-fold) > summary { min-height: 44px; }
}
.bp-dependency-body { margin-top: 0.35rem; color: var(--bp-fg); }
.bp-review {
  margin: 0.65rem 0 0 2rem;
  font-family: "Plus Jakarta Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.82rem;
  color: var(--bp-muted);
}
.bp-review summary {
  width: fit-content;
  overflow-wrap: anywhere;
  cursor: pointer;
  color: var(--bp-link);
  user-select: none;
}
.bp-review summary:hover { color: var(--bp-link-hover); text-decoration: underline; }
.bp-review-self-approved { color: var(--bp-muted); font-style: italic; }
.bp-review-open { color: var(--bp-muted); }
/* Each text color reads at 4.5:1 or more on its scheme's background. */
.bp-review-drift { color: #946200; font-weight: 600; }
[data-md-color-scheme=slate] .bp-review-drift { color: #F0B429; }
.bp-skeleton { margin-top: 0.6rem; color: var(--bp-fg); }
.bp-skeleton-title { font-weight: 600; margin-bottom: 0.3rem; }
.bp-lean {
  margin: 0 0 0.4rem;
  padding: 0.6rem 0.8rem;
  font-family: "JetBrains Mono", ui-monospace, SFMono-Regular, Menlo, monospace;
  font-size: 0.78rem;
  line-height: 1.45;
  white-space: pre-wrap;
  overflow-x: auto;
  border-left: 3px solid var(--bp-rule);
}
.bp-skeleton-meta { margin-bottom: 0.5rem; }
/* A statement's Lean declarations, under it, in the page's code colors. */
.bp-lean-source { margin: 0.6rem 0 0 2rem; }
/* Material's code box is the block's only frame. */
.bp-lean-source .bp-lean { padding: 0; border: 0; }
.md-typeset details.bp-lean-fold { margin: 0 0 0.4rem; }
/* A flex summary drops the space between the name and its line count. */
.md-typeset details.bp-lean-fold > summary { gap: 0.3em; }
.bp-lean-keyword { color: var(--md-code-hl-keyword-color); }
.bp-lean-comment { color: var(--md-code-hl-comment-color); }
.bp-lean-string { color: var(--md-code-hl-string-color); }
/* A linked name in Lean: dotted until hovered, so the code still reads as code. */
.md-typeset :is(.bp-lean-ref, .bp-lean-doc) { color: inherit; text-decoration: underline dotted; text-underline-offset: 0.2em; }
.md-typeset :is(.bp-lean-ref, .bp-lean-doc):is(:hover, :focus-visible) { color: var(--bp-link-hover); text-decoration-style: solid; }
/* A card too wide for the page scrolls, with a shade at each edge it can
   scroll toward: covers in the review panel's color scroll with the content
   and hide the shade at the end it has reached. */
.bp-readback {
  margin: 0.4rem 0 1rem;
  padding: 0.6rem 0.8rem;
  color: var(--bp-fg);
  border-left: 3px solid var(--bp-blue);
  overflow-x: auto;
  background:
    linear-gradient(to right, var(--md-admonition-bg-color, var(--bp-page)) 40%, transparent) left / 1.5rem 100% no-repeat local,
    linear-gradient(to left, var(--md-admonition-bg-color, var(--bp-page)) 40%, transparent) right / 1.5rem 100% no-repeat local,
    radial-gradient(farthest-side at 0 50%, var(--bp-scroll-shade), transparent) left / 0.6rem 100% no-repeat scroll,
    radial-gradient(farthest-side at 100% 50%, var(--bp-scroll-shade), transparent) right / 0.6rem 100% no-repeat scroll;
  background-color: var(--md-admonition-bg-color, var(--bp-page));
}
.bp-readback-title { font-weight: 600; margin-bottom: 0.3rem; }
.bp-readback-body { white-space: pre-wrap; }
.bp-readback-status { font-weight: 400; color: var(--bp-muted); }
.bp-readback-invalid { border-left-color: #B42318; }
[data-md-color-scheme=slate] .bp-readback-invalid { border-left-color: #F97066; }
.bp-readback-missing { border-left-color: var(--bp-rule); font-style: italic; }
/* A formula paints only within its own band, its box plus the slack its
   glyphs need, which a negative margin gives back. Across, it paints as TeX
   sets it, laps included, but only inside the block that holds it, and a
   display scrolls in its own; so no article formula can cover a card, a mark,
   a label, another line, or the side columns, whatever the renderer or theme.
   A card scrolls instead, so nothing in it is cut. Inline formulas become
   inline blocks to have a box to clip, and the display selector outranks
   MathJax's own sheets, which are added after this one. */
mjx-container {
  overflow-x: visible !important;
  overflow-y: clip !important;
  position: relative !important;
}
mjx-container:not([display="true"]) {
  display: inline-block;
  padding-block: 0.3em;
  margin-block: -0.3em;
}
:root mjx-container[jax][display="true"] {
  padding-block: 0.5em;
  margin-block: 0.5em;
}
div.arithmatex { overflow-x: auto; }
/* Material caps every svg at its container's width, which would shrink a wide
   SVG formula until it cannot be read; it keeps the size TeX set instead. */
mjx-container > svg { max-width: none !important; }
:is(p, h1, h2, h3, h4, h5, h6, ul, ol, td, th):has(mjx-container):not(.bp-readback *) {
  overflow-x: clip;
}
/* A page or statement published as typed: its text wraps, and nothing in it
   is markup. */
.bp-as-typed-note { color: var(--bp-muted); font-size: 0.85em; }
.bp-as-typed { white-space: pre-wrap; overflow-wrap: anywhere; }
.bp-row { display: flex; gap: 0.75rem; }
.bp-key {
  flex: 0 0 7.5rem;
  font-size: 0.78rem;
  font-weight: 600;
  color: var(--bp-muted);
}
.bp-value { flex: 1; }
/* A reference breaks between entries, never inside one; a long one wraps in its own box. Each starts with its status dot, so
   the list drops the separators, which ended every wrapped line and could take a line of their own. A project that tracks
   no Lean has no dots, so its references keep the separators. */
.bp-dependency-body .bp-ref { display: inline-block; max-width: 100%; margin-right: 0.5rem; }
.bp-dependency-body .bp-ref[class*=" bp-ref-"] + .bp-ref-sep { display: none; }
.bp-lean { font-family: "JetBrains Mono", ui-monospace, SFMono-Regular, Menlo, monospace; }
.bp-where { color: var(--bp-muted); }
.bp-missing { color: #b91c1c; }
[data-md-color-scheme=slate] .bp-missing { color: #ff7b72; }
.bp-ref[class*=" bp-ref-"]::before {
  content: "";
  display: inline-block;
  width: 0.6rem;
  height: 0.6rem;
  margin-right: 0.35rem;
  border: 1px solid var(--bp-rule);
  border-radius: 50%;
}
.bp-swatch {
  display: inline-block;
  width: 0.6rem;
  height: 0.6rem;
  border: 2px solid var(--bp-rule);
  border-radius: 50%;
  vertical-align: middle;
}

.bp-mathlib .bp-mark { color: #123C20; }
.bp-mathlib > .bp-thmcontent { border-left-color: #123C20; }
.bp-ref-mathlib::before, .bp-swatch-mathlib { background: #123C20; border-color: #123C20; }
.bp-fully_proved .bp-mark { color: #1B5B2E; }
.bp-fully_proved > .bp-thmcontent { border-left-color: #1B5B2E; }
.bp-ref-fully_proved::before, .bp-swatch-fully_proved { background: #1B5B2E; border-color: #1B5B2E; }
.bp-proved .bp-mark { color: #277B3E; }
.bp-proved > .bp-thmcontent { border-left-color: #277B3E; }
.bp-ref-proved::before, .bp-swatch-proved { background: #277B3E; border-color: #277B3E; }
.bp-defined .bp-mark { color: #349D4D; }
.bp-defined > .bp-thmcontent { border-left-color: #349D4D; }
.bp-ref-defined::before, .bp-swatch-defined { background: #349D4D; border-color: #349D4D; }
.bp-conditional .bp-mark { color: #6B3FCF; }
.bp-conditional > .bp-thmcontent { border-left-color: #6B3FCF; }
.bp-ref-conditional::before, .bp-swatch-conditional { background: #6B3FCF; border-color: #6B3FCF; }
.bp-can_prove .bp-mark { color: #0064E0; }
.bp-can_prove > .bp-thmcontent { border-left-color: #0064E0; }
.bp-ref-can_prove::before, .bp-swatch-can_prove { background: #FFFFFF; border-color: #0064E0; }
.bp-stated .bp-mark { color: #2B8F44; }
.bp-stated > .bp-thmcontent { border-left-color: #2B8F44; }
.bp-ref-stated::before, .bp-swatch-stated { background: #FFFFFF; border-color: #2B8F44; }
.bp-can_state .bp-mark { color: #0082FB; }
.bp-can_state > .bp-thmcontent { border-left-color: #0082FB; }
.bp-ref-can_state::before, .bp-swatch-can_state { background: #FFFFFF; border-color: #0082FB; }
.bp-not_ready .bp-mark { color: #B77900; }
.bp-not_ready > .bp-thmcontent { border-left-color: #B77900; }
.bp-ref-not_ready::before, .bp-swatch-not_ready { background: #B77900; border-color: #B77900; }
.bp-planned .bp-mark { color: #CED0D4; }
.bp-planned > .bp-thmcontent { border-left-color: #CED0D4; }
.bp-ref-planned::before, .bp-swatch-planned { background: #FFFFFF; border-color: #CED0D4; }

[data-md-color-scheme=slate] .bp-mathlib .bp-mark { color: #B2F3BA; }
[data-md-color-scheme=slate] .bp-mathlib > .bp-thmcontent { border-left-color: #B2F3BA; }
[data-md-color-scheme=slate] .bp-ref-mathlib::before, [data-md-color-scheme=slate] .bp-swatch-mathlib { background: #B2F3BA; border-color: #B2F3BA; }
[data-md-color-scheme=slate] .bp-fully_proved .bp-mark { color: #4DD35F; }
[data-md-color-scheme=slate] .bp-fully_proved > .bp-thmcontent { border-left-color: #4DD35F; }
[data-md-color-scheme=slate] .bp-ref-fully_proved::before, [data-md-color-scheme=slate] .bp-swatch-fully_proved { background: #4DD35F; border-color: #4DD35F; }
[data-md-color-scheme=slate] .bp-proved .bp-mark { color: #32AC4E; }
[data-md-color-scheme=slate] .bp-proved > .bp-thmcontent { border-left-color: #32AC4E; }
[data-md-color-scheme=slate] .bp-ref-proved::before, [data-md-color-scheme=slate] .bp-swatch-proved { background: #32AC4E; border-color: #32AC4E; }
[data-md-color-scheme=slate] .bp-defined .bp-mark { color: #288841; }
[data-md-color-scheme=slate] .bp-defined > .bp-thmcontent { border-left-color: #288841; }
[data-md-color-scheme=slate] .bp-ref-defined::before, [data-md-color-scheme=slate] .bp-swatch-defined { background: #288841; border-color: #288841; }
[data-md-color-scheme=slate] .bp-conditional .bp-mark { color: #9F7AEA; }
[data-md-color-scheme=slate] .bp-conditional > .bp-thmcontent { border-left-color: #9F7AEA; }
[data-md-color-scheme=slate] .bp-ref-conditional::before, [data-md-color-scheme=slate] .bp-swatch-conditional { background: #9F7AEA; border-color: #9F7AEA; }
[data-md-color-scheme=slate] .bp-can_prove .bp-mark { color: #2D88FF; }
[data-md-color-scheme=slate] .bp-can_prove > .bp-thmcontent { border-left-color: #2D88FF; }
[data-md-color-scheme=slate] .bp-ref-can_prove::before, [data-md-color-scheme=slate] .bp-swatch-can_prove { background: #101F33; border-color: #2D88FF; }
[data-md-color-scheme=slate] .bp-stated .bp-mark { color: #31A24C; }
[data-md-color-scheme=slate] .bp-stated > .bp-thmcontent { border-left-color: #31A24C; }
[data-md-color-scheme=slate] .bp-ref-stated::before, [data-md-color-scheme=slate] .bp-swatch-stated { background: #242526; border-color: #31A24C; }
[data-md-color-scheme=slate] .bp-can_state .bp-mark { color: #2D88FF; }
[data-md-color-scheme=slate] .bp-can_state > .bp-thmcontent { border-left-color: #2D88FF; }
[data-md-color-scheme=slate] .bp-ref-can_state::before, [data-md-color-scheme=slate] .bp-swatch-can_state { background: #242526; border-color: #2D88FF; }
[data-md-color-scheme=slate] .bp-not_ready .bp-mark { color: #F7B928; }
[data-md-color-scheme=slate] .bp-not_ready > .bp-thmcontent { border-left-color: #F7B928; }
[data-md-color-scheme=slate] .bp-ref-not_ready::before, [data-md-color-scheme=slate] .bp-swatch-not_ready { background: #F7B928; border-color: #F7B928; }
[data-md-color-scheme=slate] .bp-planned .bp-mark { color: #737578; }
[data-md-color-scheme=slate] .bp-planned > .bp-thmcontent { border-left-color: #737578; }
[data-md-color-scheme=slate] .bp-ref-planned::before, [data-md-color-scheme=slate] .bp-swatch-planned { background: #242526; border-color: #737578; }
.bp-swatch-inventory_checked { background: #FFFFFF; border-color: #65676B; }
[data-md-color-scheme=slate] .bp-swatch-inventory_checked { background: #242526; border-color: #C8CACE; }
.bp-swatch-inventory_pending { background: #85898E; border-color: #85898E; }
[data-md-color-scheme=slate] .bp-swatch-inventory_pending { background: #9EA1A6; border-color: #9EA1A6; }