:root {
    --bg-light: #f5f2ec;
    --bg-dark: #1c1c1f;
    --text-primary-light: #2c2c30;
    --text-primary-dark: #e8e4dc;
    --text-secondary: #7a7670;
    --operator-rust: #8b4513;
    --rule-line: #c8c4bc;
}

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

body {
    background: var(--bg-light);
    color: var(--text-primary-light);
    font-family: 'Source Serif 4', Georgia, serif;
    font-weight: 400;
    font-size: clamp(1rem, 1.2vw, 1.15rem);
    line-height: 1.85;
    overflow-x: hidden;
}

.section {
    position: relative;
}

.light-bg {
    background: var(--bg-light);
}

.dark-bg {
    background: var(--bg-dark);
}

/* Proof Column */
.proof-column {
    max-width: 55vw;
    margin-left: 20vw;
    margin-right: 25vw;
    padding: 0 0 80px;
}

/* Axiom Space */
#axiom-space {
    min-height: 100vh;
    display: flex;
    align-items: flex-start;
}

#axiom-space .proof-column {
    padding-top: 38.2vh;
}

.domain-name {
    font-family: 'Cormorant Garamond', Georgia, serif;
    font-weight: 600;
    font-style: italic;
    font-size: clamp(2.5rem, 5vw, 4rem);
    letter-spacing: 0.02em;
    color: var(--text-primary-light);
    margin-bottom: 0;
}

.axiom-spacer {
    height: 120px;
}

.section-header {
    font-family: 'Cormorant Garamond', Georgia, serif;
    font-weight: 600;
    font-size: clamp(1.8rem, 3vw, 2.8rem);
    letter-spacing: 0.02em;
    color: var(--text-primary-light);
    margin-bottom: 64px;
}

/* Deduction */
#deduction {
    padding-bottom: 80px;
}

#deduction .proof-column {
    padding-top: 80px;
}

.proposition {
    position: relative;
    margin-bottom: 64px;
    opacity: 0;
    transition: opacity 0.4s ease;
}

.proposition.revealed {
    opacity: 1;
}

.prop-number {
    font-family: 'Cormorant Garamond', Georgia, serif;
    font-weight: 600;
    font-style: italic;
    font-size: clamp(1rem, 1.5vw, 1.3rem);
    letter-spacing: 0.02em;
    color: var(--text-secondary);
    position: absolute;
    left: -80px;
    top: 4px;
    transition: color 0.3s ease;
}

.prop-number:hover {
    color: var(--operator-rust);
}

.dark-number {
    color: var(--text-secondary);
}

.dark-number:hover {
    color: var(--operator-rust);
}

.prop-text {
    color: #3d3d42;
}

.dark-text {
    color: #c8c4bc;
}

.theorem-text {
    font-size: 1.15em;
}

.sub-argument {
    margin-left: 40px;
}

.operator {
    font-family: 'JetBrains Mono', monospace;
    font-weight: 400;
    color: var(--operator-rust);
}

/* Inference Rules */
.inference-rule {
    border: none;
    border-top: 1px solid var(--rule-line);
    width: 40%;
    margin-left: 0;
    margin-top: 0;
    margin-bottom: 160px;
}

.major-section-header {
    margin-bottom: 64px;
    opacity: 0;
    transition: opacity 0.4s ease;
}

.major-section-header.revealed {
    opacity: 1;
}

/* Turnstile Gate */
#turnstile-gate {
    min-height: 60vh;
    display: flex;
    flex-direction: column;
    align-items: center;
    justify-content: center;
    background: var(--bg-dark);
}

.turnstile-symbol {
    font-size: 20vw;
    line-height: 1;
    color: var(--text-primary-dark);
    text-align: center;
    font-family: 'JetBrains Mono', monospace;
}

.therefore {
    font-family: 'Cormorant Garamond', Georgia, serif;
    font-weight: 600;
    font-size: 1.2rem;
    font-variant: small-caps;
    letter-spacing: 0.2em;
    color: var(--text-secondary);
    margin-top: 24px;
}

/* Theorem */
#theorem {
    min-height: 60vh;
    display: flex;
    align-items: flex-start;
    padding-top: 80px;
}

#theorem .proof-column {
    padding-top: 0;
}

.theorem-prop {
    margin-bottom: 40px;
}

.qed {
    font-family: 'Cormorant Garamond', Georgia, serif;
    font-weight: 600;
    font-variant: small-caps;
    letter-spacing: 0.3em;
    font-size: 1rem;
    color: var(--text-secondary);
    text-align: right;
}

.end-space {
    height: 200px;
}

/* Responsive */
@media (max-width: 768px) {
    .proof-column {
        max-width: 90vw;
        margin-left: 5vw;
        margin-right: 5vw;
    }

    .prop-number {
        position: static;
        display: block;
        margin-bottom: 8px;
    }

    .sub-argument {
        margin-left: 20px;
    }

    .turnstile-symbol {
        font-size: 30vw;
    }

    #axiom-space .proof-column {
        padding-top: 25vh;
    }
}