/* Definition-aware PA Proof Explorer. Every selector is microsite-scoped. */

body.pa-defined-proof-site {
  color-scheme: light dark;
  --pd-bg: #f4f0f7;
  --pd-paper: #fffdfd;
  --pd-paper-alt: #f8f4fa;
  --pd-ink: #27212d;
  --pd-muted: #706778;
  --pd-border: #d7ccdd;
  --pd-rule: #aa9db3;
  --pd-link: #365e91;
  --pd-link-visited: #74518a;
  --pd-accent: #713a83;
  --pd-accent-soft: #eee0f3;
  --pd-definition: #783f90;
  --pd-definition-soft: #f0e2f6;
  --pd-public: #176b45;
  --pd-candidate: #8a5a00;
  --pd-code: #f1eaf4;
  --pd-target: #ffeaa1;
  --pd-serif: Georgia, "Times New Roman", serif;
  --pd-sans: ui-sans-serif, system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  --pd-mono: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, "Liberation Mono", monospace;
  --pd-shadow: 0 0.55rem 1.7rem rgba(57, 35, 67, 0.1);
  min-height: 100vh;
  margin: 0;
  background: var(--pd-bg);
  color: var(--pd-ink);
  font-family: var(--pd-serif);
  line-height: 1.6;
}

body.pa-defined-proof-site,
body.pa-defined-proof-site * {
  box-sizing: border-box;
}

body.pa-defined-proof-site a {
  color: var(--pd-link);
  text-decoration-thickness: 0.08em;
  text-underline-offset: 0.15em;
}

body.pa-defined-proof-site a:visited {
  color: var(--pd-link-visited);
}

body.pa-defined-proof-site a:focus-visible,
body.pa-defined-proof-site button:focus-visible,
body.pa-defined-proof-site input:focus-visible,
body.pa-defined-proof-site select:focus-visible,
body.pa-defined-proof-site summary:focus-visible,
body.pa-defined-proof-site [tabindex]:focus-visible {
  outline: 0.2rem solid var(--pd-accent);
  outline-offset: 0.14rem;
}

body.pa-defined-proof-site code,
body.pa-defined-proof-site pre,
body.pa-defined-proof-site .pd-kicker,
body.pa-defined-proof-site .pd-line-number {
  font-family: var(--pd-mono);
}

body.pa-defined-proof-site code {
  overflow-wrap: anywhere;
}

body.pa-defined-proof-site .pd-header {
  padding: clamp(1.2rem, 3vw, 2.4rem);
  border-bottom: 0.3rem solid var(--pd-accent);
  background: var(--pd-paper);
  box-shadow: 0 0.2rem 0.8rem rgba(40, 27, 45, 0.08);
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site .pd-header > * {
  width: min(100%, 92rem);
  margin-right: auto;
  margin-left: auto;
}

body.pa-defined-proof-site .pd-header nav {
  display: flex;
  flex-wrap: wrap;
  gap: 0.45rem 1rem;
  margin-bottom: 1.1rem;
}

body.pa-defined-proof-site .pd-header h1 {
  max-width: 68rem;
  margin-top: 0.15rem;
  margin-bottom: 0.45rem;
  font-family: var(--pd-serif);
  font-size: clamp(2rem, 4vw, 3.6rem);
  line-height: 1.08;
}

body.pa-defined-proof-site .pd-header p {
  max-width: 68rem;
}

body.pa-defined-proof-site .pd-kicker {
  margin-bottom: 0.2rem;
  color: var(--pd-definition);
  font-size: 0.76rem;
  font-weight: 800;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}

body.pa-defined-proof-site .pd-definition-header {
  border-bottom-color: var(--pd-definition);
  background: linear-gradient(125deg, var(--pd-paper), var(--pd-definition-soft));
}

body.pa-defined-proof-site main {
  width: min(calc(100% - 2rem), 92rem);
  margin: 1.4rem auto 3rem;
}

body.pa-defined-proof-site section,
body.pa-defined-proof-site details,
body.pa-defined-proof-site aside {
  border: 1px solid var(--pd-border);
  border-radius: 0.5rem;
  background: var(--pd-paper);
  box-shadow: var(--pd-shadow);
}

body.pa-defined-proof-site section,
body.pa-defined-proof-site aside,
body.pa-defined-proof-site details[open] {
  padding: 1rem 1.15rem;
}

body.pa-defined-proof-site section + section,
body.pa-defined-proof-site section + details,
body.pa-defined-proof-site details + section {
  margin-top: 1rem;
}

body.pa-defined-proof-site h2,
body.pa-defined-proof-site h3,
body.pa-defined-proof-site label,
body.pa-defined-proof-site button,
body.pa-defined-proof-site input,
body.pa-defined-proof-site select,
body.pa-defined-proof-site output,
body.pa-defined-proof-site small,
body.pa-defined-proof-site summary {
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site h2 {
  margin-top: 0;
  font-size: 1.35rem;
}

body.pa-defined-proof-site h3 {
  margin-bottom: 0.45rem;
  font-size: 1rem;
}

body.pa-defined-proof-site pre {
  overflow: auto;
  padding: 0.9rem;
  border: 1px solid var(--pd-border);
  border-radius: 0.34rem;
  background: var(--pd-code);
  white-space: pre-wrap;
}

body.pa-defined-proof-site button,
body.pa-defined-proof-site input,
body.pa-defined-proof-site select {
  min-height: 2.35rem;
  border: 1px solid var(--pd-rule);
  border-radius: 0.32rem;
  background: var(--pd-paper);
  color: var(--pd-ink);
  font: inherit;
}

body.pa-defined-proof-site button {
  padding: 0.42rem 0.8rem;
  cursor: pointer;
}

body.pa-defined-proof-site input,
body.pa-defined-proof-site select {
  padding: 0.38rem 0.55rem;
}

body.pa-defined-proof-site .pd-callout {
  padding: 0.75rem 0.9rem;
  border-left: 0.3rem solid var(--pd-definition);
  background: var(--pd-definition-soft);
  font-family: var(--pd-sans);
  font-size: 0.9rem;
}

body.pa-defined-proof-site .pd-stats {
  display: flex;
  flex-wrap: wrap;
  gap: 0.8rem 1.3rem;
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site .pd-controls,
body.pa-defined-proof-site .pd-graph-controls {
  display: flex;
  flex-wrap: wrap;
  gap: 0.75rem;
  align-items: end;
  margin-bottom: 1rem;
}

body.pa-defined-proof-site .pd-controls label,
body.pa-defined-proof-site .pd-graph-controls label {
  display: grid;
  gap: 0.22rem;
}

body.pa-defined-proof-site .pd-controls label:first-child,
body.pa-defined-proof-site .pd-graph-controls label:first-child {
  flex: 1 1 20rem;
}

body.pa-defined-proof-site .pd-graph-note {
  margin: 0.45rem 0 0.85rem;
  color: var(--pd-muted);
  font-family: var(--pd-sans);
  font-size: 0.82rem;
}

body.pa-defined-proof-site .pd-results {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(min(100%, 22rem), 1fr));
  gap: 0.85rem;
}

body.pa-defined-proof-site .pd-result {
  margin: 0;
  padding: 0.9rem 1rem;
  border-left: 0.3rem solid var(--pd-public);
}

body.pa-defined-proof-site .pd-result-definition {
  border-left-color: var(--pd-definition);
  background: linear-gradient(135deg, var(--pd-paper), var(--pd-definition-soft));
}

body.pa-defined-proof-site .pd-result[hidden] {
  display: none;
}

body.pa-defined-proof-site .pd-result p {
  margin: 0.45rem 0;
}

body.pa-defined-proof-site .pd-result small {
  color: var(--pd-muted);
}

body.pa-defined-proof-site .pd-status {
  display: inline-block;
  width: auto;
  padding: 0.18rem 0.55rem;
  border-radius: 999px;
  background: var(--pd-definition-soft);
  color: var(--pd-accent);
  font-family: var(--pd-sans);
  font-size: 0.78rem;
  font-weight: 750;
}

body.pa-defined-proof-site .pd-status-public {
  color: var(--pd-public);
}

body.pa-defined-proof-site .pd-status-candidate {
  color: var(--pd-candidate);
}

body.pa-defined-proof-site .pd-theorem-layout {
  display: grid;
  grid-template-columns: minmax(0, 1fr) minmax(16rem, 23rem);
  gap: 1.2rem;
  align-items: start;
}

body.pa-defined-proof-site .pd-theorem-layout > aside {
  position: sticky;
  top: 1rem;
}

body.pa-defined-proof-site .pd-definition-page {
  display: grid;
  gap: 1rem;
}

body.pa-defined-proof-site .pd-definition-page > aside {
  border-left: 0.32rem solid var(--pd-definition);
}

body.pa-defined-proof-site dl {
  display: grid;
  grid-template-columns: minmax(8rem, 0.8fr) minmax(0, 1.2fr);
  gap: 0.35rem 0.75rem;
}

body.pa-defined-proof-site dt {
  color: var(--pd-muted);
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site dd {
  margin: 0;
  overflow-wrap: anywhere;
}

body.pa-defined-proof-site .pd-chip-row {
  display: flex;
  flex-wrap: wrap;
  gap: 0.42rem;
}

body.pa-defined-proof-site .pd-chip {
  display: inline-block;
  padding: 0.25rem 0.52rem;
  border: 1px solid var(--pd-border);
  border-radius: 999px;
  background: var(--pd-paper-alt);
  font-family: var(--pd-sans);
  font-size: 0.78rem;
}

body.pa-defined-proof-site .pd-definition-chip,
body.pa-defined-proof-site .pd-definition-ref {
  border-color: color-mix(in srgb, var(--pd-definition) 48%, var(--pd-border));
  background: var(--pd-definition-soft);
  color: var(--pd-definition);
  font-weight: 750;
}

body.pa-defined-proof-site .pd-definition-ref {
  padding: 0.04rem 0.14rem;
  border-bottom: 0.14rem solid currentColor;
  border-radius: 0.2rem;
  text-decoration: none;
}

body.pa-defined-proof-site .pd-empty {
  color: var(--pd-muted);
  font-style: italic;
}

body.pa-defined-proof-site .pd-formal-proof {
  margin: 0;
  padding: 0;
  list-style: none;
  counter-reset: proof-line;
}

body.pa-defined-proof-site .pd-proof-line {
  display: grid;
  grid-template-columns: 4.4rem minmax(0, 1fr);
  gap: 0.7rem;
  padding: 0.28rem 0.45rem;
  border-bottom: 1px solid color-mix(in srgb, var(--pd-border) 55%, transparent);
  scroll-margin-top: 2rem;
}

body.pa-defined-proof-site .pd-proof-line:target,
body.pa-defined-proof-site .pd-proof-line.pd-line-target {
  background: var(--pd-target);
}

body.pa-defined-proof-site .pd-proof-line-defined {
  border-left: 0.22rem solid var(--pd-definition);
  background: color-mix(in srgb, var(--pd-definition-soft) 62%, var(--pd-paper));
}

body.pa-defined-proof-site .pd-defined-command {
  min-width: 0;
  overflow-wrap: anywhere;
}

body.pa-defined-proof-site .pd-exact-line {
  grid-column: 2;
  margin: 0.2rem 0 0.35rem;
  padding: 0.35rem 0.55rem;
  border-left: 0.18rem solid var(--pd-rule);
  color: var(--pd-muted);
  font-size: 0.86rem;
}

body.pa-defined-proof-site .pd-exact-line summary {
  cursor: pointer;
  color: var(--pd-accent);
  font-weight: 700;
}

body.pa-defined-proof-site .pd-exact-line code {
  display: block;
  margin-top: 0.38rem;
  color: var(--pd-ink);
  overflow-wrap: anywhere;
}

body.pa-defined-proof-site .pd-line-number {
  color: var(--pd-muted);
  font-size: 0.78rem;
  text-decoration: none;
}

body.pa-defined-proof-site .pd-tactic-ref {
  color: var(--pd-accent);
  font-weight: 750;
}

body.pa-defined-proof-site .pd-graph-layout {
  display: grid;
  grid-template-columns: minmax(0, 1fr) minmax(17rem, 24rem);
  gap: 1rem;
  align-items: start;
}

body.pa-defined-proof-site .pd-graph-toolbar {
  display: flex;
  justify-content: space-between;
  gap: 0.7rem;
  align-items: center;
  padding: 0.7rem;
  border: 1px solid var(--pd-border);
  border-bottom: 0;
  background: var(--pd-paper);
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site .pd-graph-toolbar > div {
  display: flex;
  gap: 0.35rem;
}

body.pa-defined-proof-site .pd-graph-stage {
  height: clamp(30rem, 66vh, 48rem);
  overflow: hidden;
  border: 1px solid var(--pd-border);
  background-color: var(--pd-paper-alt);
  background-image:
    linear-gradient(color-mix(in srgb, var(--pd-border) 35%, transparent) 1px, transparent 1px),
    linear-gradient(90deg, color-mix(in srgb, var(--pd-border) 35%, transparent) 1px, transparent 1px);
  background-size: 1.2rem 1.2rem;
}

body.pa-defined-proof-site .pd-graph-stage svg {
  display: block;
  width: 100%;
  height: 100%;
  cursor: grab;
  touch-action: none;
  user-select: none;
}

body.pa-defined-proof-site .pd-graph-stage.pd-panning svg {
  cursor: grabbing;
}

body.pa-defined-proof-site .pd-graph-details {
  position: sticky;
  top: 1rem;
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site .pd-graph-details ul {
  padding-left: 1.2rem;
}

body.pa-defined-proof-site .pd-graph-layer-label {
  fill: var(--pd-muted);
  font-family: var(--pd-sans);
  font-size: 11px;
  font-weight: 750;
  letter-spacing: 0.05em;
  text-transform: uppercase;
}

body.pa-defined-proof-site .pd-graph-edge {
  fill: none;
  stroke: var(--pd-rule);
  stroke-width: 1.6;
  vector-effect: non-scaling-stroke;
}

body.pa-defined-proof-site .pd-graph-edge-proof-path {
  stroke: var(--pd-accent);
  stroke-width: 3;
}

body.pa-defined-proof-site .pd-graph-edge-declared {
  stroke-dasharray: 7 5;
}

body.pa-defined-proof-site .pd-graph-edge-notation {
  stroke: var(--pd-definition);
  stroke-width: 1.8;
  stroke-dasharray: 3 4;
}

body.pa-defined-proof-site #pd-proof-arrow path {
  fill: var(--pd-rule);
}

body.pa-defined-proof-site #pd-notation-arrow path {
  fill: var(--pd-definition);
}

body.pa-defined-proof-site .pd-graph-node {
  cursor: pointer;
  font-family: var(--pd-sans);
}

body.pa-defined-proof-site .pd-graph-node > rect,
body.pa-defined-proof-site .pd-graph-node > polygon {
  fill: var(--pd-paper);
  stroke: var(--pd-rule);
  stroke-width: 1.6;
  vector-effect: non-scaling-stroke;
}

body.pa-defined-proof-site .pd-graph-node-theorem.pd-scope-public > rect {
  stroke: var(--pd-public);
}

body.pa-defined-proof-site .pd-graph-node-theorem.pd-scope-candidate > rect {
  stroke: var(--pd-candidate);
}

body.pa-defined-proof-site .pd-graph-node-definition > polygon {
  fill: var(--pd-definition-soft);
  stroke: var(--pd-definition);
  stroke-width: 2.2;
}

body.pa-defined-proof-site .pd-graph-node-path > rect {
  stroke: var(--pd-accent);
  stroke-width: 2.8;
}

body.pa-defined-proof-site .pd-graph-node-selected > rect,
body.pa-defined-proof-site .pd-graph-node-selected > polygon {
  fill: var(--pd-target);
  stroke: var(--pd-accent);
  stroke-width: 4;
}

body.pa-defined-proof-site .pd-graph-node:hover > rect,
body.pa-defined-proof-site .pd-graph-node:hover > polygon,
body.pa-defined-proof-site .pd-graph-node:focus > rect,
body.pa-defined-proof-site .pd-graph-node:focus > polygon {
  filter: drop-shadow(0 3px 5px rgba(54, 28, 62, 0.2));
  stroke-width: 3.4;
}

body.pa-defined-proof-site .pd-graph-node:focus {
  outline: none;
}

body.pa-defined-proof-site .pd-node-id {
  fill: var(--pd-ink);
  font-family: var(--pd-mono);
  font-size: 12px;
  font-weight: 800;
}

body.pa-defined-proof-site .pd-graph-node-compact .pd-node-id {
  font-size: 8px;
  letter-spacing: 0.04em;
}

body.pa-defined-proof-site .pd-node-name {
  fill: var(--pd-muted);
  font-size: 10px;
  font-weight: 600;
}

body.pa-defined-proof-site .pd-node-open {
  fill: var(--pd-link);
  font-size: 17px;
  font-weight: 800;
}

body.pa-defined-proof-site .pd-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 0.55rem 1rem;
  margin-top: 0.65rem;
  color: var(--pd-muted);
  font-family: var(--pd-sans);
  font-size: 0.75rem;
}

body.pa-defined-proof-site .pd-legend span {
  display: inline-flex;
  gap: 0.35rem;
  align-items: center;
}

body.pa-defined-proof-site .pd-legend i {
  display: inline-block;
  width: 1.25rem;
  height: 0.82rem;
}

body.pa-defined-proof-site .pd-legend-theorem {
  border: 2px solid var(--pd-public);
  border-radius: 0.18rem;
  background: var(--pd-paper);
}

body.pa-defined-proof-site .pd-legend-definition {
  clip-path: polygon(18% 0, 82% 0, 100% 50%, 82% 100%, 18% 100%, 0 50%);
  border: 0;
  background: var(--pd-definition);
}

body.pa-defined-proof-site .pd-legend-proof,
body.pa-defined-proof-site .pd-legend-notation {
  height: 0;
  border-top: 2px solid var(--pd-rule);
}

body.pa-defined-proof-site .pd-legend-notation {
  border-top: 2px dashed var(--pd-definition);
}

@media (max-width: 880px) {
  body.pa-defined-proof-site .pd-theorem-layout,
  body.pa-defined-proof-site .pd-graph-layout {
    grid-template-columns: 1fr;
  }

  body.pa-defined-proof-site .pd-theorem-layout > aside,
  body.pa-defined-proof-site .pd-graph-details {
    position: static;
  }
}

@media (prefers-reduced-motion: reduce) {
  body.pa-defined-proof-site {
    scroll-behavior: auto;
  }
}

@media print {
  body.pa-defined-proof-site {
    background: white;
    color: black;
  }

  body.pa-defined-proof-site .pd-controls,
  body.pa-defined-proof-site .pd-graph-controls,
  body.pa-defined-proof-site .pd-graph-toolbar,
  body.pa-defined-proof-site button {
    display: none;
  }

  body.pa-defined-proof-site section,
  body.pa-defined-proof-site details,
  body.pa-defined-proof-site aside {
    box-shadow: none;
  }
}