:root{font-family:Inter,ui-sans-serif,system-ui,-apple-system,BlinkMacSystemFont,Segoe UI,sans-serif;color:#172033;background:#f4f6f8;font-synthesis:none;text-rendering:optimizeLegibility}*{box-sizing:border-box}body{margin:0;min-width:320px}button,input{font:inherit}button{border:0}.app-shell{min-height:100vh}.topbar{height:76px;display:flex;align-items:center;justify-content:space-between;padding:0 32px;background:#fff;border-bottom:1px solid #e1e5ea}.brand{font-size:22px;font-weight:750;letter-spacing:-.02em}.tagline{margin-top:3px;color:#697386;font-size:13px}.github-link{color:#273449;font-size:14px;text-decoration:none}.github-link:hover{text-decoration:underline}.topbar-links{display:flex;align-items:center;gap:16px}.workspace{display:grid;grid-template-columns:270px minmax(0,1fr);min-height:calc(100vh - 76px)}.sidebar{padding:30px 20px;background:#eef1f4;border-right:1px solid #dde2e8}.section-label{color:#7a8494;font-size:11px;font-weight:750;letter-spacing:.12em;text-transform:uppercase}.sidebar h2{margin:8px 0 18px;font-size:17px}.theorem-item{display:grid;grid-template-columns:28px 1fr;align-items:center;width:100%;padding:10px 9px;border-radius:7px;background:transparent;color:#354052;text-align:left;cursor:pointer}.theorem-item.active{background:#fff;box-shadow:0 1px 2px #1c263614;font-weight:650}.theorem-item:hover{background:#f8fafc}.status{color:#8792a2;font-variant-numeric:tabular-nums}.completed .status{color:#4f7d61}.proof-panel{width:100%;padding:42px 48px 64px}.theorem-header{display:flex;align-items:flex-start;justify-content:space-between;margin-bottom:26px}h1{margin:7px 0 0;font-size:28px;letter-spacing:-.025em}.mode-badge{padding:6px 9px;border:1px solid #d8dee6;border-radius:999px;color:#697386;background:#fff;font-size:12px}.card{margin-bottom:14px;padding:20px 22px;border:1px solid #dfe4ea;border-radius:10px;background:#fff}.card-title{color:#6f7989;font-size:12px;font-weight:750;letter-spacing:.08em;text-transform:uppercase}.goal-card{padding-top:18px}.goal-expression{margin-top:15px;font-family:ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;font-size:24px}.proof-expression{display:block;width:100%;min-width:0;max-width:100%;padding:2px 0 3px 1.5rem;overflow-wrap:anywhere;word-break:normal;white-space:normal;line-height:1.65;text-indent:-1.5rem}.proof-expression wbr{display:inline}.context-row{min-width:0}.context-row>.proof-expression{flex:1 1 auto}.bracket-pair{font-weight:750;transition:background-color .12s ease,text-shadow .12s ease}.bracket-pair:hover{text-shadow:0 0 .55em currentColor}.bracket-color-0{color:#d14d72}.bracket-color-1{color:#b7791f}.bracket-color-2{color:#4f7d61}.bracket-color-3{color:#3f6fa8}.bracket-color-4{color:#7a5aa6}.bracket-color-5{color:#b04f8a}.context-row .proof-expression{margin:0;padding:0;text-indent:0;line-height:1.4;overflow-wrap:anywhere}.context-row{display:flex;gap:10px;margin-top:13px;color:#778293}.context-row code{color:#273449}.tactic-history ol{margin:0;padding-left:1.5rem}.tactic-history li{margin:.35rem 0}.tactic-card{display:grid;grid-template-columns:1fr auto;gap:12px}.tactic-card .card-title{grid-column:1 / -1}.tactic-input{width:100%;min-width:0;padding:11px 12px;border:1px solid #cfd6df;border-radius:7px;outline:none}.tactic-input[aria-invalid=true]{border-color:#c44}.tactic-feedback{grid-column:1 / -1;margin-top:-4px;color:#b42318;font-size:14px}.tactic-input:focus{border-color:#8e9aab;box-shadow:0 0 0 3px #6e7c911f}.apply-button{align-self:stretch;padding:0 18px;border-radius:7px;background:#273449;color:#fff;font-weight:650}.proof-state{display:flex;align-items:center;justify-content:space-between;padding:20px 4px}.muted{margin:8px 0 0;color:#7a8494;font-size:14px}.goal-count{color:#697386;font-size:13px}.sr-only{position:absolute;width:1px;height:1px;padding:0;margin:-1px;overflow:hidden;clip:rect(0,0,0,0);white-space:nowrap;border:0}.state-message{margin-top:8px;font-size:14px}.state-message.neutral{color:#697386}.state-message.success{color:#356448}.state-message.error{color:#a13d3d}.goals-list{display:grid;gap:10px}.goal-item{padding:16px 18px;border:1px solid #dfe4ea;border-radius:10px;background:#fff}.goal-item.focused{border-color:#aeb8c5;box-shadow:0 1px 2px #1c26360d}.goal-heading{display:flex;justify-content:space-between;color:#6f7989;font-size:12px;font-weight:750;text-transform:uppercase;letter-spacing:.06em}.goal-context{margin-top:12px}.completed-state{display:grid;gap:5px;padding:18px;border:1px solid #cbd9cf;border-radius:10px;background:#f5f9f6;color:#356448}.completed-state span{color:#66776b;font-size:13px}.unavailable-state{display:grid;gap:7px}.unavailable-state strong{color:#5d3f3f}.unavailable-state span{color:#7a6868;font-size:13px;line-height:1.5}.next-button{margin-top:18px;padding:11px 16px;border-radius:7px;background:#273449;color:#fff;font-weight:650;cursor:pointer}.proof-layout{display:grid;grid-template-columns:minmax(0,1fr) 270px;gap:18px;align-items:start}.proof-main{min-width:0}.proof-state-card{margin-bottom:14px}.context-list{margin-top:10px}.tactic-panel{position:sticky;top:18px;padding:18px;border:1px solid #dfe4ea;border-radius:10px;background:#fff}.tactic-suggestions{display:grid;gap:9px;margin-top:12px}.tactic-suggestion{display:grid;gap:4px;width:100%;padding:11px 12px;border:1px solid #d9dfe6;border-radius:8px;background:#fff;color:#273449;text-align:left;cursor:pointer}.tactic-suggestion:hover{background:#f7f9fb;border-color:#aeb8c5}.tactic-suggestion code{font-weight:700}.tactic-suggestion span{color:#778293;font-size:12px;line-height:1.35}.tactic-other{margin-top:22px;padding-top:16px;border-top:1px solid #e4e8ed}.theorem-list{display:grid;gap:6px;max-height:320px;overflow-y:auto}.theorem-item{display:flex;align-items:center;justify-content:space-between;gap:10px}.tactic-other-item{display:block;width:100%;padding:7px 0;background:transparent;color:#667386;text-align:left;cursor:pointer}.tactic-other-item:hover{color:#273449}pre.proof-expression{white-space:pre-wrap;word-break:keep-all}.kv-shell{min-height:100vh;background:#f4f6f8}.kv-topbar{height:76px;display:flex;align-items:center;justify-content:space-between;padding:0 32px;background:#fff;border-bottom:1px solid #e1e5ea}.kv-back{color:#273449;font-size:14px;text-decoration:none}.kv-back:hover{text-decoration:underline}.kv-main{width:min(1080px,calc(100% - 36px));margin:0 auto;padding:44px 0 70px}.kv-hero{margin-bottom:24px}.kv-hero h1{font-size:clamp(30px,5vw,46px);max-width:780px}.kv-hero p{max-width:760px;color:#5f6b7b;font-size:16px;line-height:1.65}.kv-signatures{display:grid;gap:9px;margin-top:14px}.kv-formula{display:inline-block;padding:5px 8px;border-radius:6px;background:#f3f5f7;color:#273449;font-family:ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;font-size:13px}.kv-controls{display:grid;grid-template-columns:1fr 1fr auto;gap:20px;align-items:center;margin-top:20px}.kv-controls label{display:grid;grid-template-columns:auto 1fr auto;gap:10px;align-items:center;color:#526074;font-size:13px}.kv-controls input[type=range]{width:100%}.kv-controls output{min-width:22px;font-weight:700;text-align:right}.kv-check{white-space:nowrap}.kv-check input{margin:0}.kv-comparison{display:grid;grid-template-columns:1fr 1fr;gap:16px}.kv-path{min-height:280px}.kv-cached-path{border-color:#cbd9cf}.kv-node{margin-top:17px;padding:13px;border:1px solid #e1e5ea;border-radius:8px;background:#fbfcfd;text-align:center}.kv-arrow{padding:8px;color:#7b8797;text-align:center;font-size:18px}.kv-deps{margin-top:16px}.kv-dep-row{display:grid;grid-template-columns:minmax(0,1fr) 28px minmax(0,1fr) auto;gap:10px;align-items:center;padding:12px 0;border-bottom:1px solid #edf0f3}.kv-dep-row:last-child{border-bottom:0}.kv-dep-row strong{color:#4f7d61;font-size:12px;text-transform:uppercase}.kv-steps{margin-top:30px}.kv-step{display:grid;grid-template-columns:42px 1fr;gap:14px;margin-top:10px;padding:18px;border:1px solid #dfe4ea;border-radius:10px;background:#fff}.kv-step.done{border-color:#cbd9cf;background:#f9fbf9}.kv-step-number{width:30px;height:30px;display:grid;place-items:center;border-radius:50%;background:#eef1f4;color:#526074;font-weight:750}.kv-step.done .kv-step-number{background:#dce9df;color:#356448}.kv-step h3{margin:0;font-size:16px}.kv-step p{margin:7px 0 12px;color:#657184;line-height:1.5}.kv-prove-button{padding:8px 12px;border:1px solid #cfd6df;border-radius:7px;background:#fff;color:#273449;font-weight:650;cursor:pointer}.kv-prove-button:hover{background:#f5f7f9}.kv-proof-result{margin-top:12px;padding:10px 12px;border-left:3px solid #7a9a83;background:#f1f6f2;color:#526458;font-size:13px;line-height:1.5}.kv-cost{margin-top:28px}.kv-metrics{display:grid;grid-template-columns:repeat(3,1fr);gap:12px;margin-top:14px}.kv-metrics div{padding:16px;border:1px solid #e1e5ea;border-radius:8px}.kv-metrics span,.kv-metrics small{display:block;color:#718094;font-size:12px}.kv-metrics strong{display:block;margin:5px 0;font-size:28px}.kv-note{color:#7a8494;font-size:12px;line-height:1.5}.kv-conclusion{display:grid;gap:5px;margin-top:16px;padding:18px;border:1px solid #dfe4ea;border-radius:10px;background:#fff}.kv-conclusion.complete{border-color:#cbd9cf;background:#f5f9f6}.kv-conclusion strong{color:#273449}.kv-conclusion span{color:#697386;font-size:13px}@media(max-width:720px){.topbar,.kv-topbar{padding:0 18px}.workspace{grid-template-columns:1fr}.sidebar{border-right:0;border-bottom:1px solid #dde2e8;padding:22px 18px}.proof-panel{padding:30px 18px 48px}.theorem-header{gap:16px}.proof-layout{grid-template-columns:1fr}.tactic-panel{position:static}.kv-main{width:min(100% - 24px,1080px);padding-top:30px}.kv-controls,.kv-comparison,.kv-metrics{grid-template-columns:1fr}.kv-check{justify-self:start}.kv-dep-row{grid-template-columns:1fr;gap:4px}.kv-dep-row>span:nth-child(2){display:none}}.kv-hero-actions{display:flex;gap:10px;margin-top:18px}.kv-play,.kv-reset{padding:10px 15px;border-radius:8px;cursor:pointer;font-weight:700}.kv-play{background:#273449;color:#fff}.kv-reset{border:1px solid #cfd6df;background:#fff;color:#273449}.kv-interface{box-shadow:0 5px 20px #1c26360a}.kv-props-wrap{margin:14px 0;padding:13px;border:1px solid #e1e5ea;border-radius:8px;background:#fafbfd}.kv-mini-title,.kv-step-meta{color:#7a8494;font-size:10px;font-weight:800;letter-spacing:.11em;text-transform:uppercase}.kv-props{display:flex;flex-wrap:wrap;gap:7px;margin-top:9px}.kv-prop{animation:kv-pop .3s ease both}.kv-prop .kv-formula{background:#eef3f8;border:1px solid #dbe3eb}.kv-step{transition:opacity .35s ease,transform .35s ease,box-shadow .35s ease}.kv-step.hidden{display:none}.kv-step.visible{animation:kv-slide .42s ease both}.kv-step.done{box-shadow:0 0 0 2px #4f7d6114}.kv-step-meta{margin-bottom:4px}.kv-step-number{transition:transform .3s ease}.kv-step.done .kv-step-number{transform:scale(1.08)}.kv-timeline{height:5px;margin:12px 0 16px;border-radius:999px;background:#e4e8ed;overflow:hidden}.kv-timeline-progress{height:100%;border-radius:999px;background:#526074;transition:width .5s ease}.kv-deps{overflow:hidden}.kv-graph{display:grid;grid-template-columns:1fr 30px 1fr 30px 1.25fr;gap:10px;align-items:center;margin-top:16px}.kv-graph-node{min-height:70px;padding:12px;border:1px solid #dfe4ea;border-radius:9px;background:#fbfcfd;text-align:center;animation:kv-pop .4s ease both}.kv-graph-node small,.kv-node small{display:block;margin-top:6px;color:#7a8494;font-size:11px}.kv-graph-node.cache{border-color:#cbd9cf;background:#f5f9f6}.kv-graph-node.recompute{border-color:#d7dce3}.kv-graph-node.new{grid-column:1}.kv-graph-arrow{text-align:center;color:#8a95a5;font-size:20px}.kv-legend{display:flex;flex-wrap:wrap;gap:18px;margin-top:14px;color:#697386;font-size:12px}.kv-legend i{display:inline-block;width:8px;height:8px;margin-right:6px;border-radius:50%;background:#7a8494}.kv-legend .cache-dot{background:#4f7d61}.kv-legend .new-dot{background:#b7791f}.kv-legend .use-dot{background:#3f6fa8}.cache-node{border-color:#cbd9cf}.new-node{border-color:#e3d6bb}.kv-node{transition:transform .2s ease,box-shadow .2s ease}.kv-node:hover{transform:translateY(-2px);box-shadow:0 4px 12px #1c263612}@keyframes kv-slide{0%{opacity:0;transform:translateY(12px)}to{opacity:1;transform:translateY(0)}}@keyframes kv-pop{0%{opacity:0;transform:scale(.97)}to{opacity:1;transform:scale(1)}}@media(max-width:720px){.kv-controls,.kv-comparison,.kv-graph{grid-template-columns:1fr}.kv-graph-arrow{transform:rotate(90deg)}.kv-graph-node.new{grid-column:auto}.kv-main{width:min(100% - 24px,1080px);padding-top:28px}.kv-hero h1{font-size:32px}.kv-metrics{grid-template-columns:1fr}.kv-step{grid-template-columns:34px 1fr;padding:14px}.kv-topbar{height:68px}}