/* ============ Header controls (mount in the sticky navbar) ============ */
/* Detail [range] n/max [manual]  [?] — always at hand while reading. */
.detail-ctl {
  display: inline-flex; align-items: center; gap: .45rem;
  margin-left: auto; padding: 0 .6rem;
  font-size: .8rem; white-space: nowrap; color: inherit;
}
.detail-ctl input[type="range"] { width: 6.5rem; vertical-align: middle; }
.detail-ctl .detail-val { font-variant-numeric: tabular-nums; opacity: .7; }
.detail-ctl button {
  border: 1px solid rgba(0,0,0,.25); border-radius: 5px;
  background: transparent; color: inherit; cursor: pointer;
  font-size: .75rem; padding: .1rem .45rem; line-height: 1.3;
}
.detail-ctl button.active { background: #111; color: #fff; }
.detail-ctl .notn-toggle { font-weight: 700; }
.detail-ctl .notn-toggle.off { opacity: .45; text-decoration: line-through; }
@media (max-width: 700px) { .detail-ctl input[type="range"] { width: 4rem; }
  .detail-ctl label { display: none; } }
/* dark mode keys on the theme's .dark-mode class (readability-options.js
   sets it from the system preference and the user toggle) — a bare media
   query would disagree with the manual toggle */
:root.dark-mode .detail-ctl button { border-color: rgba(255,255,255,.3); }
:root.dark-mode .detail-ctl button.active { background: #e8e8e8; color: #111; }

/* reader turned notation links off: no affordance either */
body.notation-links-off .ptxfar, body.notation-links-off .ptxfar *,
body.notation-links-off [class*="ptxnotn-"] {
  cursor: inherit;
}
body.notation-links-off [class*="ptxnotn-"]:hover {
  text-decoration: none;
}

/* ============ Notation hovers (no knowl underline) ============ */
/* The tagged symbol gets only a help cursor by default; a faint dotted
   underline appears on hover so nothing distracts inside equations. */
[class*="ptxnotn-"] { cursor: help; }
[class*="ptxnotn-"]:hover,
[class*="ptxnotn-"]:focus {
  text-decoration: underline dotted 1px;
  text-underline-offset: 3px;
  outline: none;
}

.notation-popup {
  position: absolute; z-index: 1200; max-width: 24rem;
  background: #fff; color: #111;
  border: 1px solid rgba(0,0,0,.2); border-radius: 6px;
  box-shadow: 0 6px 18px rgba(0,0,0,.18);
  padding: .5rem .7rem; font-size: .9rem; line-height: 1.35;
  pointer-events: none; opacity: 0; transform: translateY(-2px);
  transition: opacity .1s ease, transform .1s ease;
}
.notation-popup.show { opacity: 1; transform: translateY(0); pointer-events: auto; }
.notation-popup .notation-popup-key {
  display: block; font-weight: 600; opacity: .55;
  font-size: .72rem; letter-spacing: .02em; margin-bottom: .2rem;
}
:root.dark-mode .notation-popup {
  background: #22262b; color: #e8e8e8; border-color: rgba(255,255,255,.18);
}

/* ============ Formalization badges (<lean> as child of a theorem block,
   and inline in the intro trust-base table's dl) ============ */
article.theorem-like > .lean-link, section > .lean-link,
.ptx-content dl .lean-link {
  display: inline-block; font-size: .78rem; font-family: ui-monospace, monospace;
  padding: .1rem .5rem; margin: .2rem .3rem .2rem 0;
  border: 1px solid rgba(25,100,60,.4); border-radius: 999px;
  background: rgba(40,160,90,.08); text-decoration: none;
}
article.theorem-like > .lean-link::before,
.ptx-content dl .lean-link::before { content: "⚙ "; }
/* Two independent formalizations, distinguished by color:
   gq2-claude (the GQ2 library) keeps the green above;
   gq2-gpt (Q2Presentation) gets indigo. Tooltips name the project. */
.ptx-content .lean-link.lean-proj-gq2-gpt {
  border-color: rgba(55, 80, 180, 0.45);
  background: rgba(70, 100, 220, 0.08);
}
/* declarations without a docs page (private): same pill, visibly inert —
   dashed outline, help cursor, tooltip carries the explanation */
.ptx-content .lean-link.lean-nolink {
  border-style: dashed; opacity: .8; cursor: help;
}

/* Far notation (notation_far.py): NO rest-state affordance. On hover the
   cursor is the help question-mark; the definition popup appears after a
   delay (FAR_DELAY_MS in detail-ui.js) with a see-in-context link. */
.ptxfar, .ptxfar * { cursor: help; }

/* hovering a notation link also lights up the DEFINING OCCURRENCE of that
   symbol, a beat before the popup. Highlighter amber, with a box-shadow
   halo for "padding" that cannot disturb the layout. */
.notation-defsite-hl {
  background: rgba(255, 196, 0, 0.4);
  box-shadow: 0 0 0 5px rgba(255, 196, 0, 0.4);
  border-radius: 4px;
  transition: background 0.2s ease-in, box-shadow 0.2s ease-in;
}

/* at the defining occurrence itself there is no popup: the mouse cursor
   becomes an =-in-a-circle (parallel to the help cursor's ?-in-a-circle)
   — "this is the source of the notation" */
.notation-defcursor, .notation-defcursor * {
  cursor: url('data:image/svg+xml;utf8,<svg xmlns="http://www.w3.org/2000/svg" width="20" height="20"><circle cx="10" cy="10" r="8.5" fill="black" stroke="white" stroke-width="1.5"/><text x="10" y="14" font-size="12" font-weight="bold" text-anchor="middle" fill="white">=</text></svg>') 10 10, default;
}

/* landing highlight: following a popup context link paints the specific
   referenced text (the defining occurrence, or the target's heading) and
   fades it out over five seconds — replacing the theme's whole-block
   :target flash, which the pushState navigation deliberately bypasses */
.pf-landing-hl {
  background: rgba(255, 196, 0, 0.45);
  box-shadow: 0 0 0 5px rgba(255, 196, 0, 0.45);
  border-radius: 4px;
}
.pf-landing-hl.pf-landing-fade {
  background: rgba(255, 196, 0, 0);
  box-shadow: 0 0 0 5px rgba(255, 196, 0, 0);
  transition: background 5s ease-out, box-shadow 5s ease-out;
}

.notation-popup .notation-ctx-link {
  display: block; margin-top: .4rem; font-size: .78rem;
  opacity: .85; text-decoration: none; border-top: 1px solid rgba(128,128,128,.25);
  padding-top: .3rem;
}
.notation-popup .notation-ctx-link:hover { text-decoration: underline; }

/* proof-local details tier button (quiet, matching the proof knowl look) */
.detail-next-btn {
  display: block; margin: .4em 0 .2em; padding: .15em .7em;
  background: #f5f5f5; border: none; border-radius: 3px;
  font-family: inherit; font-style: italic; font-size: .95em;
  color: #333; cursor: pointer;
}
.detail-next-btn:hover { background: #ececec; }

/* inline detail tiers: hidden until a container (body via the slider, a
   proof via its details button, or a statement via its own button) enables
   them. Level 1 = statement detail; levels 2+ = proof detail. */
.para.detail-level-1, .para.detail-level-2,
.para.detail-level-3, .para.detail-level-4 { display: none; }
.show-dl-1 .para.detail-level-1, .show-dl-2 .para.detail-level-2,
.show-dl-3 .para.detail-level-3, .show-dl-4 .para.detail-level-4 {
  display: block; }

/* the statement stepper sits on its own line at the end of the statement */
.detail-next-btn.detail-stmt-btn { display: block; margin: .3em 0 .1em; }

/* the details button sits on the Proof line, only while the proof is open */
.detail-next-btn { display: inline-block; margin: 0 0 0 .9em;
  padding: .05em .55em; vertical-align: baseline; }
details.hiddenproof:not([open]) .detail-next-btn { display: none; }

/* equation-range knowls: "(1.1)–(1.3)" opens all equations in the range */
.eqrange { cursor: pointer; white-space: nowrap; }
.eqrange-knowl { background: #f5f5f5; border-radius: 4px;
  padding: .4em .9em; margin: .45em 0; overflow-x: auto; }
.eqrange-knowl-foot { margin-top: .2em; text-align: right; font-size: .92em; }
.eqrange-knowl a { color: #111; }
:root.dark-mode .eqrange-knowl { background: #2c2d27; }
:root.dark-mode .eqrange-knowl a { color: #f2f2f2; }

/* inline section knowls: a division xref click opens its summary */
.section-knowl { background: #f5f5f5; border-radius: 4px; padding: .6em .9em;
  margin: .45em 0; font-size: .95em; }
.section-knowl .section-knowl-title { font-weight: 700; margin-bottom: .35em; }
.section-knowl .para { margin: .35em 0; }
.section-knowl .section-knowl-foot { margin-top: .45em; text-align: right;
  font-size: .92em; }
.section-knowl a { color: #111; }

/* inline Lean knowls: a badge click opens the declaration's doc entry */
.lean-knowl { background: #f5f5f5; border-radius: 4px; padding: .6em .9em;
  margin: .45em 0; font-size: .9em; overflow-x: auto; }
.lean-knowl .decl_header, .lean-knowl code, .lean-knowl pre {
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
  font-size: .95em; }
.lean-knowl-foot { margin-top: .45em; text-align: right; font-size: .92em; }
.lean-knowl a { color: #111; }

/* homepage links injected by addHomeLinks(): quiet, matching the site's
   back-link voice; colors inherit so both schemes work */
.site-home-link {
  padding: .45rem 1rem .1rem;
  font: 650 0.85rem/1.2 system-ui, sans-serif;
}
.site-home-link a, .site-home-return a {
  color: inherit;
  text-decoration: underline;
  text-decoration-color: rgba(40, 160, 90, 0.55);
  text-decoration-thickness: 2px;
  text-underline-offset: 0.2em;
}
.site-home-link a:hover, .site-home-return a:hover {
  text-decoration-color: currentColor;
}
.site-home-return {
  max-width: 58rem;
  margin: 1.4rem auto 0;
  padding: 0.9rem 0 0.4rem;
  border-top: 1px solid rgba(128, 128, 128, 0.3);
  font-size: 0.95rem;
}

/* dark counterparts for every literal light value above (same .dark-mode
   signal as the theme; panels sit a step off the dark body #23241f) */
:root.dark-mode .detail-next-btn { background: #33342c; color: #d5d6d0; }
:root.dark-mode .detail-next-btn:hover { background: #3c3d34; }
:root.dark-mode .section-knowl, :root.dark-mode .lean-knowl {
  background: #2c2d27;
}
:root.dark-mode .section-knowl a, :root.dark-mode .lean-knowl a {
  color: #f2f2f2;
}
:root.dark-mode article.theorem-like > .lean-link,
:root.dark-mode section > .lean-link,
:root.dark-mode .ptx-content dl .lean-link {
  border-color: rgba(120, 200, 150, 0.45);
}
:root.dark-mode .ptx-content .lean-link.lean-proj-gq2-gpt {
  border-color: rgba(130, 150, 240, 0.55);
}