/* Semantic round-trip and theorem-denoising extension for the Lean graph. */
.ulg-hero dl{grid-template-columns:repeat(3,1fr)}
.ulg-hero dl div:nth-child(2n){border-right:1px solid var(--line)}
.ulg-hero dl div:nth-child(3n){border-right:0}
.ulg-hero dl div:nth-last-child(-n+3){border-bottom:0}
.ulg-semantics>div:last-child{grid-template-columns:repeat(3,1fr)}

.ulg-node .status.fidelity-exact,.ulg-detail i.fidelity-exact,.ulg-legend i[data-status="fidelity-exact"]{fill:var(--green);background:var(--green)}
.ulg-node .status.review-required,.ulg-detail i.review-required,.ulg-legend i[data-status="review-required"]{fill:var(--yellow);background:var(--yellow)}
.ulg-node .status.fidelity-mismatch,.ulg-detail i.fidelity-mismatch,.ulg-legend i[data-status="fidelity-mismatch"]{fill:var(--red);background:var(--red)}
.ulg-node .status.fidelity-repaired,.ulg-detail i.fidelity-repaired,.ulg-legend i[data-status="fidelity-repaired"]{fill:var(--accent);background:var(--accent)}
.ulg-node .status.proposal,.ulg-detail i.proposal,.ulg-legend i[data-status="proposal"]{fill:var(--purple);background:var(--purple)}

.ulg-semantic-verdict .ulg-verdict{display:grid;gap:5px;padding:12px;border:1px solid var(--line);border-radius:10px;background:linear-gradient(110deg,color-mix(in srgb,var(--accent-soft) 46%,var(--surface)),var(--surface))}
.ulg-semantic-verdict .ulg-verdict strong{font:650 16px/1.25 var(--font-display)}
.ulg-semantic-verdict .ulg-verdict span{color:var(--muted);font:500 10px/1.4 var(--font-code);text-transform:uppercase;letter-spacing:.06em}
.ulg-theorem-text{margin:0;padding:13px 14px;border:1px solid var(--line);border-left:3px solid var(--accent);border-radius:9px;background:var(--surface-2);font-size:13px;line-height:1.6;white-space:pre-wrap}
.ulg-theorem-text.repair{border-left-color:var(--purple)}
.ulg-blind-badge{display:inline-flex;margin:0 0 9px;padding:5px 8px;border:1px solid color-mix(in srgb,var(--accent) 36%,var(--line));border-radius:999px;color:var(--accent);background:color-mix(in srgb,var(--accent-soft) 42%,var(--surface));font:600 9px/1 var(--font-code);letter-spacing:.06em;text-transform:uppercase}
.ulg-warning{margin:9px 0 0;color:var(--muted);font-size:11px}
.ulg-semantic-table-wrap{overflow:auto;border:1px solid var(--line);border-radius:10px}
.ulg-semantic-table{width:100%;min-width:720px;border-collapse:collapse;font-size:11px;line-height:1.45}
.ulg-semantic-table th,.ulg-semantic-table td{padding:9px 10px;border-right:1px solid var(--line);border-bottom:1px solid var(--line);vertical-align:top;text-align:left}
.ulg-semantic-table tr:last-child th,.ulg-semantic-table tr:last-child td{border-bottom:0}
.ulg-semantic-table th:last-child,.ulg-semantic-table td:last-child{border-right:0}
.ulg-semantic-table thead th{color:var(--muted);background:var(--surface-2);font:600 8px/1.2 var(--font-code);letter-spacing:.07em;text-transform:uppercase}
.ulg-semantic-table tbody th{min-width:98px;color:var(--ink);background:color-mix(in srgb,var(--surface-2) 45%,var(--surface));font-weight:650}
.ulg-semantic-table td b{display:inline-block;padding:3px 6px;border-radius:999px;color:var(--accent);background:var(--accent-soft);font:600 8px/1.2 var(--font-code);text-transform:uppercase}
.ulg-semantic-table td small{display:block;margin-top:6px;color:var(--muted);line-height:1.45}
.ulg-deltas{display:grid;gap:8px;margin:0;padding:0;list-style:none}
.ulg-deltas li{padding:11px;border:1px solid var(--line);border-left:3px solid var(--yellow);border-radius:9px;background:var(--surface-2)}
.ulg-deltas li[data-severity="blocking"]{border-left-color:var(--red)}
.ulg-deltas li[data-severity="informational"]{border-left-color:var(--green)}
.ulg-deltas li span{display:block;margin-bottom:6px;color:var(--muted);font:600 8px/1.2 var(--font-code);letter-spacing:.06em;text-transform:uppercase}
.ulg-deltas li strong{font-size:12px}.ulg-deltas li p{margin:5px 0 0;color:var(--muted);font-size:11px}
.ulg-repairs{display:grid;gap:10px}
.ulg-repairs article{padding:12px;border:1px solid var(--line);border-radius:10px;background:linear-gradient(120deg,color-mix(in srgb,var(--purple) 7%,var(--surface)),var(--surface))}
.ulg-repairs article header{display:flex;justify-content:space-between;gap:8px;padding:0 0 9px;border-bottom:1px solid var(--line)}
.ulg-repairs article header span,.ulg-repairs article header b{font:600 8px/1.2 var(--font-code);letter-spacing:.06em;text-transform:uppercase}
.ulg-repairs article header span{color:var(--purple)}.ulg-repairs article header b{color:var(--muted)}
.ulg-repairs article>strong{display:block;margin-top:10px;font-size:12px}.ulg-repairs article>p{margin:6px 0;color:var(--muted);font-size:11px}
.ulg-repairs dl{display:grid;gap:5px;margin:9px 0}.ulg-repairs dl div{display:grid;grid-template-columns:76px 1fr;gap:7px}.ulg-repairs dt{color:var(--muted);font:600 8px/1.35 var(--font-code);text-transform:uppercase}.ulg-repairs dd{margin:0;font-size:10px}
.ulg-repairs article>small{display:block;padding-top:8px;border-top:1px solid var(--line);color:var(--red);font:600 8px/1.35 var(--font-code);text-transform:uppercase}

@media(max-width:900px){.ulg-semantics>div:last-child{grid-template-columns:repeat(2,1fr)}}
@media(max-width:650px){.ulg-hero dl div:nth-child(3n){border-right:1px solid var(--line)}.ulg-hero dl div:nth-child(2n){border-right:0}.ulg-hero dl div:nth-last-child(-n+3){border-bottom:1px solid var(--line)}.ulg-hero dl div:nth-last-child(-n+2){border-bottom:0}.ulg-semantics>div:last-child{grid-template-columns:1fr}}