Add Nexus Mutual book value invariant research article

components/research/NexusMutualGuarantee.jsx

@@ -0,0 +1,137 @@
+import { useState, useEffect, useRef } from 'react'
+import katex from 'katex'
+import { ExternalLinkIcon } from './ExternalLink'
+
+function K({ tex }) {
+  const html = katex.renderToString(tex, { throwOnError: false })
+  return <span dangerouslySetInnerHTML={{ __html: html }} />
+}
+
+function Term({ tex, label, detail, align = 'center' }) {
+  const posClass =
+    align === 'left'
+      ? 'left-0'
+      : align === 'right'
+        ? 'right-0'
+        : 'left-1/2 -translate-x-1/2'
+
+  return (
+    <span className="relative group/term">
+      <span className="cursor-help border-b border-dotted border-muted/40 group-hover/term:border-heading/60 transition-colors">
+        <K tex={tex} />
+      </span>
+      <span
+        className={`pointer-events-none absolute ${posClass} bottom-full mb-2 opacity-0 group-hover/term:opacity-100 transition-opacity duration-150 z-10 w-max max-w-[260px]`}
+      >
+        <span className="block bg-heading text-white text-[12px] leading-snug font-sans rounded px-3 py-2 shadow-lg">
+          <span className="font-semibold">{label}</span>
+          <br />
+          {detail}
+        </span>
+      </span>
+    </span>
+  )
+}
+
+export default function NexusMutualGuarantee() {
+  const [showEnglish, setShowEnglish] = useState(true)
+  const timerRef = useRef(null)
+
+  useEffect(() => {
+    timerRef.current = setTimeout(() => setShowEnglish(false), 5000)
+    return () => clearTimeout(timerRef.current)
+  }, [])
+
+  const handleToggle = () => {
+    if (timerRef.current) {
+      clearTimeout(timerRef.current)
+      timerRef.current = null
+    }
+    setShowEnglish((prev) => !prev)
+  }
+
+  return (
+    <div className="py-6">
+      <button
+        onClick={handleToggle}
+        className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-muted hover:text-heading transition-colors cursor-pointer mb-4"
+      >
+        <svg
+          viewBox="0 0 24 24"
+          className="w-[13px] h-[13px]"
+          fill="none"
+          stroke="currentColor"
+          strokeWidth="1.5"
+          strokeLinecap="round"
+          strokeLinejoin="round"
+        >
+          <path d="m5 8 6 6" />
+          <path d="m4 14 6-6 2-3" />
+          <path d="M2 5h12" />
+          <path d="M7 2h1" />
+          <path d="m22 22-5-10-5 10" />
+          <path d="M14 18h6" />
+        </svg>
+        {showEnglish ? 'Switch to math' : 'Switch to English'}
+      </button>
+
+      <div className="grid text-center [&>*]:col-start-1 [&>*]:row-start-1">
+        <div
+          className="flex items-center justify-center transition-opacity duration-200 text-2xl md:text-3xl"
+          style={{
+            opacity: showEnglish ? 0 : 1,
+            pointerEvents: showEnglish ? 'none' : 'auto'
+          }}
+          aria-hidden={showEnglish}
+        >
+          <span className="inline-flex items-baseline gap-[0.15em] flex-wrap justify-center">
+            <Term
+              tex={'\\texttt{sellPrice}'}
+              label="Sell spot price"
+              detail="1e18 × ethReserve / nxmSellReserve"
+              align="left"
+            />
+            <K tex={'\\;\\leq\\;'} />
+            <Term
+              tex={'\\texttt{bookValue}'}
+              label="Book value per NXM"
+              detail="1e18 × poolCapital / totalSupply"
+            />
+            <K tex={'\\;\\leq\\;'} />
+            <Term
+              tex={'\\texttt{buyPrice}'}
+              label="Buy spot price"
+              detail="1e18 × ethReserve / nxmBuyReserve"
+              align="right"
+            />
+          </span>
+        </div>
+        <div
+          className="flex items-center justify-center transition-opacity duration-200"
+          style={{
+            opacity: showEnglish ? 1 : 0,
+            pointerEvents: showEnglish ? 'auto' : 'none'
+          }}
+          aria-hidden={!showEnglish}
+        >
+          <p className="text-xl md:text-2xl leading-snug font-serif">
+            The Nexus Mutual liquidity pool never sells NXM below book value,
+            and never buys it back above book value.
+          </p>
+        </div>
+      </div>
+
+      <div className="text-right mt-4">
+        <a
+          href="https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/NexusMutual/RammPriceBand/Specs.lean"
+          target="_blank"
+          rel="noopener noreferrer"
+          className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-accent hover:text-heading transition-colors cursor-pointer"
+        >
+          View Lean
+          <ExternalLinkIcon />
+        </a>
+      </div>
+    </div>
+  )
+}

data/research.js

@@ -1,4 +1,13 @@
 export const research = [
+  {
+    slug: 'nexus-mutual-book-value',
+    title: 'Nexus Mutual Book Value Invariant',
+    subtitle: 'A formally verified price band property of the RAMM.',
+    description:
+      'How we proved the book value invariant of Nexus Mutual\'s RAMM pricing mechanism using Verity and Lean 4.',
+    date: '2026-04-09',
+    tag: 'Case study'
+  },
   {
     slug: 'formalizing-transaction-interpretation',
     title: 'Formalizing Transaction Interpretation',