/* Plectis Atlas: the family page (scripts/family_page.py).

   The reading register of the Plectis maths pages: the mathematics first, set in
   the serif at reading size, every evidence state said in words. One centrepiece,
   the theorem; then the Lean beside it with the qualification at the join; then
   who has checked it, as sentences. No symbols that need a key. A side column on
   wide screens carries the contents and, when a record is selected, its details
   (inspect.css). Colours come from atlas.css: steel for Lean, brick for the paper
   side's own marks, low-chroma greys for structure, one flat ground. */

:root {
  --fx-lean-mono: var(--lean-mono, "Atlas Lean Mono", "JuliaMono", "DejaVu Sans Mono", Menlo, "Cascadia Mono", Consolas,
    "Noto Sans Mono", "Liberation Mono", "Plectis Math", "STIX Two Math", "Cambria Math", "Apple Symbols",
    "Segoe UI Symbol", monospace);
  --fx-measure: 40rem;
}

/* ---- The head ---------------------------------------------------------- */
.fx { --fx-col: 100%; --fx-rail: 0px; --fx-gap: 0px; }
@media (min-width: 1240px) { .fx { --fx-col: 52rem; --fx-rail: 232px; --fx-gap: 48px; } }
@media (min-width: 1700px) { .fx { --fx-col: 68rem; --fx-rail: 260px; --fx-gap: 56px; } }
.fx-head > :not(.fx-bar) { max-width: var(--fx-col); }
.fx-head > .fx-bar, .fx-head > .sib { max-width: calc(var(--fx-col) + var(--fx-gap) + var(--fx-rail)); }
.fx-bar { display: flex; flex-wrap: wrap; align-items: center; justify-content: space-between; gap: 8px 24px; margin-bottom: 16px; }
.fx-bar .trail { margin: 0; }
.fx-tools { display: flex; flex-wrap: wrap; gap: 8px; margin: 0; }
.fx-title { font-family: var(--serif); font-weight: 500; font-size: clamp(1.9rem, 1.3rem + 1.8vw, 2.75rem); line-height: 1.14; letter-spacing: -0.014em;
  margin: 0 0 14px; max-width: 24em; text-wrap: balance; overflow-wrap: break-word; }
.fx-title--long { font-size: clamp(1.7rem, 1.25rem + 1.3vw, 2.25rem); }
.fx-quote { margin: 0; max-width: var(--fx-measure); }
.fx-quote__src { margin: 0 0 6px; font-size: var(--fs-meta); color: var(--muted); }
.fx-quote__src a { color: var(--ink-soft); }
.fx-quote__q { margin: 0; padding: 2px 0 2px 18px; border-left: 2px solid var(--rule-strong); }
.fx-quote__q p { font-family: var(--serif); font-size: 1.125rem; line-height: 1.62; color: var(--ink-soft); margin: 0; text-wrap: pretty; }
.fx-fact { max-width: var(--fx-measure); margin: 14px 0 0; font-size: var(--fs-body); color: var(--ink-soft); line-height: 1.55; }
.fx-fact a:not(.ext) { color: var(--ink-soft); text-decoration-color: var(--rule-control); }
.fx-nw { white-space: nowrap; }
.fx-diagram, .fx-st .stmt__diagram { display: block; margin: 0.6em 0; padding: 8px 12px; border: 1px dashed var(--rule-strong); border-radius: var(--r-sm); font-family: var(--sans); font-size: var(--fs-small); color: var(--muted); }

/* ---- Body and side column ------------------------------------------------ */
.fx-body { margin-top: 8px; }
.fx-main { min-width: 0; container-type: inline-size; container-name: fxmain; }
.fx-aside .fx-toc { display: none; }
@media (min-width: 1240px) {
  .fx-body { display: grid; grid-template-columns: minmax(0, var(--fx-col)) var(--fx-rail); gap: var(--fx-gap); align-items: start; justify-content: start; }
  .fx-aside .fx-toc { display: block; }
  .fx-aside { display: block; position: sticky; top: 16px; max-height: calc(100vh - 32px); overflow: auto; padding-top: 28px; }
  .fx-aside__in { display: grid; gap: 18px; }
}
.fx-toc__h { margin: 0 0 6px; font-size: var(--fs-small); font-weight: 600; color: var(--muted); }
.fx-toc ol { list-style: none; margin: 0; padding: 0; border-left: 1px solid var(--rule); }
.fx-toc li a { display: block; padding: 4px 0 4px 12px; margin-left: -1px; border-left: 1px solid transparent; font-size: var(--fs-meta); color: var(--muted); text-decoration: none; line-height: 1.35; }
.fx-toc li a:hover { color: var(--ink); border-left-color: var(--rule-control); }
.fx-toc li a[aria-current="true"] { color: var(--ink); border-left-color: var(--ink); }

/* ---- Sections ------------------------------------------------------------ */
.fx-sec { margin-top: 56px; padding-top: 36px; border-top: 1px solid var(--rule); scroll-margin-top: 12px; }
.fx-sec--theorem { margin-top: 26px; padding-top: 0; border-top: 0; }
/* The theorem section ends on the status lines' bottom rule, which is also the next
   section's rule: no second rule and no empty band between them. */
.fx-sec--theorem + .fx-sec { margin-top: 0; border-top: 0; }
.fx-sec--quiet .fx-h2 { font-size: 1.375rem; color: var(--ink-soft); }
.fx-h2 { font-family: var(--serif); font-weight: 500; font-size: 1.75rem; line-height: 1.25; letter-spacing: -0.008em; margin: 0 0 10px; text-wrap: balance; }
.fx-h3 { font-family: var(--serif); font-weight: 600; font-size: 1.1875rem; line-height: 1.3; margin: 36px 0 8px; scroll-margin-top: 12px; }
.fx-h4 { font-family: var(--sans); font-weight: 600; font-size: var(--fs-base); margin: 24px 0 6px; }
.fx-intro { color: var(--muted); max-width: var(--fx-measure); font-size: var(--fs-body); line-height: 1.55; margin: 0 0 16px; text-wrap: pretty; }
.fx-prose { max-width: var(--fx-measure); font-size: var(--fs-base); line-height: 1.6; color: var(--ink-soft); }
.fx-lead-s { max-width: var(--fx-measure); font-family: var(--serif); font-size: 1.0625rem; line-height: 1.55; color: var(--ink); margin: 0 0 10px; text-wrap: pretty; }
.fx-muted { color: var(--muted); }
.fx-alias, .fam-alias { display: block; height: 0; scroll-margin-top: 12px; }
.fx-tag, .fam-tag { font-size: var(--fs-small); color: var(--steel-text); }
.fx-plain { margin: 0; padding-left: 1.1em; max-width: 64ch; font-size: var(--fs-body); line-height: 1.55; color: var(--ink-soft); }
.fx-plain li { margin: 4px 0; }
.fx-plain code, .fx-left code, .fx-draft code, .fx-rd code, .fx-join code { font-family: var(--fx-lean-mono); font-size: 0.86em; overflow-wrap: anywhere; }

/* ---- A paper statement, exactly as printed ---------------------------------- */
.fx-st { margin: 0 0 18px; padding: 18px 22px 12px; background: var(--surface); border: 1px solid var(--rule-strong); border-radius: var(--r-lg); scroll-margin-top: 12px; }
.fx-st__head { font-family: var(--serif); font-size: 1.125rem; line-height: 1.35; font-weight: 400; margin: 0 0 2px; }
.fx-st__kind { font-weight: 700; color: var(--ink); }
.fx-st__title { font-style: italic; color: var(--ink-soft); }
.fx-st__src { margin: 0 0 12px; font-size: var(--fs-meta); color: var(--ink-soft); }
.fx-st__src a { color: var(--ink-soft); }
.fx-st__src a:hover { color: var(--ink); }
.fx-st__body { font-family: var(--serif); font-size: 1.0625rem; line-height: 1.62; color: var(--ink); overflow-wrap: break-word; }
.fx-st__body p { margin: 0 0 0.6em; }
.fx-st__body em { font-style: italic; }
.fx-st__body .katex-display, .fx-st__body .m[data-d="1"] { overflow-x: auto; overflow-y: hidden; max-width: 100%; }
.fx-st__foot { display: flex; flex-wrap: wrap; align-items: center; gap: 6px 16px; margin-top: 12px; padding-top: 10px; border-top: 1px solid var(--rule); }
.fx-st__acts { display: flex; flex-wrap: wrap; align-items: center; gap: 8px; margin: 0; }
.fx-st__tex { margin-left: auto; font-size: var(--fs-small); min-height: 28px; }
.fx-st--none { background: none; border-style: dashed; padding: 16px 20px; }
.fx-st__none { margin: 0 0 6px; font-family: var(--serif); font-size: 1.0625rem; color: var(--ink-soft); }

/* The centrepiece: the theorem, set large. */
.fx-st--big { padding: 24px 36px 18px; border-color: var(--rule-strong); }
.fx-st--big .fx-st__head { font-size: 1.5rem; margin-bottom: 4px; }
.fx-st--big .fx-st__src { font-size: var(--fs-meta); margin-bottom: 18px; }
.fx-st--big .fx-st__body { font-size: 1.3125rem; line-height: 1.6; }
.fx-st--big .fx-st__foot { margin-top: 18px; padding-top: 14px; }
@media (max-width: 640px) {
  .fx-st { padding: 14px 16px 10px; }
  .fx-st--big { padding: 20px 18px 12px; }
  .fx-st--big .fx-st__head { font-size: 1.3rem; }
  .fx-st--big .fx-st__body { font-size: 1.15rem; }
}
/* The heading group: what the object is (number, title, paper, date) and, for a possible
   match, what the atlas proposes about it, in the interface face and set apart from the
   paper's own words below by one rule. The qualification is part of the heading, never
   small print at the card's foot; the other possible matches are named there too. */
.fx-st__hg--state { margin-bottom: 14px; padding-bottom: 12px; border-bottom: 1px solid var(--rule); }
.fx-st__hg--state .fx-st__src { margin-bottom: 8px; }
.fx-st--big .fx-st__hg--state { margin-bottom: 18px; padding-bottom: 16px; }
.fx-st--big .fx-st__hg--state .fx-st__src { margin-bottom: 10px; }
.fx-st__state { display: grid; gap: 4px; }
.fx-st__qual, .fx-st__alt { margin: 0; max-width: 68ch; font-family: var(--sans); font-size: var(--fs-meta); line-height: 1.5; color: var(--ink-soft); text-wrap: pretty; }
.fx-st__qual .fx-why, .fx-st__alt .fx-why { margin-left: 2px; font-size: var(--fs-meta); color: var(--ink-soft); }
.fx-st__alt .fx-why { margin-left: 0; }
.fx-st__alt a { color: var(--ink-soft); text-decoration: underline; text-decoration-thickness: 1px; text-underline-offset: 0.18em; text-decoration-color: color-mix(in oklab, currentColor 40%, transparent); }
.fx-st__alt a:hover { color: var(--ink); }
.fx-st__altk { font-weight: 600; white-space: nowrap; }
.fx-cand { max-width: 80ch; margin: 12px 0 0; font-size: var(--fs-small); line-height: 1.5; color: var(--muted); }
/* The rail's record of a possible match carries the paper and date under its number, in
   the same heading group (two papers can each have a Theorem 1.1). */
.ins-rec__title:has(+ .ins-rec__sub) { margin-bottom: 1px; }
.ins-rec__sub { margin: 0 0 8px; font-size: var(--fs-small); line-height: 1.45; color: var(--muted); overflow-wrap: anywhere; }
.fx-cand--open { font-family: var(--serif); font-size: 1.0625rem; color: var(--ink-soft); margin: 0 0 14px; max-width: var(--fx-measure); }
.fx-h2--theorem { margin-bottom: 4px; font-size: 1.5rem; }

/* Two lines kept apart: the formal status and the readable argument. */
.fx-status { margin: 22px 0 0; display: grid; gap: 0; }
.fx-status__row { display: grid; grid-template-columns: 11rem minmax(0, 1fr); gap: 4px 18px; padding: 10px 0; border-top: 1px solid var(--rule); }
.fx-status__row:last-child { border-bottom: 1px solid var(--rule); }
.fx-status dt { font-size: var(--fs-meta); font-weight: 600; color: var(--ink-soft); padding-top: 1px; }
.fx-status dd { margin: 0; font-size: var(--fs-body); line-height: 1.55; color: var(--ink-soft); }
.fx-status a { color: var(--ink-soft); }
.fx-status a:hover { color: var(--ink); }
@media (max-width: 560px) { .fx-status__row { grid-template-columns: 1fr; } }

/* Compact rows of statements (alternatives). */
.fx-alts { list-style: none; margin: 4px 0 0; padding: 0; }
.fx-alt { padding: 7px 0; border-top: 1px solid var(--rule); font-size: var(--fs-body); }
.fx-alt__k { font-family: var(--serif); font-weight: 600; font-size: 1rem; }
.fx-alt__p { color: var(--ink-soft); }
.fx-alt__s { color: var(--muted); font-size: var(--fs-small); }
.fx-alt .ins { font-size: var(--fs-small); color: var(--muted); white-space: nowrap; }
.fx-others { margin-top: 22px; }
.fx-others .fx-h3 { margin-top: 0; font-size: 1.0625rem; }

/* ---- The Lean beside the theorem ---------------------------------------------- */
/* The Lean statements, one entry each in the same rhythm: the mathematical name (the
   link that chooses it), the formal identifier on its own line in the code face, then
   two labelled lines with separate jobs, the paper theorem and the re-runs. Gaps inside
   an entry are smaller than the gaps between entries. The chosen entry is marked by a
   bar and a heavier name as well as by colour. */
.fx-idx { margin: 18px 0 26px; }
.fx-idx .fx-h3 { margin-top: 0; }
.fx-idx__list { list-style: none; margin: 0; padding: 0; }
.fx-idx__i { position: relative; padding: 14px 0 15px; border-top: 1px solid var(--rule); }
.fx-idx__i:last-child { border-bottom: 1px solid var(--rule); }
.fx-idx__i:has(> .fx-idx__a[aria-current="true"])::before { content: ""; position: absolute; left: -13px; top: 14px; bottom: 15px; width: 3px; border-radius: 2px; background: var(--steel-text); }
/* The name chooses the comparison shown below (family.js). Every name rests on a faint
   rule (a border, so it runs unbroken under typeset mathematics) that reads as a control
   and turns full strength under the pointer; the chosen one is bold over a heavier steel
   rule, beside the steel marker. The identifier under it opens the Lean page: steel
   code, underlined on hover. */
.fx-idx__a { display: inline-flex; align-items: center; min-height: 24px; color: var(--ink); text-decoration: none; }
.fx-idx__t { font-family: var(--serif); font-size: 1.0625rem; line-height: 1.35; color: var(--ink);
  padding-bottom: 1px; border-bottom: 1px solid color-mix(in oklab, currentColor 30%, transparent); }
.fx-idx__a:hover { text-decoration: none; }
.fx-idx__a:hover .fx-idx__t { border-bottom-color: currentColor; }
.fx-idx__a[aria-current="true"] .fx-idx__t { font-weight: 600; border-bottom: 2px solid var(--steel-text); }
.fx-idx__id > a:not(:hover) { text-decoration: none; }
.fx-idx__id { margin: 1px 0 0; font-size: var(--fs-small); line-height: 1.45; color: var(--muted); }
.fx-idx__id code { font-family: var(--fx-lean-mono); font-size: 0.95em; color: var(--steel-text); overflow-wrap: anywhere; }
.fx-idx__dl { display: grid; grid-template-columns: 6.25rem minmax(0, 1fr); gap: 2px 12px; margin: 8px 0 0; font-size: var(--fs-small); line-height: 1.5; }
.fx-idx__dl > div { display: contents; }
.fx-idx__dl dt { font-weight: 600; color: var(--muted); }
.fx-idx__dl dd { margin: 0; color: var(--ink-soft); max-width: 72ch; }
@container fxmain (max-width: 480px) {
  .fx-idx__dl { grid-template-columns: minmax(0, 1fr); gap: 0; }
  .fx-idx__dl dd { margin-bottom: 4px; }
}

.fx-cmp { margin-top: 26px; scroll-margin-top: 12px; }
.fx-cmp:first-child { margin-top: 8px; }
/* With scripts on, one comparison stands at a time: the build hides the others before
   the first paint (family_page.comparison_one); without scripts every one is shown. */
:root.js .fx-cmp--rest { display: none; }
:root.js .fx-cmp + .fx-cmp { margin-top: 8px; }
.fx-cmp__h { margin: 0 0 10px; font-family: var(--sans); font-size: var(--fs-base); font-weight: 600; color: var(--ink-soft); }
.fx-cmp__h code { font-family: var(--fx-lean-mono); font-size: 0.95em; color: var(--ink); overflow-wrap: anywhere; }
.fx-cmp__side { margin: 0 0 6px; font-size: var(--fs-small); font-weight: 600; color: var(--muted); }
.fx-cmp__lhead { margin: 0 0 6px; }
.fx-cmp__state { margin: 0; font-size: var(--fs-meta); font-weight: 600; color: var(--ink); }
.fx-cmp__qual { margin: 0; font-size: var(--fs-small); font-style: italic; color: var(--ink-soft); }
.fx-st__role { margin: 0 0 4px; font-size: var(--fs-small); font-weight: 600; color: var(--muted); }
.fx-cmp__grid { display: grid; grid-template-columns: minmax(0, 1fr); grid-template-areas: "paper" "join" "lean"; gap: 0; }
.fx-cmp__paper { grid-area: paper; min-width: 0; }
.fx-cmp__lean { grid-area: lean; min-width: 0; }
.fx-cmp__grid .fx-st { margin-bottom: 0; max-width: none; }
.fx-cmp__why { margin: 6px 0; font-size: var(--fs-small); color: var(--muted); }
/* The join: the words that qualify the two statements' being side by side. Between
   them when they stack; a band across both, above them, when they stand side by side. */
.fx-join { grid-area: join; margin: 14px 0; padding: 8px 0 8px 14px; border-left: 2px solid var(--steel); font-size: var(--fs-body); line-height: 1.55; color: var(--ink-soft); max-width: 48rem; }
.fx-join--unavailable { border-left-color: var(--rule-control); }
.fx-join__quote { display: block; margin-top: 6px; font-size: var(--fs-small); color: var(--muted); }
@container fxmain (min-width: 860px) {
  .fx-cmp__grid { grid-template-columns: minmax(0, 1fr) minmax(0, 1fr); grid-template-areas: "join join" "paper lean"; gap: 0 24px; align-items: start; }
  .fx-join { margin: 0 0 16px; }
}

.fx-lean { padding: 16px 18px 12px; background: var(--surface); border: 1px solid color-mix(in oklab, var(--steel) 40%, var(--rule-strong)); border-radius: var(--r-lg); }
.fx-lean__head { margin: 0 0 2px; font-family: var(--serif); font-size: 1.125rem; font-weight: 600; line-height: 1.35; }
.fx-lean__head a { color: var(--ink); text-decoration: none; }
.fx-lean__head a:hover { text-decoration: underline; }
.fx-lean__file { margin: 0 0 10px; font-size: var(--fs-small); color: var(--muted); }
.fx-lean__file code { font-family: var(--fx-lean-mono); color: var(--steel-text); overflow-wrap: anywhere; }
.fx-lean__code { font-family: var(--fx-lean-mono); margin: 0 0 8px; }
.fx-lean__code code { font-family: inherit; }
.fx-lean__code .x { color: var(--muted); font-weight: 600; }
.fx-lean__more, .fx-lean__note, .fx-lean__runs, .fx-lean__go { margin: 6px 0 0; font-size: var(--fs-small); line-height: 1.5; color: var(--ink-soft); }
.fx-lean__more code, .fx-lean__note code { font-family: var(--fx-lean-mono); }
.fx-lean__terms { list-style: none; margin: 4px 0 0; padding: 0; font-size: var(--fs-small); color: var(--ink-soft); line-height: 1.5; }
.fx-forms { list-style: none; padding: 0; margin: 0; }
.fx-forms li { margin: 12px 0; }

/* ---- Who has checked it --------------------------------------------------------- */
.fx-rds { display: grid; gap: 0 32px; align-items: start; }
@container fxmain (min-width: 760px) { .fx-rds { grid-template-columns: 1fr 1fr; } }
.fx-rd { padding: 12px 0 8px; border-top: 1px solid var(--rule); min-width: 0; }
.fx-rd__v { margin: 0 0 8px; font-family: var(--serif); font-size: 1.0625rem; line-height: 1.5; color: var(--ink); }
.fx-rd--none .fx-rd__v { color: var(--muted); }
.fx-rd__who { font-weight: 600; }
.fx-rd__note { margin: 0 0 6px; font-size: var(--fs-body); line-height: 1.55; color: var(--ink-soft); overflow-wrap: break-word; }
.fx-rd__k { font-weight: 600; color: var(--ink-soft); }
.fx-rd__def, .fx-rd__method { margin: 0 0 6px; font-size: var(--fs-small); line-height: 1.5; color: var(--muted); }
.fx-rd__links { display: flex; flex-wrap: wrap; align-items: center; gap: 4px 14px; margin: 6px 0 0; font-size: var(--fs-small); }
/* The AI agent's drafts: a subordinate group after the outside readers and OpenAI's
   note, smaller and quieter, each naming the Lean statement it classifies. */
.fx-drafts { margin-top: 30px; max-width: var(--fx-measure); }
.fx-drafts__h { margin: 0 0 4px; font-size: var(--fs-meta); color: var(--ink-soft); }
.fx-draft { list-style: none; margin: 0; padding: 0; font-size: var(--fs-small); line-height: 1.5; color: var(--muted); }
.fx-draft__i { padding: 8px 0; border-top: 1px solid var(--rule); }
.fx-draft__obj { margin: 0; color: var(--ink-soft); }
.fx-draft__t { font-family: var(--serif); font-size: var(--fs-meta); }
.fx-draft__obj code { color: var(--steel-text); }
.fx-draft__v { margin: 2px 0 0; }
.fx-draft__k { font-weight: 600; }
.fx-producer { margin-top: 18px; max-width: var(--fx-measure); }
.fx-producer__h { margin: 0 0 4px; font-size: var(--fs-meta); font-weight: 600; }
.fx-producer__q { margin: 0; padding-left: 14px; border-left: 2px solid var(--rule-strong); font-size: var(--fs-body); line-height: 1.55; color: var(--ink-soft); }

/* Re-runs, grouped by the Lean statement they ran: its name heads the group, with any
   fact true of every record in it; inside, one row per report with the same fields in
   the same columns, so reporters, words, accounts, dates and receipts can be compared.
   In a narrow column each row stacks its fields, labelled, in the same order. */
.fx-rg { margin: 24px 0 0; scroll-margin-top: 12px; }
.fx-rg__h { margin: 0; font-family: var(--sans); font-size: var(--fs-base); font-weight: 600; line-height: 1.4; color: var(--ink); }
.fx-rg__t { font-family: var(--serif); font-size: 1.0625rem; }
.fx-rg__h code { font-family: var(--fx-lean-mono); font-size: 0.8125rem; font-weight: 400; color: var(--steel-text); overflow-wrap: anywhere; }
.fx-rg__common { margin: 2px 0 8px; font-size: var(--fs-small); color: var(--muted); }
.fx-rt { width: 100%; border-collapse: collapse; font-size: var(--fs-small); line-height: 1.5; color: var(--ink-soft); }
.fx-rt thead th { padding: 0 14px 6px 0; text-align: left; vertical-align: bottom; font-weight: 600; color: var(--muted); border-bottom: 1px solid var(--rule-strong); white-space: nowrap; }
.fx-rt tbody th, .fx-rt td { padding: 9px 14px 9px 0; text-align: left; vertical-align: top; font-weight: 400; border-bottom: 1px solid var(--rule); }
.fx-rt tr > :last-child { padding-right: 0; }
.fx-rt tbody th { width: 22%; color: var(--ink); }
.fx-rt tbody td:nth-child(2) { width: 18%; }
.fx-rt tbody td:nth-child(4) { width: 8.5rem; }
.fx-rt tbody td:nth-child(5) { width: 7.5rem; }
.fx-rt__term { color: var(--ink); overflow-wrap: anywhere; }
.fx-rt__go { display: flex; flex-wrap: wrap; align-items: baseline; gap: 0 10px; }
.fx-run__det { color: var(--muted); }
.fx-rt .ins, .fx-rd .ins, .fx-card .ins { font-size: var(--fs-small); color: var(--muted); }
@container fxmain (max-width: 600px) {
  .fx-rt, .fx-rt tbody, .fx-rt tr { display: block; }
  .fx-rt thead { display: none; }
  .fx-rt tr { padding: 8px 0 9px; border-bottom: 1px solid var(--rule); }
  .fx-rt tr:first-child { border-top: 1px solid var(--rule); }
  .fx-rt tbody th, .fx-rt td { display: grid; grid-template-columns: 6.5rem minmax(0, 1fr); gap: 0 10px; width: auto !important; padding: 1px 0; border: 0; }
  .fx-rt tbody th::before, .fx-rt td::before { content: attr(data-label); font-weight: 600; color: var(--muted); }
}

/* Checks by another method: each record leads with what it checked (the statement, as
   the paper prints it, and the paper; or the fact a HOL Light card states), then the
   same fields in the same order: who reports it, the method, their outcome in their own
   term, what it covers in their words, and the receipt. */
.fx-cards { list-style: none; margin: 0; padding: 0; }
.fx-card { padding: 14px 0 16px; border-top: 1px solid var(--rule); }
.fx-card__id { margin: 0; font-family: var(--serif); font-size: 1.0625rem; line-height: 1.45; color: var(--ink); text-wrap: pretty; overflow-wrap: break-word; }
.fx-card__id a { color: var(--ink); }
.fx-card__id a:hover { color: var(--steel-text); }
.fx-card__date { font-family: var(--sans); font-size: var(--fs-meta); color: var(--muted); }
.fx-card__sub { margin: 1px 0 0; font-size: var(--fs-small); color: var(--muted); }
.fx-fields { display: grid; grid-template-columns: 7.25rem minmax(0, 1fr); gap: 3px 14px; margin: 8px 0 0; font-size: var(--fs-small); line-height: 1.5; }
.fx-fields > div { display: contents; }
.fx-fields dt { font-weight: 600; color: var(--muted); }
.fx-fields dd { margin: 0; color: var(--ink-soft); overflow-wrap: break-word; max-width: 72ch; }
.fx-fields dd.fx-fields__scope { font-size: var(--fs-body); line-height: 1.55; color: var(--ink); }
.fx-fields__gloss { color: var(--muted); }
@container fxmain (max-width: 520px) {
  .fx-fields { grid-template-columns: minmax(0, 1fr); gap: 0; }
  .fx-fields dd { margin-bottom: 5px; }
}

.fx-finds { list-style: none; margin: 0; padding: 0; }
.fx-find { padding: 9px 0; border-top: 1px solid var(--rule); }
.fx-find__what { margin: 0; font-size: var(--fs-body); line-height: 1.55; color: var(--ink); max-width: 64ch; }
.fx-find__who { margin: 0 0 3px; font-size: var(--fs-small); color: var(--muted); }
#problems + .fx-intro + .fx-finds .fx-find { border-top-color: color-mix(in oklab, var(--brick) 35%, var(--rule)); }

/* Rows of prose keep a reading measure, whatever the column's width. */

/* ---- What is left to check --------------------------------------------------------- */
.fx-left__g .fx-h3 { font-size: 1.0625rem; margin-top: 24px; }
.fx-left { list-style: none; margin: 0; padding: 0; }
.fx-left__i { padding: 7px 0; border-top: 1px solid var(--rule); font-size: var(--fs-body); line-height: 1.5; color: var(--ink-soft); }
.fx-left__t { font-weight: 600; color: var(--ink); }
.fx-left__r { overflow-wrap: break-word; }
.fx-left__names { display: block; font-size: var(--fs-small); color: var(--muted); }
.fx-left__go { font-size: var(--fs-small); white-space: nowrap; }

/* ---- Papers (paper_row in build_site.py), connections, explain ---------------------- */
.pps { margin-top: 4px; }
.pp { padding: 18px 0 16px; border-top: 1px solid var(--rule); scroll-margin-top: 12px; }
.pp__title { font-family: var(--serif); font-size: 1.25rem; font-weight: 500; line-height: 1.3; margin: 0 0 4px; max-width: 40em; }
.pp__title a { color: var(--ink); }
.pp__title a:hover { color: var(--steel-text); }
.pp__meta { font-size: var(--fs-meta); color: var(--muted); margin: 0; }
.pp__acts { display: flex; flex-wrap: wrap; align-items: center; gap: 8px; margin: 10px 0 6px; }
.pp__prev { font-size: var(--fs-meta); color: var(--muted); margin: 6px 0; }
.pp__abstract { font-family: var(--serif); font-size: 1.0625rem; line-height: 1.6; color: var(--ink-soft); max-width: 42em; margin: 4px 0 14px; }
.pp__note { font-size: var(--fs-meta); color: var(--ink-soft); max-width: 62ch; }
.fx-checks { font-size: var(--fs-body); color: var(--ink-soft); }
.fx-checks a { margin-right: 4px; }
.fx-forms-wrap { margin-top: 28px; }
.fam-numstate { font-weight: 400; font-style: italic; color: var(--muted); font-size: 0.92em; }
.fx-pps { list-style: none; margin: 0; padding: 0; }
.fx-pp { padding: 8px 0; border-top: 1px solid var(--rule); font-family: var(--serif); font-size: 1.0625rem; scroll-margin-top: 12px; }
.fx-pp a:first-child { color: var(--ink); }
.fx-pp__m { font-family: var(--sans); font-size: var(--fs-small); color: var(--muted); }
.fx-pp__pdf { font-family: var(--sans); font-size: var(--fs-small); }
.wds { margin-top: 30px; }
.wd { padding: 14px 0; border-top: 1px solid color-mix(in oklab, var(--brick) 35%, var(--rule)); scroll-margin-top: 12px; }
.wd__title { font-family: var(--serif); font-size: 1.125rem; font-weight: 500; margin: 0 0 6px; }
.wd__title a { color: var(--ink); }
.wd__note { font-size: var(--fs-meta); color: var(--ink-soft); max-width: 62ch; }
.wd__when { font-size: var(--fs-small); color: var(--muted); margin: 4px 0 0; }
.fx-cols2 { display: grid; gap: 0 40px; }
@container fxmain (min-width: 760px) { .fx-cols2 { grid-template-columns: 1fr 1fr; } }
.fx-cols2 .fx-h3 { margin-top: 12px; }
.fx-refs { margin-top: 30px; scroll-margin-top: 12px; }
.fam-invite { font-family: var(--serif); font-size: 1.125rem; line-height: 1.55; color: var(--ink-soft); max-width: 34em; margin: 0; }
.fx-contrib { margin-top: 26px; scroll-margin-top: 12px; }
.fx-contrib .actions { margin-top: 8px; }
.rel li { max-width: 70ch; }

/* ---- No shift while the formulas are typeset ---------------------------------------
   The statements and the catalogue's words carry TeX that KaTeX typesets once the
   deferred scripts run; raw TeX is wider, so the text would reflow and move what is
   below it. With scripting on, those parts wait (invisibly, keeping their space) until
   atlas.js marks the document typeset, or 1.5 s at most, so nothing moves under the
   reader. With scripting off they show at once, as plain TeX. */
@media (scripting: enabled) {
  html:not([data-math]) .fx-quote__q, html:not([data-math]) .fx-fact, html:not([data-math]) .fx-body {
    visibility: hidden; animation: fx-typeset 0s linear 1.5s forwards;
  }
}
@keyframes fx-typeset { to { visibility: visible; } }

/* ---- One reading measure ----------------------------------------------------------
   Cards, lists and rules share the column's right edge; the prose inside them keeps a
   reading measure near 60 to 80 characters, and displayed equations take their own
   width. Nothing scrolls inside the column, and nothing is clamped. */
.fx-main :is(p, li) { max-width: 72ch; }
.fx-st__body p, .fx-st__body li { max-width: 72ch; }
.fx-st__foot p, .fx-cmp__grid p { max-width: none; }
.fx-cmp__grid .fx-st__body p { max-width: 72ch; }

/* The state of a possible match, and the quiet way to how it was found. */
.fx-why { font-size: var(--fs-small); color: var(--muted); margin-left: 4px; white-space: nowrap; }


/* A cited passage, read in place under the theorem (family.js). */
.fx-src { margin: 14px 0 4px; padding: 10px 0 8px 16px; border-left: 2px solid var(--rule-control); }
.fx-src__h { margin: 0 0 6px; font-size: var(--fs-small); font-weight: 600; color: var(--ink-soft); }
.fx-src__h:focus { outline: none; }
.fx-src__h:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.fx-src__body { font-family: var(--serif); font-size: 1rem; line-height: 1.6; color: var(--ink); }
.fx-src__body p { margin: 0 0 0.5em; max-width: 64ch; }
.fx-src__body .pr-eq { margin: 0.5em 0; overflow-x: auto; overflow-y: hidden; }
.fx-src__body .pr-thm-h { font-weight: 700; }
.fx-src__body .pr-thm-note { font-weight: 400; font-style: italic; }
.fx-src__body .pr-m--fail { font-family: var(--mono); font-size: 0.85em; }
.fx-src__foot { display: flex; flex-wrap: wrap; align-items: center; gap: 6px 16px; margin: 6px 0 0; font-size: var(--fs-small); }
.fx-st__body a.xref[aria-expanded="true"] { text-decoration-style: solid; }

/* ---- Pointing and choosing (DESIGN.md, "Motion and hover") ---------------------------
   A card or a record row answers pointing with a darker border or a faint ground, over
   the hover time; nothing lifts or moves the text. The chosen Lean statement's mark moves
   to the entry chosen and the comparisons swap in place over the state time (family.js);
   the contents mark the section being read the same way. All of it is instant when the
   reader asks for reduced motion. */
.fx-st { transition: border-color var(--t-hover, 120ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)); }
.fx-card, .fx-alt, .fx-find, .fx-draft__i, .fx-rt tbody tr, .fx-idx__i, .fx-left__i {
  transition: background-color var(--t-hover, 120ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)); }
@media (hover: hover) and (pointer: fine) {
  .fx-st:hover { border-color: var(--rule-control); }
  .fx-card:hover, .fx-alt:hover, .fx-find:hover, .fx-draft__i:hover, .fx-rt tbody tr:hover, .fx-idx__i:hover, .fx-left__i:hover {
    background-color: color-mix(in oklab, var(--sunk) 55%, transparent); }
}
.fx-toc li a { transition: color var(--t-state, 180ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)), border-color var(--t-state, 180ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)); }
/* One mark for the chosen Lean statement, moved by family.js; the per-entry bar stands in
   until then, and whenever scripts are off. */
.fx-idx { position: relative; }
.fx-idx__mark { position: absolute; left: -13px; top: 0; width: 3px; border-radius: 2px; background: var(--steel-text); pointer-events: none;
  transition: transform var(--t-state, 180ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)), height var(--t-state, 180ms) var(--ease-out, cubic-bezier(0.16, 1, 0.3, 1)); }
.fx-idx--marked .fx-idx__i::before { display: none; }
@media (prefers-reduced-motion: reduce) {
  .fx-st, .fx-card, .fx-alt, .fx-find, .fx-draft__i, .fx-rt tbody tr, .fx-idx__i, .fx-left__i, .fx-toc li a, .fx-idx__mark { transition: none; }
}

/* A note under a Lean statement keeps a reading measure (about 75 characters) however
   wide the column is. */
.fx-lean__note { max-width: 75ch; }

/* An unresolved headline: after the statements the papers print, one line of information
   on how they were chosen and where the open task is listed. */
.fx-cand--note { margin: 2px 0 18px; max-width: 75ch; }