/* Chapter 5 — What is proved? (coverage, marked identity, smoothing, error budget, scope). Prefix pf-. Apache-2.0. */
.pf-lab .ex-object svg{max-width:460px}
/* KaTeX draws radicals and wide accents as inline SVG: keep them out of the figure sizing rules above. */
.pf-lab .katex svg{display:block;width:100%;height:inherit;max-width:none;margin:0}
.pf-h{font-size:16px;margin:14px 0 4px;color:var(--muted);font-weight:600}
/* numbers never break inside a digit group; only very long ones (more than 24 characters) may wrap */
.pf-num{font-variant-numeric:tabular-nums;white-space:nowrap}
.pf-q{font-variant-numeric:tabular-nums;white-space:nowrap}
.pf-num.pf-long,.pf-q.pf-long{white-space:normal;overflow-wrap:anywhere}
.pf-mono{font-family:var(--mono);font-size:14px;overflow-wrap:anywhere}
.pf-entry label{min-width:0;flex:1 1 240px}
.pf-entry input[type=text]{width:100%}
.pf-verdict{padding:6px 10px;border-radius:6px;margin:8px 0 2px}
.pf-verdict.is-ok{background:#fff;border:1px solid var(--teal-line)}
.pf-verdict.is-no{background:#fff;border:1px solid var(--red)}
.pf-verdict.is-na{background:#fff;border:1px solid var(--control-line)}
.pf-links{font-size:15.5px}
.pf-link{color:var(--wine);text-decoration:underline;text-underline-offset:3px;display:inline-block;padding:10px 2px;min-height:44px;min-width:44px;text-align:center;box-sizing:border-box}
.pf-link:focus-visible{outline:3px solid var(--focus);outline-offset:2px}
/* links inside running text keep their 44 px target but do not stretch the line they sit on */
.ex-rule .pf-link,.ex-bridge .pf-link,.ex-legend .pf-link,.ex-note .pf-link,.pf-always .pf-link,.c2-details .pf-link{margin-top:-10px;margin-bottom:-10px;vertical-align:baseline}

/* SVG text and shared marks */
svg .pf-t{font-size:14px}
svg .pf-ts{font-size:12.5px}
svg .pf-st{font-size:14px}
svg .pf-sts{font-size:13px}
svg .pf-halo{paint-order:stroke;stroke:#fff;stroke-width:4px;stroke-linejoin:round}
.pf-sub{display:block;font-size:13.5px;color:var(--muted);margin-top:2px;line-height:1.3}
svg .pf-muted{fill:var(--muted)}
svg .pf-bold{font-weight:700}
svg .pf-teal{fill:var(--teal)}
svg .pf-intext{font-weight:700;pointer-events:none;paint-order:stroke;stroke:#fff;stroke-width:4px;stroke-linejoin:round}
.pf-marker{fill:var(--wine)}
.pf-tick{stroke:var(--ink);stroke-width:1.5;stroke-dasharray:3 2}

/* d-axis strip */
.pf-strip{display:block;width:100%;height:auto;max-width:460px;margin:0 auto}
.pf-seg{stroke-width:1.2}
.pf-seg-trivial{fill:#eef0f2;stroke:var(--slate)}
.pf-seg-cert{fill:var(--wine-tint);stroke:var(--wine)}
.pf-seg-open{fill:var(--red-tint);stroke:var(--red);stroke-dasharray:5 3}
.pf-seg-proof{fill:var(--teal-tint);stroke:var(--teal)}

/* coverage: tails and coordinates */
.pf-fwd{fill:var(--wine-tint);stroke:var(--wine);stroke-width:1.3}
.pf-rev{fill:var(--teal-tint);stroke:var(--teal);stroke-width:1.3}
.pf-sel{fill:none;stroke:var(--ink);stroke-width:3}
.pf-cellsep{stroke:#fff;stroke-width:2}
.pf-selline{stroke:var(--ink);stroke-width:3}
.pf-end{fill:#dfe3e6;stroke:var(--slate);stroke-width:1.3}
.pf-unk{fill:url(#pf-hatch);stroke:var(--ochre);stroke-width:1.3}
.pf-pos{fill:var(--teal-tint);stroke:var(--teal);stroke-width:1.3}
/* index range of Prop. 9.4 when its hypothesis d ≥ 2^72 fails: outlined only, no “positive” fill */
.pf-range{fill:#fff;stroke:var(--teal);stroke-width:1.3;stroke-dasharray:5 3}
.pf-hatch-bg{fill:var(--ochre-tint)}
.pf-hatch-line{stroke:var(--ochre-fill);stroke-width:2}
.pf-split{stroke:var(--wine);stroke-width:1.6;stroke-dasharray:5 3}
.pf-bracket{fill:none;stroke:var(--ink);stroke-width:2}
.pf-legend{list-style:none;margin:8px 0 0;padding:0;display:flex;flex-direction:column;gap:4px;font-size:15px;line-height:1.35}
.pf-legend li{display:flex;gap:8px;align-items:flex-start}
.pf-sw{flex:0 0 auto;display:inline-block;width:22px;height:14px;border-radius:3px;margin-top:3px;border:1.5px solid}
.pf-sw.pf-fwd{background:var(--wine-tint);border-color:var(--wine)}
.pf-sw.pf-rev,.pf-sw.pf-pos{background:var(--teal-tint);border-color:var(--teal)}
.pf-sw.pf-range{background:#fff;border-color:var(--teal);border-style:dashed}
.pf-sw.pf-unk{border-color:var(--ochre);background:repeating-linear-gradient(45deg,var(--ochre-fill) 0 2px,var(--ochre-tint) 2px 6px)}
.pf-sw.pf-end{background:#dfe3e6;border-color:var(--slate)}
.pf-rows{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:10px}
.pf-row{border:1px solid var(--line);border-radius:8px;background:#fff;padding:8px 12px;font-size:15.5px;line-height:1.4;min-width:0}
.pf-row p{margin:4px 0}
.pf-row.is-on{border:2px solid var(--wine);padding:7px 11px;background:var(--wine-tint)}

/* marked identity */
.pf-coords{max-width:420px}
.pf-coords .btn{min-height:44px;min-width:76px}
.pf-terms .btn{min-height:44px;min-width:64px}
.pf-neg{color:var(--ochre);font-weight:700}
.pf-times{white-space:nowrap}
.pf-sum{margin:2px 0}
.pf-sum-narrow{display:none}
.pf-dseg{margin-bottom:10px}
.pf-running{margin-top:4px}
.pf-rule-p{margin:4px 0}
.pf-why{margin:14px 0 0}
.pf-negmark{font-size:12.5px;font-weight:400;display:block}
.pf-run{display:block;width:100%;height:auto;max-width:460px}
.pf-zero{stroke:var(--control-line);stroke-width:1.2}
.pf-target{stroke:var(--teal);stroke-width:2;stroke-dasharray:6 4}
.pf-dot{fill:var(--muted)}
.pf-step-pos{stroke:var(--wine);stroke-width:3}
.pf-step-neg{stroke:var(--ochre);stroke-width:3;stroke-dasharray:7 3}
.pf-arr-pos{fill:var(--wine)}
.pf-arr-neg{fill:var(--ochre)}
#marked-term h4{margin:0}
/* the block that contains position 1, one row per term of (37); the selected term is framed, not only coloured */
.pf-terms-two{margin-top:10px}
/* two columns: the picture stays in view beside a long term table (d = 8), below the sticky chapter bar */
.pf-terms-two>#marked-blocks{position:sticky;top:64px;align-self:start}
.pf-blocks{display:block;width:100%;height:auto;max-width:460px;margin:0 auto}
.pf-blocks-one{display:block;width:100%;height:auto;max-width:460px;margin:2px 0 4px}
.pf-blk-on{fill:none;stroke:var(--ink);stroke-width:2.5}
.pf-blk-mark{fill:var(--wine);fill-opacity:.14;stroke:var(--wine);stroke-width:1.8}
.pf-blk-rest{fill:#fff;stroke:var(--slate);stroke-width:1.5;stroke-dasharray:5 3}
.pf-blk-in{fill:#fff;stroke:var(--wine);stroke-width:1.5}
.pf-blk-p1{fill:var(--wine);stroke:var(--wine);stroke-width:1.5}
.pf-blk-out{fill:#fff;stroke:var(--slate);stroke-width:1.3}
svg .pf-blk-num{font-weight:600;pointer-events:none}
svg .pf-blk-num1{fill:#fff;font-weight:700}

/* coins and their law */
.pf-pmf{display:block;width:100%;height:auto}
.pf-bar{fill:var(--wine);fill-opacity:.55;stroke:var(--wine);stroke-width:1}
.pf-bar-mode{fill-opacity:.9}
.pf-after{fill:none;stroke:var(--ink);stroke-width:2;stroke-dasharray:5 3}
.pf-mean{stroke:var(--teal);stroke-width:2;stroke-dasharray:6 4}
.pf-coins{display:grid;grid-template-columns:repeat(auto-fill,minmax(96px,1fr));gap:6px}
.pf-coin{flex-direction:column;gap:2px;min-height:64px;padding:6px 6px;font-size:14.5px;line-height:1.2}
.pf-coin .pf-coin-p{font-family:var(--mono);font-size:13.5px;overflow-wrap:anywhere}
.pf-pie{width:22px;height:22px}
.pf-pie-bg{fill:#fff;stroke:var(--ink);stroke-width:1.4}
.pf-pie-fill{fill:var(--ochre-fill);stroke:var(--ink);stroke-width:1}
.pf-pie-full{fill:var(--ochre-fill);stroke:var(--ink);stroke-width:1.4}
.pf-change-row{display:flex;flex-wrap:wrap;gap:10px;align-items:flex-start}
.pf-change-row .pf-entry{flex:1 1 300px}
.pf-change-buttons{display:flex;flex-wrap:wrap;gap:8px;padding-top:24px}
.pf-change-buttons .btn{min-height:44px}
.pf-values{max-width:560px}
.pf-exact td{vertical-align:top}

/* error budget */
.pf-budget{display:block;width:100%;height:auto}
.pf-slot{stroke:var(--control-line);stroke-width:1.2}
.pf-slot-a{fill:var(--wine-tint)}
.pf-slot-b{fill:#eef0f2}
.pf-slot-c{fill:var(--teal-tint)}
.pf-bound{fill:var(--red-tint);stroke:var(--red);stroke-width:1.4}
.pf-bound-ok{fill:var(--wine-tint);stroke:var(--wine);stroke-width:1.4}
.pf-bound-over{fill:url(#pf-over);stroke:var(--red);stroke-width:1.4}
.pf-over-bg{fill:var(--red-tint)}
.pf-over-line{stroke:var(--red);stroke-width:1.6}
.pf-break{fill:none;stroke:var(--ink);stroke-width:2}
.pf-ref{stroke:var(--teal);stroke-width:2.2;stroke-dasharray:6 4}
.pf-checks{margin:6px 0;padding-left:1.3em;display:flex;flex-direction:column;gap:6px}
.pf-parts{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:10px}
.pf-part{border:1px solid var(--line);border-radius:8px;background:#fff;padding:8px 12px;font-size:15.5px;line-height:1.4;min-width:0}
.pf-part p{margin:4px 0}
.pf-part-from{color:var(--ink);font-size:15px}
.pf-part .c2-details{padding:2px 0;margin-top:6px}
.pf-part .c2-details[open]{padding:4px 8px 6px}
.pf-combine{margin-top:4px}
.pf-exact-list{margin:4px 0;padding-left:1.1em;display:flex;flex-direction:column;gap:4px}

/* scope */
.pf-class .ex-tag{margin-right:8px}
.pf-scope-open{background:var(--red-tint);border-left-color:var(--red)}
.pf-scope-certificate{background:var(--wine-tint);border-left-color:var(--wine)}
.pf-scope-table td:first-child{white-space:nowrap}
.pf-scope-table .ex-tag{margin:2px 4px 2px 0}
.pf-always{margin:0;padding-left:1.2em;display:flex;flex-direction:column;gap:8px;font-size:16px;line-height:1.45}
.pf-evidence{display:grid;grid-template-columns:max-content 1fr;gap:8px 12px;margin:0;font-size:15.5px;line-height:1.4}
.pf-evidence dt{margin:0}
.pf-evidence dd{margin:0}

@media(max-width:760px){
 .pf-parts,.pf-rows{grid-template-columns:minmax(0,1fr)}
 /* one column: the picture comes first and scrolls normally; the term panel repeats the selected row */
 .pf-terms-two>#marked-blocks{position:static}
}
@media(max-width:640px){
 svg .pf-t{font-size:17px}
 svg .pf-ts{font-size:16px}
 svg .pf-st{font-size:19px}
 svg .pf-sts{font-size:18px}
 .pf-legend{font-size:14.5px}
 .pf-evidence{grid-template-columns:minmax(0,1fr);gap:2px 0}
 .pf-evidence dd{margin-bottom:8px}
 .pf-coins{grid-template-columns:repeat(auto-fill,minmax(88px,1fr))}
 .pf-change-buttons{padding-top:0}
 .pf-sum-wide.has-narrow{display:none}
 .pf-coords td{padding-top:2px;padding-bottom:2px}
 .pf-terms{font-size:14px}
 .pf-terms .pf-times{display:block}
 .pf-terms th,.pf-terms td{padding-left:3px;padding-right:3px}
 .pf-terms th+th,.pf-terms td+td{padding-left:8px}
 .pf-terms .btn{min-width:54px}
 .pf-sum-narrow{display:block}
 /* the term panel repeats one row inside its padding, narrower than the full picture: a larger font keeps it ≥ 12 px */
 svg.pf-blocks-one .pf-ts{font-size:18px}
}
@media(prefers-reduced-motion:reduce){.pf-lab *{transition:none!important;animation:none!important}}