* {
  margin: 0;
  padding: 0;
  box-sizing: border-box;
}

:root {
  --bg-dark: #1a1625;
  --bg-card: #2a2438;
  --bg-hover: #3a3448;
  --accent: #8b7dd8;
  --accent-bright: #a394e8;
  --text-main: #e8e4f3;
  --text-dim: #b8b4c8;
  --text-bright: #ffffff;
  --border: #3a3448;
  --success: #6dd47e;
  --code-bg: #1a1625;
  --code-border: #4a4458;
}

body {
  font-family: 'Segoe UI', system-ui, -apple-system, sans-serif;
  background: var(--bg-dark);
  color: var(--text-main);
  line-height: 1.7;
  min-height: 100vh;
  display: flex;
  flex-direction: column;
}

.container {
  max-width: 1100px;
  margin: 0 auto;
  padding: 0 20px;
}

/* ===== HEADER ===== */
header {
  background: linear-gradient(135deg, #2a2438 0%, #1a1625 100%);
  padding: 3rem 0 2.5rem;
  border-bottom: 2px solid var(--border);
  text-align: center;
}

.header-title {
  display: flex;
  align-items: center;
  justify-content: center;
  gap: 1rem;
  margin-bottom: 0.5rem;
}

.logo {
  filter: drop-shadow(0 2px 8px rgba(139, 125, 216, 0.3));
  animation: logoFloat 3s ease-in-out infinite;
}

@keyframes logoFloat {
  0%, 100% { transform: translateY(0px); }
  50% { transform: translateY(-5px); }
}

header h1 {
  font-size: 2.8rem;
  font-weight: 700;
  color: var(--text-bright);
  letter-spacing: -0.5px;
}

.tagline {
  font-size: 1.3rem;
  color: var(--accent-bright);
  font-weight: 400;
  margin-bottom: 0.8rem;
}

.stats {
  font-size: 0.95rem;
  color: var(--text-dim);
  font-weight: 400;
}

.stats strong {
  color: var(--success);
  font-weight: 600;
}

/* ===== BREADCRUMBS ===== */
.breadcrumbs {
  display: flex;
  align-items: center;
  gap: 0.5rem;
  padding: 1rem 0;
  font-size: 0.9rem;
  color: var(--text-dim);
  flex-wrap: wrap;
}

.breadcrumbs a,
.breadcrumbs span {
  color: var(--text-dim);
  text-decoration: none;
  transition: color 0.2s;
}

.breadcrumbs a:hover {
  color: var(--accent-bright);
}

.breadcrumbs .current {
  color: var(--text-main);
  font-weight: 600;
}

.breadcrumbs .separator {
  color: var(--border);
  user-select: none;
}

/* ===== PAGE TRANSITIONS ===== */
.page-transition {
  animation: fadeIn 0.3s ease-in-out;
}

@keyframes fadeIn {
  from {
    opacity: 0;
    transform: translateY(10px);
  }
  to {
    opacity: 1;
    transform: translateY(0);
  }
}

/* ===== LOADING SKELETON ===== */
.loading-skeleton {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(300px, 1fr));
  gap: 1.5rem;
  margin: 2rem 0;
}

.skeleton-card {
  background: linear-gradient(
    90deg,
    var(--bg-card) 0%,
    var(--bg-hover) 50%,
    var(--bg-card) 100%
  );
  background-size: 200% 100%;
  animation: shimmer 1.5s infinite;
  border-radius: 12px;
  height: 200px;
}

@keyframes shimmer {
  0% { background-position: -200% 0; }
  100% { background-position: 200% 0; }
}

/* ===== MAIN CONTENT ===== */
main {
  flex: 1;
  padding: 2.5rem 0;
}

/* ===== SEARCH SECTION ===== */
.search-section {
  margin-bottom: 3rem;
}

.search-container {
  display: flex;
  gap: 0.75rem;
  max-width: 800px;
  margin: 0 auto;
  flex-wrap: wrap;
}

#search-input {
  flex: 1;
  min-width: 250px;
  padding: 0.85rem 1.2rem;
  font-size: 1rem;
  background: var(--bg-card);
  border: 2px solid var(--border);
  border-radius: 8px;
  color: var(--text-main);
  transition: all 0.2s;
}

#search-input:focus {
  outline: none;
  border-color: var(--accent);
  background: var(--bg-hover);
}

#search-input::placeholder {
  color: var(--text-dim);
}

#search-btn,
.random-btn {
  padding: 0.85rem 1.8rem;
  font-size: 1rem;
  font-weight: 600;
  background: var(--accent);
  color: var(--text-bright);
  border: none;
  border-radius: 8px;
  cursor: pointer;
  transition: all 0.2s;
}

#search-btn:hover,
.random-btn:hover {
  background: var(--accent-bright);
  transform: translateY(-1px);
}

.random-btn {
  background: linear-gradient(135deg, #6a5acd 0%, #8b7dd8 100%);
}

.search-results {
  max-width: 800px;
  margin: 1.5rem auto 0;
  background: var(--bg-card);
  border-radius: 10px;
  padding: 1.5rem;
  border: 1px solid var(--border);
}

.search-results.hidden {
  display: none;
}

.search-results h3 {
  font-size: 1.2rem;
  margin-bottom: 1rem;
  color: var(--accent-bright);
}

.search-results ul {
  list-style: none;
}

.search-results li {
  padding: 0.75rem;
  margin-bottom: 0.5rem;
  background: var(--bg-dark);
  border-radius: 6px;
  cursor: pointer;
  transition: all 0.2s;
  border: 1px solid var(--border);
}

.search-results li:hover,
.search-results li.selected {
  background: var(--bg-hover);
  border-color: var(--accent);
  transform: translateX(4px);
}

.search-results .theorem-name {
  font-weight: 600;
  color: var(--accent-bright);
  font-size: 1rem;
}

.search-results .theorem-snippet {
  font-size: 0.9rem;
  color: var(--text-dim);
  margin-top: 0.3rem;
}

.search-results .curated-badge {
  display: inline-block;
  background: var(--accent);
  color: var(--text-bright);
  padding: 0.15rem 0.5rem;
  border-radius: 4px;
  font-size: 0.75rem;
  font-weight: 600;
  margin-left: 0.5rem;
}

/* ===== HEADER TOP LAYOUT ===== */
.header-top {
  display: flex;
  justify-content: space-between;
  align-items: flex-start;
  gap: 2rem;
}

.header-left {
  flex: 1;
}

/* ===== THEOREM OF THE DAY ===== */
.theorem-of-day {
  flex: 0 0 340px;
  background: linear-gradient(135deg, rgba(139, 125, 216, 0.1) 0%, rgba(163, 148, 232, 0.05) 100%);
  border: 2px solid var(--accent);
  border-radius: 12px;
  padding: 1.5rem;
  cursor: pointer;
  transition: all 0.3s;
}

.theorem-of-day:hover {
  border-color: var(--accent-bright);
  transform: translateY(-2px);
  box-shadow: 0 8px 24px rgba(139, 125, 216, 0.2);
}

.theorem-of-day .badge {
  display: inline-block;
  background: var(--accent);
  color: var(--text-bright);
  padding: 0.25rem 0.6rem;
  border-radius: 6px;
  font-size: 0.8rem;
  font-weight: 600;
  margin-bottom: 0.8rem;
}

.theorem-of-day h3 {
  font-size: 1.1rem;
  color: var(--accent-bright);
  margin-bottom: 0.5rem;
  word-break: break-word;
}

.theorem-of-day .description {
  font-size: 0.9rem;
  color: var(--text-dim);
  line-height: 1.6;
}

/* ===== CATEGORIES GRID ===== */
.home-view h2 {
  font-size: 1.8rem;
  margin-bottom: 1.5rem;
  color: var(--text-bright);
  text-align: center;
}

.categories-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(280px, 1fr));
  gap: 1.5rem;
}

.category-card {
  background: var(--bg-card);
  border: 2px solid var(--border);
  border-radius: 12px;
  padding: 2rem;
  cursor: pointer;
  transition: all 0.3s;
  text-align: center;
}

.category-card:hover {
  border-color: var(--accent);
  transform: translateY(-4px);
  box-shadow: 0 8px 20px rgba(139, 125, 216, 0.2);
}

.category-icon {
  font-size: 1.8rem;
  font-family: 'JetBrains Mono', 'Fira Code', 'Source Code Pro', monospace;
  color: var(--accent-bright);
  background: rgba(139, 125, 216, 0.1);
  padding: 0.5rem 0.8rem;
  border-radius: 8px;
  margin-bottom: 0.8rem;
  display: inline-block;
  letter-spacing: -0.02em;
}

.category-card h3 {
  font-size: 1.4rem;
  color: var(--accent-bright);
  margin-bottom: 0.6rem;
}

.category-description {
  font-size: 0.95rem;
  color: var(--text-dim);
  line-height: 1.6;
}

.category-count {
  margin-top: 0.8rem;
  font-size: 0.85rem;
  color: var(--success);
  font-weight: 600;
}

/* ===== CATEGORY VIEW ===== */
.category-view h2,
.theorem-view h2 {
  font-size: 2rem;
  color: var(--text-bright);
  margin-bottom: 1.5rem;
}

.theorems-list {
  list-style: none;
}

.theorems-list li {
  background: var(--bg-card);
  padding: 1.2rem;
  margin-bottom: 1rem;
  border-radius: 10px;
  cursor: pointer;
  border: 2px solid var(--border);
  transition: all 0.2s;
}

.theorems-list li:hover {
  border-color: var(--accent);
  background: var(--bg-hover);
  transform: translateX(6px);
}

.theorem-name {
  font-size: 1.1rem;
  font-weight: 600;
  color: var(--accent-bright);
}

/* ===== THEOREM DETAIL ===== */
.theorem-actions {
  display: flex;
  justify-content: flex-end;
  margin-bottom: 1rem;
}

.share-btn {
  background: var(--bg-card);
  border: 2px solid var(--border);
  color: var(--text-main);
  padding: 0.6rem 1.2rem;
  border-radius: 8px;
  cursor: pointer;
  font-size: 0.9rem;
  font-weight: 600;
  transition: all 0.2s;
}

.share-btn:hover {
  border-color: var(--accent);
  background: var(--bg-hover);
  color: var(--accent-bright);
}

.share-btn.copied {
  background: var(--success);
  border-color: var(--success);
  color: var(--text-bright);
}

#theorem-detail {
  background: var(--bg-card);
  padding: 2.5rem;
  border-radius: 12px;
  border: 2px solid var(--border);
}

#theorem-detail h2 {
  font-size: 1.8rem;
  color: var(--text-bright);
  margin-bottom: 0.5rem;
}

#theorem-detail .theorem-metadata {
  color: var(--text-dim);
  font-size: 0.9rem;
  margin-bottom: 2rem;
  padding-bottom: 1.5rem;
  border-bottom: 1px solid var(--border);
}

#theorem-detail .section-title {
  font-size: 1.3rem;
  color: var(--accent-bright);
  margin-top: 2rem;
  margin-bottom: 1rem;
  font-weight: 600;
}

#theorem-detail .description,
#theorem-detail .why-matters,
#theorem-detail .intuition {
  font-size: 1.05rem;
  line-height: 1.8;
  color: var(--text-main);
  margin-bottom: 1.5rem;
}

#theorem-detail .formal-statement {
  background: var(--code-bg);
  padding: 1.5rem;
  border-radius: 8px;
  border: 2px solid var(--code-border);
  overflow-x: auto;
  margin: 1.5rem 0;
}

#theorem-detail .formal-statement pre {
  margin: 0;
  font-family: 'Fira Code', 'Consolas', monospace;
  font-size: 0.95rem;
  color: #e0def4;
  line-height: 1.6;
}

/* Lean signature block */
.lean-signature-block {
  background: #1a1a2e;
  padding: 1.5rem;
  border-radius: 10px;
  border-left: 4px solid var(--accent);
  margin: 1.5rem 0;
  overflow-x: auto;
}

.lean-signature-block pre {
  margin: 0;
  font-family: 'JetBrains Mono', 'Fira Code', 'Source Code Pro', monospace;
  font-size: 0.9rem;
  color: #e0def4;
  line-height: 1.7;
  white-space: pre-wrap;
  word-break: break-word;
}

.lean-signature-block code {
  font-family: inherit;
  background: none;
  padding: 0;
}

/* Condensed signature in lists */
.condensed-signature {
  font-family: 'JetBrains Mono', 'Fira Code', 'Source Code Pro', monospace;
  font-size: 0.8rem;
  color: var(--accent-bright);
  background: rgba(139, 125, 216, 0.1);
  padding: 0.4rem 0.6rem;
  border-radius: 6px;
  margin: 0.5rem 0;
  border-left: 3px solid var(--accent);
  overflow-x: auto;
  white-space: nowrap;
}

#theorem-detail .lean-keyword {
  color: #9ccfd8;
  font-weight: 600;
}

#theorem-detail .lean-type {
  color: #f6c177;
}

#theorem-detail .lean-name {
  color: #c4a7e7;
}

#theorem-detail .mathlib-link {
  display: inline-block;
  margin-top: 1.5rem;
  padding: 0.75rem 1.5rem;
  background: var(--accent);
  color: var(--text-bright);
  text-decoration: none;
  border-radius: 8px;
  font-weight: 600;
  transition: all 0.2s;
}

#theorem-detail .mathlib-link:hover {
  background: var(--accent-bright);
  transform: translateY(-2px);
}

/* ===== RELATED THEOREMS ===== */
.related-theorems {
  margin-top: 3rem;
}

.related-theorems h3 {
  font-size: 1.5rem;
  color: var(--text-bright);
  margin-bottom: 1.5rem;
}

.related-theorems .related-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(250px, 1fr));
  gap: 1rem;
}

.related-theorems .related-card {
  background: var(--bg-card);
  border: 2px solid var(--border);
  border-radius: 10px;
  padding: 1.5rem;
  cursor: pointer;
  transition: all 0.2s;
}

.related-theorems .related-card:hover {
  border-color: var(--accent);
  background: var(--bg-hover);
  transform: translateY(-2px);
}

.related-theorems .related-name {
  font-size: 1rem;
  font-weight: 600;
  color: var(--accent-bright);
  margin-bottom: 0.5rem;
}

.related-theorems .related-snippet {
  font-size: 0.9rem;
  color: var(--text-dim);
  line-height: 1.5;
}

/* ===== BUTTONS ===== */
.back-btn {
  background: transparent;
  border: 2px solid var(--border);
  color: var(--text-main);
  padding: 0.6rem 1.2rem;
  border-radius: 8px;
  cursor: pointer;
  font-size: 0.95rem;
  font-weight: 600;
  margin-bottom: 1.5rem;
  transition: all 0.2s;
}

.back-btn:hover {
  border-color: var(--accent);
  color: var(--accent-bright);
  background: var(--bg-hover);
}

/* ===== FOOTER ===== */
footer {
  background: var(--bg-card);
  padding: 2rem 0;
  border-top: 2px solid var(--border);
  text-align: center;
  margin-top: 4rem;
}

footer p {
  margin: 0.5rem 0;
  color: var(--text-dim);
  font-size: 0.95rem;
}

footer a {
  color: var(--accent-bright);
  text-decoration: none;
  font-weight: 600;
  transition: color 0.2s;
}

footer a:hover {
  color: var(--text-bright);
}

/* ===== DEPENDENCY GRAPH ===== */
.dep-map-btn {
  padding: 0.85rem 1.8rem;
  font-size: 1rem;
  font-weight: 600;
  background: linear-gradient(135deg, #8b7dd8 0%, #a394e8 100%);
  color: var(--text-bright);
  border: none;
  border-radius: 8px;
  cursor: pointer;
  transition: all 0.2s;
}

.dep-map-btn:hover {
  background: linear-gradient(135deg, #9a8dd8 0%, #b3a4f8 100%);
  transform: translateY(-1px);
}

.deps-btn {
  background: linear-gradient(135deg, #6a5acd 0%, #8b7dd8 100%);
  border: none;
  color: var(--text-bright);
  padding: 0.6rem 1.2rem;
  border-radius: 8px;
  cursor: pointer;
  font-size: 0.9rem;
  font-weight: 600;
  transition: all 0.2s;
  margin-right: 0.5rem;
}

.deps-btn:hover {
  background: linear-gradient(135deg, #7a6add 0%, #9b8de8 100%);
  transform: translateY(-1px);
}

.graph-view {
  min-height: 600px;
}

.graph-controls {
  display: flex;
  gap: 0.75rem;
  margin-bottom: 1.5rem;
  flex-wrap: wrap;
}

.graph-btn,
.graph-toggle-btn {
  padding: 0.6rem 1.2rem;
  font-size: 0.9rem;
  font-weight: 600;
  background: var(--bg-card);
  color: var(--text-main);
  border: 2px solid var(--border);
  border-radius: 8px;
  cursor: pointer;
  transition: all 0.2s;
}

.graph-btn:hover,
.graph-toggle-btn:hover {
  border-color: var(--accent);
  background: var(--bg-hover);
  color: var(--accent-bright);
}

.graph-toggle-btn {
  background: var(--accent);
  color: var(--text-bright);
  border-color: var(--accent);
}

.graph-toggle-btn:hover {
  background: var(--accent-bright);
  border-color: var(--accent-bright);
}

#graph-title {
  font-size: 2rem;
  color: var(--text-bright);
  margin-bottom: 1rem;
  text-align: center;
}

.graph-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 1rem;
  justify-content: center;
  margin-bottom: 1.5rem;
  padding: 1rem;
  background: var(--bg-card);
  border-radius: 10px;
  border: 2px solid var(--border);
}

.graph-legend-item {
  display: flex;
  align-items: center;
  gap: 0.5rem;
  font-size: 0.9rem;
  color: var(--text-dim);
}

.graph-legend-color {
  width: 20px;
  height: 20px;
  border-radius: 50%;
  border: 2px solid var(--border);
}

.graph-container {
  width: 100%;
  height: 700px;
  background: var(--bg-card);
  border-radius: 12px;
  border: 2px solid var(--border);
  overflow: hidden;
  position: relative;
}

.graph-container svg {
  width: 100%;
  height: 100%;
  cursor: grab;
}

.graph-container svg:active {
  cursor: grabbing;
}

.graph-node {
  cursor: pointer;
  transition: all 0.2s;
}

.graph-node:hover {
  filter: brightness(1.3);
}

.graph-node circle {
  stroke: var(--bg-dark);
  stroke-width: 2;
}

.graph-node.highlighted circle {
  stroke: var(--accent-bright);
  stroke-width: 4;
}

.graph-node.dimmed {
  opacity: 0.2;
}

.graph-link {
  stroke: var(--text-dim);
  stroke-opacity: 0.3;
  fill: none;
  stroke-width: 1.5;
}

.graph-link.highlighted {
  stroke: var(--accent-bright);
  stroke-opacity: 0.8;
  stroke-width: 2.5;
}

.graph-link.dimmed {
  stroke-opacity: 0.05;
}

.graph-label {
  font-size: 11px;
  fill: var(--text-main);
  pointer-events: none;
  text-anchor: middle;
  font-weight: 500;
}

.graph-label.dimmed {
  opacity: 0.2;
}

.graph-tooltip {
  position: absolute;
  background: var(--bg-dark);
  border: 2px solid var(--accent);
  border-radius: 8px;
  padding: 0.75rem 1rem;
  pointer-events: none;
  opacity: 0;
  transition: opacity 0.2s;
  font-size: 0.9rem;
  color: var(--text-bright);
  max-width: 250px;
  z-index: 1000;
  box-shadow: 0 4px 12px rgba(0, 0, 0, 0.4);
}

.graph-tooltip.visible {
  opacity: 1;
}

.graph-tooltip-name {
  font-weight: 600;
  color: var(--accent-bright);
  margin-bottom: 0.25rem;
}

.graph-tooltip-category {
  font-size: 0.8rem;
  color: var(--text-dim);
}

/* ===== UTILITY CLASSES ===== */
.hidden {
  display: none !important;
}

/* ===== RESPONSIVE ===== */
@media (max-width: 768px) {
  header h1 {
    font-size: 2rem;
  }

  .tagline {
    font-size: 1.1rem;
  }

  .header-top {
    flex-direction: column;
  }

  .theorem-of-day {
    flex: 1 1 auto !important;
  }

  .categories-grid {
    grid-template-columns: 1fr;
  }

  .search-container {
    flex-direction: column;
  }

  #search-input,
  #search-btn,
  .random-btn {
    width: 100%;
  }

  #theorem-detail {
    padding: 1.5rem;
  }

  .related-theorems .related-grid {
    grid-template-columns: 1fr;
  }
}

/* ===== DEPENDENCY TREES ===== */
.deps-section {
  display: flex;
  gap: 2rem;
  flex-wrap: wrap;
  margin-bottom: 1.5rem;
}
.deps-group {
  flex: 1;
  min-width: 250px;
  background: rgba(139, 125, 216, 0.05);
  border-radius: 10px;
  padding: 1rem 1.2rem;
  border: 1px solid var(--border);
}
.deps-group strong {
  color: var(--accent-bright);
  font-size: 0.95rem;
  display: block;
  margin-bottom: 0.5rem;
}
ul.dep-tree {
  list-style: none;
  padding-left: 1.2rem;
  margin: 0;
  border-left: 2px solid var(--border);
}
ul.dep-tree > li {
  position: relative;
  padding: 0.25rem 0 0.25rem 0.8rem;
}
ul.dep-tree > li::before {
  content: '';
  position: absolute;
  left: -2px;
  top: 0.85rem;
  width: 0.6rem;
  height: 0;
  border-top: 2px solid var(--border);
}
.dep-link {
  color: var(--accent);
  text-decoration: none;
  font-size: 0.9rem;
  transition: color 0.2s;
}
.dep-link:hover {
  color: var(--accent-bright);
  text-decoration: underline;
}

/* Compact dependency graph */
.dep-graph-compact {
  padding: 0;
}

.dep-layer {
  margin-bottom: 1.5rem;
}

.dep-layer-header {
  display: flex;
  align-items: center;
  gap: 0.8rem;
  margin-bottom: 0.8rem;
}

.dep-layer-label {
  font-size: 0.75rem;
  font-weight: 600;
  text-transform: uppercase;
  letter-spacing: 0.08em;
  color: var(--accent);
  white-space: nowrap;
}

.dep-layer-line {
  flex: 1;
  height: 1px;
  background: linear-gradient(to right, var(--accent), transparent);
}

.dep-layer-count {
  font-size: 0.7rem;
  color: var(--text-dim);
  background: rgba(139, 125, 216, 0.1);
  padding: 0.1rem 0.4rem;
  border-radius: 10px;
}

.dep-nodes {
  display: flex;
  flex-wrap: wrap;
  gap: 0.4rem;
}

.dep-node {
  display: inline-block;
  padding: 0.3rem 0.6rem;
  background: rgba(139, 125, 216, 0.08);
  border: 1px solid rgba(139, 125, 216, 0.15);
  border-radius: 6px;
  color: var(--text);
  text-decoration: none;
  font-size: 0.82rem;
  line-height: 1.3;
  transition: all 0.15s;
  cursor: pointer;
}

.dep-node:hover {
  background: rgba(139, 125, 216, 0.2);
  border-color: var(--accent);
  color: var(--accent-bright);
  text-decoration: none;
}

.dep-node-large {
  font-weight: 600;
  font-size: 0.9rem;
  background: rgba(139, 125, 216, 0.15);
  border-color: rgba(139, 125, 216, 0.3);
}

.dep-node-medium {
  font-weight: 500;
}

.dep-node-def {
  border-style: dashed;
  color: var(--text-dim);
}