/* Real-rooted atlas.  One type scale (1rem body, .875rem small, 1.25/1.6rem
   headings), one spacing unit (.25rem steps), tokens for light and dark. */
:root {
  --bg: #fbfbf8; --fg: #1d2329; --muted: #5b6570; --line: #d9dcd6; --accent: #1f5fa8;
  --card: #ffffff; --badge: #eef1ec; --root: #dcefdc; --code: #f1f2ee; --focus: #1f5fa8;
  --shadow: rgba(20, 30, 40, .16); --chip-flag: #f3efe4; --chip-flag-line: #ddd3bb;
  color-scheme: light;
}
@media (prefers-color-scheme: dark) {
  :root { --bg: #15191d; --fg: #dde2e6; --muted: #9ea9b3; --line: #2f383f; --accent: #82b6f0;
          --card: #1b2127; --badge: #252d34; --root: #223a26; --code: #20272d; --focus: #82b6f0;
          --shadow: rgba(0, 0, 0, .5); --chip-flag: #2b2820; --chip-flag-line: #4a4334;
          color-scheme: dark; }
}
* { box-sizing: border-box; }
html { -webkit-text-size-adjust: 100%; text-size-adjust: 100%; }
body { margin: 0; background: var(--bg); color: var(--fg);
  font: 16px/1.5 system-ui, -apple-system, "Segoe UI", Roboto, sans-serif; }
a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; }
:focus-visible { outline: 2px solid var(--focus); outline-offset: 2px; border-radius: 2px; }
.skip-link { position: absolute; left: -999px; top: .5rem; padding: .4rem .8rem; background: var(--card);
  border: 1px solid var(--line); border-radius: 4px; z-index: 10; }
.skip-link:focus { left: .5rem; }
code, pre { font-family: ui-monospace, "SFMono-Regular", Menlo, Consolas, monospace; font-size: .875em;
  background: var(--code); border-radius: 3px; }
code { padding: 0 .25em; display: inline-block; max-width: 100%; overflow-wrap: break-word; vertical-align: bottom; line-height: 1.4; }
pre code { display: inline; }
pre { padding: .6em .8em; overflow-x: auto; }
main { max-width: 62rem; margin: 0 auto; padding: .5rem 1rem 3rem; }
h1 { font-size: 1.6rem; margin: .8em 0 .3em; line-height: 1.25; overflow-wrap: break-word; }
h2 { font-size: 1.25rem; margin: 1.6em 0 .5em; border-bottom: 1px solid var(--line); padding-bottom: .2em;
  line-height: 1.3; }
h3 { font-size: 1.05rem; margin: 1.1em 0 .3em; }
p, li, dd { overflow-wrap: break-word; }
.muted { color: var(--muted); }
.small { font-size: .875rem; }
.error { color: #b3261e; }

/* Header: brand and nav on one row; the search fills the rest of the row on wide
   screens and takes its own full-width row on phones. */
.site-header { display: flex; flex-wrap: wrap; gap: .5rem 1.5rem; align-items: center;
  padding: .55rem 1rem; border-bottom: 1px solid var(--line); background: var(--card); }
.header-row { display: flex; align-items: center; gap: .3rem 1rem; flex-wrap: wrap; min-width: 0; }
.brand { display: inline-flex; align-items: center; gap: .45rem; font-weight: 700; font-size: 1.1rem;
  color: var(--fg); white-space: nowrap; }
.brand:hover { text-decoration: none; }
.brand-mark { color: var(--accent); flex: none; }
.site-nav { display: flex; gap: .9rem; }
.search-form { display: flex; gap: .4rem; min-width: 0; }
.search-form input[type=search] { flex: 1 1 auto; min-width: 0; width: 100%; }
.header-search { margin-left: auto; flex: 0 1 22rem; }
.header-search button { padding: .35em .55em; line-height: 0; }
.search-form.big { margin: .6rem 0; flex-wrap: wrap; }
.search-form.big input[type=search] { flex: 1 1 14rem; }
input, select, button { font: inherit; padding: .4em .6em; border: 1px solid var(--line);
  border-radius: 5px; background: var(--card); color: var(--fg); max-width: 100%; }
input:focus-visible, select:focus-visible, button:focus-visible { outline-offset: 1px; }
button { background: var(--accent); color: #fff; border-color: var(--accent); cursor: pointer; }
@media (prefers-color-scheme: dark) { button { color: #0d1620; } }
@media (max-width: 40rem) {
  .site-header { padding: .5rem 1rem .6rem; }
  .header-row { flex: 1 1 100%; justify-content: space-between; flex-wrap: nowrap; }
  .brand { font-size: 1rem; gap: .35rem; }
  .site-nav { gap: .8rem; font-size: .95rem; }
  .header-search { flex: 1 1 100%; margin-left: 0; }
  h1 { font-size: 1.35rem; }
  h2 { font-size: 1.15rem; }
}

/* Start page. */
.hero h1 { margin-top: .9em; }
.lead { max-width: 46rem; font-size: 1.05rem; }
.home-search { max-width: 46rem; }
.example-grid { list-style: none; padding: 0; margin: .5rem 0 1rem; display: grid; gap: .6rem;
  grid-template-columns: repeat(auto-fill, minmax(min(100%, 17rem), 1fr)); }
.example-card { padding: .6rem .8rem; border: 1px solid var(--line); border-radius: 8px;
  background: var(--card); min-width: 0; }
.example-link { display: flex; justify-content: space-between; align-items: baseline; gap: .5rem;
  font-weight: 600; }
.example-link .badge { flex: none; }
.example-card .card-rows { margin-top: .25rem; }

/* Generic tables. */
table { border-collapse: collapse; width: 100%; }
th, td { text-align: left; padding: .3em .6em; border-bottom: 1px solid var(--line); vertical-align: top; }
td.num, th.num { text-align: right; font-variant-numeric: tabular-nums; }
tr.current td { background: var(--root); }
.stats { display: flex; flex-wrap: wrap; gap: .6rem 2rem; list-style: none; padding: 0; margin: .8rem 0; }
.stats strong { font-size: 1.4rem; }
.two-col { display: grid; grid-template-columns: repeat(auto-fit, minmax(min(100%, 20rem), 1fr)); gap: 0 2rem; }
main > table, .table-wrap { display: block; overflow-x: auto; }

/* Chips. */
.badge { display: inline-block; padding: 0 .5em; border-radius: 1em; background: var(--badge);
  border: 1px solid var(--line); font-size: .8rem; line-height: 1.6; margin: .1em .1em; color: var(--fg);
  white-space: nowrap; }
a.badge:hover { text-decoration: none; border-color: var(--accent); }
.badge.root { background: var(--root); }
.badge.region, .badge.oeis { color: var(--accent); }
.badge.region { white-space: normal; }
.badge.flag { background: var(--chip-flag); border-color: var(--chip-flag-line); }
.badge.jargon { color: var(--fg); border-style: dashed; }

/* Lists of sequences. */
.node-list, .compact, .properties { list-style: none; padding: 0; margin: .5rem 0; }
.compact li { padding: .15em 0; }
.node-card { padding: .55rem .8rem; margin: .45rem 0; border: 1px solid var(--line);
  border-radius: 8px; background: var(--card); min-width: 0; }
.node-name { font-weight: 600; overflow-wrap: break-word; }
.node-card .node-chain { margin: .05em 0 0; }
.card-rows { font-size: .875rem; margin-top: .2rem; overflow-wrap: anywhere;
  font-variant-numeric: tabular-nums; }
.rows-preview { display: block; }
.row-sums { display: block; font-size: .8rem; }
.row-sep { color: var(--muted); padding: 0 .1em; }
.card-meta { margin-top: .2rem; line-height: 1.9; }
.card-meta:empty { display: none; }
.filter-form { display: flex; flex-wrap: wrap; gap: .5rem .8rem; align-items: flex-end; margin: .6rem 0 .3rem; }
.filter-form input[type=search] { flex: 1 1 14rem; min-width: 0; }
.filter { display: inline-flex; flex-direction: column; font-size: .8rem; color: var(--muted); gap: .1rem; }
.filter select { font-size: 1rem; color: var(--fg); }
.filter-form { align-items: center; }
.filter-check { display: inline-flex; align-items: center; gap: .35rem; font-size: .95rem; white-space: nowrap; cursor: pointer; }
.filter-check input { width: 1.05rem; height: 1.05rem; margin: 0; }
details.help { margin: .2rem 0 .6rem; color: var(--muted); }
details.help summary { cursor: pointer; width: fit-content; }
details.help p { margin: .3rem 0; max-width: 46rem; }
.pager { display: flex; flex-wrap: wrap; gap: .6rem 1.2rem; align-items: center; margin: 1rem 0; }
.site-footer { text-align: center; color: var(--muted); font-size: .875rem; padding: 1.5rem 1rem;
  line-height: 2; }

/* Proof trees. */
.properties li { padding: .4em 0; border-bottom: 1px solid var(--line); }
.proof-tree, .premises { list-style: none; padding-left: .8rem; margin: .3rem 0; border-left: 1px dotted var(--line); }
.proof-edge { margin: .35rem 0; overflow-wrap: anywhere; }
.proof-edge summary { cursor: pointer; }
.theorem { margin: .3rem 0 .3rem .8rem; font-size: .9rem; color: var(--muted); overflow-wrap: anywhere; }
.claim-explanation { margin: .15rem 0; }

/* OEIS submission text. */
details.oeis-text { border: 1px solid var(--line); border-radius: 4px; padding: .3em .8em; margin: .6em 0; background: var(--card); }
details.oeis-text summary { cursor: pointer; }
.oeis-field { margin: .6em 0; }
.oeis-field-head { display: flex; gap: .5rem; align-items: center; font-size: .9rem; margin-bottom: .2em; }
pre.oeis-value { margin: 0; white-space: pre; max-height: 24em; overflow: auto; }
/* Copy buttons: a small clipboard icon at the top-right corner of each copyable
   block; it shows a check mark (and "Copied!") for a moment after copying.  The
   buttons appear only when the script can copy (class `ready`). */
.copyable { position: relative; }
.copyable pre { padding-right: 2.6em; }
.copy-btn { display: none; position: absolute; top: .3em; right: .3em; align-items: center; gap: .3em;
  padding: 3px; border: 1px solid var(--line); border-radius: 4px; background: var(--card);
  color: var(--muted); cursor: pointer; line-height: 0; }
.copy-btn.ready { display: inline-flex; }
.copy-btn:hover, .copy-btn:focus-visible { color: var(--accent); border-color: var(--accent); }
.copy-btn .icon-check, .copy-btn .copy-feedback { display: none; }
.copy-btn.copied { color: #2e7d32; border-color: #2e7d32; }
.copy-btn.copied .icon-copy { display: none; }
.copy-btn.copied .icon-check { display: inline; }
.copy-btn.copied .copy-feedback { display: inline; font-size: .75rem; line-height: 1; padding-right: .2em; }
.tool-btn { font-size: .8rem; padding: 2px 10px; border: 1px solid var(--line); border-radius: 3px;
  background: var(--badge); color: var(--fg); cursor: pointer; font-family: inherit; }
.tool-btn:hover { background: var(--line); }
.tool-btn:disabled { opacity: .6; cursor: progress; }

/* Node pages: headline, map chain, chips and the proved line. */
.node-head h1 { margin-bottom: .15em; }
.node-chain { margin: 0 0 .3em; color: var(--muted); overflow-wrap: break-word; }
.head-chips { margin: .3em 0 0; line-height: 1.9; }
.property-line { margin: .4em 0 .8em; line-height: 1.7; }
.property-line .prop[title] { text-decoration: underline dotted var(--muted); text-underline-offset: 3px;
  cursor: help; }
.property-line .sep { color: var(--muted); padding: 0 .15em; }
.definition { margin: .8rem 0; padding: .3rem 0 .3rem .8rem; border-left: 3px solid var(--line); min-width: 0; }
.definition-head { margin: 0 0 .2rem; font-size: .95rem; }
.definition-head .muted { margin-left: .3rem; }
.poly-rows { overflow-x: auto; overflow-y: hidden; }
.poly-row { padding: .25em 0; white-space: nowrap; }
/* Scroll shadows: a soft edge shows that a container has more content sideways. */
.scroll-x {
  background:
    linear-gradient(to right, var(--bg) 30%, rgba(0, 0, 0, 0)) left center / 2rem 100% no-repeat local,
    linear-gradient(to left, var(--bg) 30%, rgba(0, 0, 0, 0)) right center / 2rem 100% no-repeat local,
    radial-gradient(farthest-side at 0 50%, var(--shadow), rgba(0, 0, 0, 0)) left center / .7rem 100% no-repeat scroll,
    radial-gradient(farthest-side at 100% 50%, var(--shadow), rgba(0, 0, 0, 0)) right center / .7rem 100% no-repeat scroll;
}
details.technical { margin: 2rem 0 .5rem; border: 1px solid var(--line); border-radius: 8px;
  padding: .4rem .9rem; background: var(--card); }
details.technical > summary { cursor: pointer; color: var(--muted); font-weight: 600; }
details.technical[open] > summary { margin-bottom: .4rem; }
details.technical h3 { font-size: .95rem; }
.facts { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: .25rem 1rem; margin: .3rem 0;
  font-size: .9rem; }
.facts dt { color: var(--muted); }
.facts dd { margin: 0; min-width: 0; }
.observations { font-size: .9rem; padding-left: 1.2rem; margin: .3rem 0 .5rem; }
@media (max-width: 30rem) {
  .facts { grid-template-columns: minmax(0, 1fr); gap: 0; }
  .facts dd { margin-bottom: .35rem; }
}

/* Coefficient tables: one row per n, coefficients right-aligned.  The table
   scrolls inside its container; the index column (n) sticks to the left and the
   row sums to the right, each with a soft shadow over the scrolled cells. */
.table-scroll { overflow-x: auto; max-width: 100%; }
table.coeffs { width: auto; min-width: 0; font-variant-numeric: tabular-nums; font-size: .9rem; }
table.coeffs th, table.coeffs td { padding: .15em .5em; white-space: nowrap; }
table.coeffs thead th { color: var(--muted); font-weight: 600; }
table.coeffs tbody th { color: var(--muted); font-weight: normal; }
table.coeffs thead th:first-child, table.coeffs tbody th {
  position: sticky; left: 0; z-index: 1; background: var(--bg);
  box-shadow: 6px 0 6px -6px var(--shadow); }
table.coeffs .sum { position: sticky; right: 0; z-index: 1; background: var(--bg);
  border-left: 1px solid var(--line); box-shadow: -6px 0 6px -6px var(--shadow); }
.row-tools { margin: .5em 0 1em; }
.toolbar { display: flex; flex-wrap: wrap; gap: .4rem 1rem; align-items: center; margin: .5em 0;
  padding: .35rem .5rem; border: 1px solid var(--line); border-radius: 6px; background: var(--card);
  font-size: .875rem; }
.tool-group { display: inline-flex; gap: .35rem; align-items: center; }
.row-generator { display: flex; flex-wrap: wrap; gap: .4rem .8rem; align-items: center; margin: .5em 0; }
.row-generator[hidden] { display: none; }
.row-generator input[type=number] { width: 6.5em; padding: .2em .4em; }
.row-generator label { display: inline-flex; gap: .35rem; align-items: center; }
.gen-result { flex-basis: 100%; }
.gen-status:empty { display: none; }
.js-only-note { margin-top: .2em; }

/* Tabs: every panel is in the page.  With :has (all current browsers) one panel is
   shown at a time: the one addressed by the URL fragment (#sequence, #oeis,
   #proof, or an anchor inside a panel), else the first; older browsers show all. */
.tabs { display: flex; gap: .2rem; border-bottom: 1px solid var(--line); margin: .6rem 0 .8rem;
  position: sticky; top: 0; background: var(--bg); z-index: 2; overflow-x: auto; }
.tabs a { padding: .45em .9em; border: 1px solid transparent; border-bottom: none;
  border-radius: 6px 6px 0 0; color: var(--muted); white-space: nowrap; }
.tabs a:hover { text-decoration: none; color: var(--fg); }
.tab-count { font-size: .75rem; color: var(--muted); }
.tab-panel { scroll-margin-top: 3rem; }
.tab-panel > h2:first-child { margin-top: .4em; }
@supports selector(:has(*)) {
  .tabbed .tab-panel { display: none; }
  .tabbed .tab-panel:target, .tabbed .tab-panel:has(:target) { display: block; }
  .tabbed:not(:has(.tab-panel:target, .tab-panel :target)) .tab-panel.tab-default { display: block; }
  .tabbed:has(#sequence:target, #sequence :target) .tabs a[data-tab=sequence],
  .tabbed:has(#oeis:target, #oeis :target) .tabs a[data-tab=oeis],
  .tabbed:has(#proof:target, #proof :target) .tabs a[data-tab=proof],
  .tabbed:not(:has(.tab-panel:target, .tab-panel :target)) .tabs a[data-tab=sequence] {
    color: var(--fg); background: var(--card); border-color: var(--line); margin-bottom: -1px;
    font-weight: 600; }
}
@media (max-width: 40rem) {
  .tabs a { padding: .45em .7em; }
  table.coeffs { font-size: .85rem; }
}
.oeis-matches li { padding: .35em 0; border-bottom: 1px solid var(--line); }

.filter-check label { display: inline-flex; align-items: center; gap: .35rem; cursor: pointer; }
.help-tip { position: relative; display: inline-flex; align-items: center; justify-content: center;
  width: 1.05rem; height: 1.05rem; margin-left: .3rem; border-radius: 50%; border: 1px solid var(--muted);
  color: var(--muted); font-size: .72rem; font-weight: 600; line-height: 1; cursor: help; user-select: none; }
.help-tip:hover, .help-tip:focus { color: var(--fg); border-color: var(--fg); outline: none; }
.help-tip::after { content: attr(data-tip); position: absolute; z-index: 20; top: calc(100% + .4rem); left: 50%;
  transform: translateX(-50%); width: max-content; max-width: min(18rem, 80vw); padding: .45rem .6rem;
  border-radius: .35rem; background: var(--fg); color: var(--bg); font-size: .8rem; font-weight: 400;
  line-height: 1.35; white-space: normal; text-align: left; box-shadow: 0 2px 8px rgba(0,0,0,.2);
  opacity: 0; visibility: hidden; transition: opacity .12s; pointer-events: none; }
.help-tip:hover::after, .help-tip:focus::after { opacity: 1; visibility: visible; }

/* Theorem citations of proof steps: short name, [labels], links, (?) tip with the original text */
.step-name { font-weight: 600; color: var(--fg); }
.step-link { margin-left: .3rem; }
.help-tip-wide::after { left: 0; transform: none; max-width: min(34rem, 80vw); }
.references { padding-left: 0; list-style: none; font-size: .9rem; }
.references li { margin: .35rem 0; overflow-wrap: anywhere; }
.references li:target { background: var(--line); }
.ref-label { display: inline-block; min-width: 3.2rem; font-weight: 600; }
.ref-title { font-style: italic; }

/* Sequence list: sort control and the collapsed Advanced section with paired range sliders */
.sort-control { display: inline-flex; align-items: center; gap: .35rem; font-size: .95rem; }
.sort-control select { max-width: 11rem; }
.advanced { flex: 1 1 100%; border-top: 1px solid var(--line); padding-top: .4rem; }
.advanced summary { cursor: pointer; font-size: .95rem; }
.range-filter { display: flex; flex-wrap: wrap; align-items: center; gap: .3rem .8rem; margin: .5rem 0; }
.range-name { flex: 0 0 11rem; font-size: .95rem; }
.range-inputs { display: inline-flex; align-items: center; gap: .4rem; }
.range-inputs input[type=number] { width: 4.6rem; }
.dual-range { position: relative; flex: 1 1 12rem; min-width: 9rem; height: 1.6rem; }
.dual-range[hidden] { display: none; }
.dual-range::before { content: ''; position: absolute; left: 0; right: 0; top: 50%; height: 4px; margin-top: -2px;
  border-radius: 2px; background: var(--line); }
.dual-range input[type=range] { position: absolute; left: 0; top: 0; width: 100%; height: 100%; margin: 0;
  background: none; pointer-events: none; -webkit-appearance: none; appearance: none; }
.dual-range input[type=range]::-webkit-slider-runnable-track { background: none; height: 100%; }
.dual-range input[type=range]::-moz-range-track { background: none; }
.dual-range input[type=range]::-webkit-slider-thumb { -webkit-appearance: none; appearance: none; pointer-events: auto;
  width: 1.1rem; height: 1.1rem; margin-top: .25rem; border-radius: 50%; border: 2px solid var(--accent);
  background: var(--bg); cursor: pointer; }
.dual-range input[type=range]::-moz-range-thumb { pointer-events: auto; width: .9rem; height: .9rem; border-radius: 50%;
  border: 2px solid var(--accent); background: var(--bg); cursor: pointer; }
.dual-range input[type=range]:focus-visible::-webkit-slider-thumb { outline: 2px solid var(--accent); outline-offset: 2px; }
@media (max-width: 600px) { .range-name { flex-basis: 100%; } .dual-range { flex-basis: 100%; } }

/* Hidden tips must not widen the page; on phones a tip spans the viewport below its (?) */
.help-tip:not(:hover):not(:focus)::after { display: none; }
@media (max-width: 600px) {
  .help-tip::after, .help-tip-wide::after { position: fixed; left: 1rem; right: 1rem; width: auto;
    max-width: none; transform: none; }
}