/* Lean-Blueprint Design Language (PlasTeX / Lean 4 Community Aesthetic)
   Faithfully replicating the look and feel of Lean 4 project blueprints.
*/
:root {
  /* Lean-Blueprint Brand & Layout Colors */
  --bp-header: #1E293B;       /* Deep academic slate navbar */
  --bp-header-text: #F8FAFC;
  --bp-header-sub: #94A3B8;
  --bp-header-accent: #3B82F6;
  
  /* Lean-Blueprint Status Palettes */
  --green: #2E7D32;           /* Proved in Lean 4 */
  --green-d: #1B5E20;
  --green-bg: #E6F4EA;
  --green-border: #81C784;
  --card: #F4FBF6;
  --card-b: #81C784;
  --ink: #0F172A;
  --sub: #475569;
  --edge: #64748B;
  
  --blue: #0288D1;            /* Stated / Ready to prove */
  --blue-d: #01579B;
  --blue-bg: #E1F5FE;
  --blue-border: #4FC3F7;
  
  --violet: #7C3AED;          /* Definitions */
  --violet-bg: #F3E8FF;
  --violet-border: #C4B5FD;
  
  --amber: #D97706;           /* Axioms & Postulates */
  --amber-bg: #FEF3C7;
  --amber-border: #FCD34D;
  
  --bg: #F8FAFC;              /* Clean blueprint canvas */
  --rule: #E2E8F0;
  --warn: #B45309;
  
  /* Academic Latin Modern & Sans Typography */
  --mono: "JetBrains Mono", "SFMono-Regular", Menlo, Monaco, Consolas, monospace;
  --sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
  --serif: "Latin Modern Roman", "Computer Modern", Georgia, "Times New Roman", serif;
}

* { box-sizing: border-box; }
html { font-size: 16px; }
body {
  margin: 0;
  font-family: var(--sans);
  color: #1E293B;
  background: var(--bg);
  line-height: 1.6;
  -webkit-font-smoothing: antialiased;
}

a { color: var(--green); text-decoration: none; }
a:hover { text-decoration: underline; color: var(--green-d); }

code, pre { font-family: var(--mono); font-size: 0.86rem; }
code {
  background: #F1F5F9;
  color: #0F172A;
  padding: 0.15em 0.35em;
  border-radius: 4px;
  word-break: break-word;
  border: 1px solid #E2E8F0;
}
a code { color: inherit; }

pre {
  background: #0F172A;
  color: #F8FAFC;
  border: 1px solid #334155;
  border-radius: 6px;
  padding: 0.8rem 1rem;
  overflow-x: auto;
  line-height: 1.45;
  white-space: pre-wrap;
  word-break: break-word;
}
pre code { background: none; padding: 0; border: none; color: inherit; }

h1 {
  font-family: var(--serif);
  font-weight: 700;
  font-size: 2.1rem;
  margin: 0.4em 0 0.3em;
  color: #0F172A;
  letter-spacing: -0.01em;
}
h2 {
  font-family: var(--serif);
  font-size: 1.35rem;
  margin: 1.8em 0 0.6em;
  color: #0F172A;
  border-bottom: 1px solid var(--rule);
  padding-bottom: 0.3em;
  font-weight: 600;
}
h3 {
  font-family: var(--serif);
  font-size: 1.1rem;
  margin: 1.3em 0 0.4em;
  color: #1E293B;
  font-weight: 600;
}

.small { font-size: 0.85em; }
.muted { color: var(--sub); }
.warn { color: var(--warn); }

/* Lean-Blueprint Academic Header */
header.top {
  background: var(--bp-header);
  border-bottom: 2px solid #334155;
  color: var(--bp-header-text);
  position: sticky;
  top: 0;
  z-index: 50;
  box-shadow: 0 2px 10px rgba(0,0,0,0.18);
}
header.top .inner {
  max-width: 1440px;
  margin: 0 auto;
  padding: 0.6rem 1.5rem;
  display: flex;
  align-items: center;
  gap: 1.2rem;
  flex-wrap: wrap;
}
header.top .brand {
  font-family: var(--serif);
  font-size: 1.22rem;
  color: #FFFFFF;
  text-decoration: none;
  white-space: nowrap;
  display: flex;
  align-items: center;
  gap: 0.5rem;
}
header.top .brand b {
  color: #FFFFFF;
  font-weight: 700;
}
header.top .brand .bp-badge {
  background: #2563EB;
  color: #FFFFFF;
  font-family: var(--sans);
  font-size: 0.68rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.06em;
  padding: 0.15rem 0.45rem;
  border-radius: 4px;
}
header.top nav {
  display: flex;
  align-items: center;
  gap: 0.3rem;
  flex-wrap: wrap;
}
header.top nav a {
  color: var(--bp-header-sub);
  font-size: 0.90rem;
  font-weight: 500;
  padding: 0.35rem 0.7rem;
  border-radius: 5px;
  transition: all 0.15s ease;
  text-decoration: none;
}
header.top nav a:hover {
  color: #FFFFFF;
  background: rgba(255,255,255,0.08);
  text-decoration: none;
}
header.top nav a.cur {
  color: #FFFFFF;
  background: rgba(59,130,246,0.22);
  border: 1px solid rgba(59,130,246,0.45);
  font-weight: 600;
}

/* Search Bar in Blueprint Style */
.search { position: relative; flex: 1; min-width: 250px; }
.search input {
  width: 100%;
  padding: 0.42rem 0.8rem;
  background: #0F172A;
  color: #F8FAFC;
  border: 1px solid #475569;
  border-radius: 6px;
  font-size: 0.90rem;
  font-family: var(--mono);
  transition: all 0.15s ease;
}
.search input::placeholder { color: #64748B; }
.search input:focus {
  outline: none;
  border-color: #38BDF8;
  box-shadow: 0 0 0 2px rgba(56,189,248,0.25);
  background: #1E293B;
}
#q-results {
  display: none;
  position: absolute;
  top: 108%;
  left: 0;
  right: 0;
  background: #FFFFFF;
  border: 1px solid #CBD5E1;
  border-radius: 6px;
  max-height: 70vh;
  overflow: auto;
  box-shadow: 0 10px 30px rgba(0,0,0,0.14);
  z-index: 60;
}
a.sr { display: block; padding: 0.5rem 0.8rem; border-bottom: 1px solid #F1F5F9; color: #1E293B; text-decoration: none; }
a.sr:hover, a.sr.active { background: #F8FAFC; text-decoration: none; }
a.sr code { display: block; background: none; border: none; font-size: 0.78rem; color: #64748B; margin-top: 0.15rem; }
.sr-kind {
  display: inline-block;
  font-size: 0.68rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.05em;
  color: #FFFFFF;
  background: var(--green);
  border-radius: 3px;
  padding: 0.1em 0.4em;
  margin-right: 0.4em;
}
.sr-kind.def { background: var(--violet); }
.sr-title { font-size: 0.90rem; font-weight: 600; color: #0F172A; }
.sr-num { font-size: 0.75rem; color: var(--sub); }
.sr-empty, .sr-more { padding: 0.6rem 0.8rem; color: var(--sub); font-size: 0.85rem; }

main { max-width: 1440px; margin: 0 auto; padding: 1.2rem 1.5rem 4rem; }
main.prose { max-width: 960px; }
.prose p, .prose li { font-family: var(--serif); font-size: 1.06rem; line-height: 1.7; color: #1E293B; }
.prose table { border-collapse: collapse; font-size: 0.92rem; margin: 1.2em 0; width: 100%; }
.prose th, .prose td { border: 1px solid var(--rule); padding: 0.5em 0.8em; vertical-align: top; text-align: left; }
.prose th { background: #F8FAFC; font-family: var(--serif); font-weight: 600; }
.prose blockquote {
  border-left: 3.5px solid var(--green);
  margin: 1.2em 0;
  padding: 0.4em 1.2em;
  color: #1E293B;
  background: #FAFDFB;
  font-family: var(--serif);
  font-style: italic;
}

/* Lean-Blueprint Badges */
.badge {
  display: inline-block;
  font-size: 0.73rem;
  font-weight: 600;
  border-radius: 12px;
  padding: 0.12em 0.65em;
  margin-right: 0.35em;
  vertical-align: middle;
  white-space: nowrap;
  border: 1px solid transparent;
}
.badge.proved {
  background: var(--green-bg);
  border-color: var(--green);
  color: var(--green-d);
}
.badge.ready {
  background: var(--blue-bg);
  border-color: var(--blue);
  color: var(--blue-d);
}
.badge.def {
  background: var(--violet-bg);
  border-color: var(--violet);
  color: #581C87;
}
.badge.postulate {
  background: var(--amber-bg);
  border-color: var(--amber);
  color: #92400E;
}
.badge.lm {
  background: var(--green-d);
  border-color: var(--green-d);
  color: #FFFFFF;
}
.badge.root {
  background: #0F172A;
  border-color: #0F172A;
  color: #FFFFFF;
}
.badge.stage {
  background: #FFFFFF;
  border-color: #CBD5E1;
  color: #475569;
}
.badge.dup {
  background: #FEF3C7;
  border-color: #F59E0B;
  color: #92400E;
}

/* Navigation Breadcrumbs */
.breadcrumbs {
  font-size: 0.85rem;
  color: #64748B;
  margin-bottom: 0.4rem;
  font-family: var(--sans);
}
.breadcrumbs a { color: #2563EB; }
.breadcrumbs a:hover { text-decoration: underline; }

/* PlasTeX / Lean-Blueprint Vertical Rule Theorem Environments */
.theorem-box, div.theorem_thmcontent, div.proposition_thmcontent, .en {
  background: #FFFFFF;
  border: 1px solid #E2E8F0;
  border-left: 4.5px solid var(--green);
  border-radius: 0 8px 8px 0;
  padding: 1.1rem 1.4rem;
  margin-bottom: 1.3rem;
  box-shadow: 0 1px 4px rgba(0,0,0,0.04);
  font-family: var(--serif);
  font-size: 1.05rem;
  line-height: 1.65;
}
div.lemma_thmcontent, div.corollary_thmcontent {
  background: #FFFFFF;
  border: 1px solid #E2E8F0;
  border-left: 3.5px solid var(--green);
  border-radius: 0 8px 8px 0;
  padding: 1rem 1.3rem;
  margin-bottom: 1.2rem;
  font-family: var(--serif);
  font-size: 1.03rem;
}
div.definition_thmcontent {
  background: #FCFBFD;
  border: 1px solid #E2E8F0;
  border-left: 3.5px dashed var(--violet);
  border-radius: 0 8px 8px 0;
  padding: 1rem 1.3rem;
  margin-bottom: 1.2rem;
  font-family: var(--serif);
  font-size: 1.03rem;
}
div.proof_content {
  border-left: 2.5px solid #94A3B8;
  background: #F8FAFC;
  padding: 0.9rem 1.2rem;
  margin-top: 0.8rem;
  border-radius: 0 6px 6px 0;
  font-family: var(--serif);
  font-size: 0.98rem;
  line-height: 1.6;
}

/* Theorem Environment Headings */
.thm-env-header {
  display: flex;
  justify-content: space-between;
  align-items: baseline;
  flex-wrap: wrap;
  gap: 0.6rem;
  margin-bottom: 0.8rem;
  border-bottom: 1px solid #F1F5F9;
  padding-bottom: 0.4rem;
}
.thm-title-main {
  font-family: var(--serif);
  font-size: 1.28rem;
  font-weight: 700;
  color: #0F172A;
}
.thm-title-informal {
  font-style: italic;
  font-weight: normal;
  color: #334155;
  margin-left: 0.35rem;
}
.lean-decl-pill {
  font-family: var(--mono);
  font-size: 0.78rem;
  background: #EFF6FF;
  border: 1px solid #BFDBFE;
  color: #1E40AF;
  padding: 0.22rem 0.65rem;
  border-radius: 14px;
  text-decoration: none;
  display: inline-flex;
  align-items: center;
  gap: 0.3rem;
  font-weight: 500;
}
.lean-decl-pill:hover {
  background: #DBEAFE;
  text-decoration: none;
  border-color: #93C5FD;
}

/* Lean Code Pre / Blocks */
pre.lean {
  background: #0F172A;
  border: 1px solid #334155;
  color: #F8FAFC;
  border-radius: 6px;
  padding: 0.8rem 1rem;
}
pre.lean.stmt {
  border-left: 4px solid #2563EB;
  font-size: 0.88rem;
}

/* Buttons */
.btn {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 0.35rem;
  padding: 0.42rem 0.85rem;
  font-size: 0.88rem;
  font-weight: 500;
  border-radius: 6px;
  border: 1px solid #CBD5E1;
  background: #FFFFFF;
  color: #1E293B;
  cursor: pointer;
  text-decoration: none;
  transition: all 0.15s ease;
  line-height: 1.4;
}
.btn:hover {
  background: #F8FAFC;
  border-color: #94A3B8;
  color: #0F172A;
  text-decoration: none;
}
.btn.small {
  padding: 0.25rem 0.55rem;
  font-size: 0.78rem;
}
.btn.alt {
  background: #F1F5F9;
  border-color: #E2E8F0;
  color: #334155;
}
.btn.alt:hover {
  background: #E2E8F0;
  color: #0F172A;
}
.btn.trace-btn {
  background: var(--green);
  color: #FFFFFF;
  font-weight: 600;
  border-color: var(--green-d);
}
.btn.trace-btn:hover {
  background: var(--green-d);
  box-shadow: 0 2px 6px rgba(46,125,50,0.3);
  color: #FFFFFF;
}

/* Perspective Switcher & Orbit Guides */
.view-switch-group {
  display: inline-flex;
  background: #E2E8F0;
  border-radius: 6px;
  padding: 3px;
  gap: 3px;
}
.view-btn {
  background: transparent;
  border: none;
  padding: 0.42rem 0.95rem;
  font-size: 0.84rem;
  font-weight: 600;
  color: #475569;
  border-radius: 5px;
  cursor: pointer;
  transition: all 0.15s ease;
}
.view-btn:hover { color: #0F172A; }
.view-btn.active {
  background: #FFFFFF;
  color: #0F172A;
  box-shadow: 0 1px 4px rgba(0,0,0,0.12);
}
.view-btn.active#btn-mode-axiom {
  background: #FEF3C7;
  color: #92400E;
  box-shadow: 0 1px 4px rgba(245,158,11,0.25);
}

/* Theorem Inspector Cards */
.insp-card {
  background: #FFFFFF;
  border: 1px solid #E2E8F0;
  border-radius: 8px;
  overflow: hidden;
  box-shadow: 0 1px 4px rgba(0,0,0,0.05);
}
.insp-head {
  padding: 1rem 1.2rem;
  border-bottom: 1px solid #E2E8F0;
  background: #FAFDFB;
}
.insp-body {
  padding: 1rem 1.2rem;
  font-size: 0.88rem;
}

/* Metric / Numbers list */
ul.kv {
  list-style: none;
  padding: 0;
  margin: 0;
  display: flex;
  flex-direction: column;
  gap: 0.45rem;
}
ul.kv li {
  font-size: 0.88rem;
  color: #334155;
  border-bottom: 1px dashed #F1F5F9;
  padding-bottom: 0.35rem;
}
ul.kv li:last-child { border-bottom: none; }

/* Reduction Timeline */
.reduction-timeline {
  background: #F8FAFC;
  border: 1px solid #E2E8F0;
  border-radius: 6px;
  padding: 1.1rem;
}
.reduction-timeline ol {
  margin: 0.6rem 0 0 1.2rem;
  padding: 0;
  font-size: 0.86rem;
  line-height: 1.6;
}
.reduction-timeline li { margin-bottom: 0.4rem; color: #334155; }

/* Graph Tools Bar */
.graph-tools {
  background: #F8FAFC;
  border: 1px solid #E2E8F0;
  padding: 0.6rem 1rem;
  display: flex;
  align-items: center;
  flex-wrap: wrap;
  gap: 0.6rem;
}

/* Footer */
footer {
  border-top: 1px solid var(--rule);
  padding: 2rem 1.5rem;
  text-align: center;
  font-size: 0.86rem;
  color: #64748B;
  background: #FFFFFF;
  font-family: var(--serif);
}

/* Corpus Switcher for Multi-Book Platform */
.corpus-switcher {
  display: inline-flex;
  align-items: center;
  gap: 0.4rem;
  margin-left: auto;
}
.corpus-select {
  background: #0F172A;
  color: #F8FAFC;
  border: 1px solid #475569;
  border-radius: 6px;
  padding: 0.38rem 0.75rem;
  font-size: 0.84rem;
  font-family: var(--sans);
  font-weight: 500;
  cursor: pointer;
  transition: all 0.15s ease;
}
.corpus-select:focus {
  outline: none;
  border-color: #38BDF8;
  box-shadow: 0 0 0 2px rgba(56,189,248,0.25);
}