diff --git a/.gitignore b/.gitignore
index 5e3f6474..b38986da 100644
--- a/.gitignore
+++ b/.gitignore
@@ -64,12 +64,19 @@ data/*.iso
 **/_build/
 **/__pycache__/
 
+# Agda build artifacts
+*.agdai
+
 # Hardware/FPGA build artifacts
 **/obj_dir/
 **/hardware/sparkle/tangnano9k/*.fs
 **/hardware/sparkle/tangnano9k/*.pnr.json
 **/hardware/sparkle/tangnano9k/*.history
 **/hardware/sparkle/tangnano9k/sparkle_tangnano9k.json
+4-Infrastructure/hardware/tangnano9k/
+4-Infrastructure/hardware/tangnano9k_*.fs
+4-Infrastructure/hardware/tangnano9k_*.json
+4-Infrastructure/hardware/tangnano9k_*_pnr.json
 *.vcd
 *_tb.v
 *_test_vectors.json
@@ -89,6 +96,10 @@ shared-data/
 **/target/
 tools/servo-fetch/
 
+# Local runtime sandboxes
+**/.sandbox-home/
+**/.sandbox-tmp/
+
 # JavaScript build artifacts
 **/node_modules/
 
@@ -112,12 +123,72 @@ extensions/
 2-Search-Space/PINNs/
 2-Search-Space/alphageometry/
 2-Search-Space/neural-conservation-law/
+2-Search-Space/search/stract/crates/optics/testcases/samples/
 6-Documentation/papers/Downloads_from_internet/
 6-Documentation/papers/downloads/
 6-Documentation/papers/facebook_pdfs/
 6-Documentation/papers/literature/
 6-Documentation/papers/supporting-materials/
 
+# Generated benchmark corpora and run outputs.
+3-Mathematical-Models/dna_benchmark/**/corpus/
+3-Mathematical-Models/dna_benchmark/results/
+3-Mathematical-Models/dna_benchmark/**/compressor_manifold.json
+3-Mathematical-Models/dna_benchmark/**/eigenvalue_survey.json
+3-Mathematical-Models/equations_parquet_tagged/*_curriculum.jsonl
+3-Mathematical-Models/equations_parquet_tagged/*_receipt.json
+3-Mathematical-Models/equations_parquet_tagged/*_table.csv
+3-Mathematical-Models/unified_surface/cache/
+
+# Generated shim/app run bundles.
+4-Infrastructure/shim/erdos_surface_orchestrator/out/
+4-Infrastructure/shim/*_after.json
+4-Infrastructure/shim/*_benchmarks.csv
+4-Infrastructure/shim/*_before.json
+4-Infrastructure/shim/*_bit.json
+4-Infrastructure/shim/*_checkpoint.json
+4-Infrastructure/shim/*_compression.json
+4-Infrastructure/shim/*_curriculum.jsonl
+4-Infrastructure/shim/*_eigenvectors.json
+4-Infrastructure/shim/*_lut.json
+4-Infrastructure/shim/*_manifest.jsonl
+4-Infrastructure/shim/*_packages.json
+4-Infrastructure/shim/*_packets.jsonl
+4-Infrastructure/shim/*_pull.json
+4-Infrastructure/shim/*_receipt.json
+4-Infrastructure/shim/*_receipt_*.json
+4-Infrastructure/shim/*_report.json
+4-Infrastructure/shim/*_responses.jsonl
+4-Infrastructure/shim/*_results.json
+4-Infrastructure/shim/*_sft.jsonl
+4-Infrastructure/shim/*_smoke.json
+4-Infrastructure/shim/*_stream.bin
+4-Infrastructure/shim/finance_claim_remote_bundle/
+4-Infrastructure/shim/finance_claim_lut_fixtures/claim-*/
+4-Infrastructure/shim/finance_claim_lut_fixtures/*.pdf
+4-Infrastructure/shim/full_gambit_runs/
+4-Infrastructure/shim/h200_encode_dry_run/
+4-Infrastructure/shim/offload_receipts/
+4-Infrastructure/shim/parallel_metaprobe_runs/
+4-Infrastructure/shim/tang9k_pbacs_receipts/
+5-Applications/linear-native-tauri/gen/
+
+# Generated hardware probe products.
+4-Infrastructure/hardware/batch_results/
+4-Infrastructure/hardware/*_receipt.json
+4-Infrastructure/hardware/*.png
+4-Infrastructure/hardware/*.pdf
+4-Infrastructure/hardware/metamanifold_prover.json
+
+# Local documentation exports and downloaded references.
+6-Documentation/chat-log-dumps/
+6-Documentation/docs/reference-videos/
+6-Documentation/docs/x86_64_specs/*.pdf
+6-Documentation/docs/x86_64_specs/*.txt
+6-Documentation/reports/jupyter-books/
+6-Documentation/reports/typst/*.pdf
+5-Applications/text-to-cad/models/.*/
+
 # Kernel module build artifacts
 *.ko
 *.mod
diff --git a/5-Applications/scripts/adaptive_research_analysis.py b/5-Applications/scripts/adaptive_research_analysis.py
new file mode 100644
index 00000000..9ab733fe
--- /dev/null
+++ b/5-Applications/scripts/adaptive_research_analysis.py
@@ -0,0 +1,334 @@
+#!/usr/bin/env python3
+# /// script
+# requires-python = ">=3.10"
+# dependencies = ["requests", "rich"]
+# ///
+"""
+Adaptive Research Stack Analyzer
+Uses Ollama Cloud API to run a three-pass analysis:
+  1. Summarize  - distill key ideas from core documents
+  2. Cross-link - find connections across domains
+  3. Critique   - identify gaps, weak claims, missing proofs
+
+Usage:
+    uv run scripts/adaptive_research_analysis.py
+    uv run scripts/adaptive_research_analysis.py --model gemma3:12b --out /tmp/analysis.md
+"""
+
+import argparse
+import datetime
+import json
+import os
+import sys
+import textwrap
+from pathlib import Path
+
+import requests
+from rich.console import Console
+from rich.markdown import Markdown
+from rich.panel import Panel
+from rich.progress import Progress, SpinnerColumn, TextColumn
+
+# ---------------------------------------------------------------------------
+# Config
+# ---------------------------------------------------------------------------
+RESEARCH_ROOT = Path("/home/allaun/Documents/Research Stack")
+API_BASE = "https://ollama.com/v1"
+API_KEY = os.environ.get("OLLAMA_API_KEY", "")
+# Model priority: cogito (Cognition 671B) → qwen3-next (80B) → gemma4 (31B) → deepseek-v4-flash
+DEFAULT_MODEL = "cogito-2.1:671b"
+FALLBACK_CHAIN = ["qwen3-next:80b", "gemma4:31b", "deepseek-v4-flash"]
+
+# Key documents to feed into the analysis (relative to RESEARCH_ROOT)
+CORE_DOCS = [
+    "README.md",
+    "CONCEPTS.md",
+    "ARCHITECTURE.md",
+    "SIGNAL_THEORY_COMPENDIUM.md",
+    "6-Documentation/EXPLANATION_FOR_HUMANS.md",
+    "6-Documentation/MATH_CORE.md",
+    "6-Documentation/VISION_NORTH_STAR.md",
+    "6-Documentation/GLOSSARY.md",
+    "6-Documentation/FIRST_PRINCIPLES_DAG.md",
+    "6-Documentation/FIELD_EQUATION_COMPARISON.md",
+    "6-Documentation/docs/SKEPTICISM_GRADIENT_REASSESSMENT_2026-04-29.md",
+    "6-Documentation/docs/CLAIM_STATE_AUDIT_2026-05-05.md",
+    "6-Documentation/docs/IMPLEMENTATION_ATTACK_ANALYSIS.md",
+    "6-Documentation/docs/ENE_RESEARCH_TOPIC_CANDIDATES.md",
+    "6-Documentation/docs/OTOM_V1_PAPER_STRUCTURE_AND_NEXT_GEN_SIMULATOR.md",
+    "6-Documentation/docs/stack_solidification_staging_manifest_2026-05-10.md",
+    "6-Documentation/docs/cross_domain_adaptation_numeric_review.md",
+    "6-Documentation/docs/BAD_MATH_CLEANUP_REPORT.md",
+]
+
+DOMAIN_DIRS = {
+    "Core Formalism (Lean)":   "0-Core-Formalism",
+    "Distributed Systems":     "1-Distributed-Systems",
+    "Search Space":            "2-Search-Space",
+    "Mathematical Models":     "3-Mathematical-Models",
+    "Infrastructure / FPGA":  "4-Infrastructure",
+    "Applications":            "5-Applications",
+    "Documentation":           "6-Documentation/docs",
+}
+
+MAX_CHARS_PER_DOC = 8_000    # truncate individual docs (DeepSeek handles large context)
+MAX_CONTEXT_CHARS = 120_000  # total context fed per LLM call
+
+console = Console()
+
+
+# ---------------------------------------------------------------------------
+# Helpers
+# ---------------------------------------------------------------------------
+
+def load_doc(path: Path, max_chars: int = MAX_CHARS_PER_DOC) -> str:
+    try:
+        text = path.read_text(errors="replace")
+        if len(text) > max_chars:
+            text = text[:max_chars] + f"\n\n[... truncated at {max_chars} chars ...]"
+        return text
+    except Exception as e:
+        return f"[Could not read {path}: {e}]"
+
+
+def gather_context() -> str:
+    """Load core docs and first-file samples from each domain directory."""
+    parts = []
+
+    # Core documents
+    for rel in CORE_DOCS:
+        p = RESEARCH_ROOT / rel
+        if p.exists():
+            parts.append(f"\n\n---\n## FILE: {rel}\n\n{load_doc(p)}")
+
+    # Domain directory samples — grab up to 3 .md files per domain
+    for domain, rel_dir in DOMAIN_DIRS.items():
+        d = RESEARCH_ROOT / rel_dir
+        if not d.is_dir():
+            continue
+        md_files = sorted(d.glob("*.md"))[:3]
+        for mdf in md_files:
+            rel_path = mdf.relative_to(RESEARCH_ROOT)
+            parts.append(f"\n\n---\n## FILE [{domain}]: {rel_path}\n\n{load_doc(mdf, 3000)}")
+
+    combined = "\n".join(parts)
+    if len(combined) > MAX_CONTEXT_CHARS:
+        combined = combined[:MAX_CONTEXT_CHARS] + "\n\n[... context truncated ...]"
+    return combined
+
+
+def chat(model: str, system: str, user: str, label: str, retries: int = 3) -> str:
+    """Call Ollama Cloud chat completions endpoint with retry + fallback."""
+    import time
+
+    headers = {
+        "Authorization": f"Bearer {API_KEY}",
+        "Content-Type": "application/json",
+    }
+
+    models_to_try = [model] + [m for m in FALLBACK_CHAIN if m != model]
+
+    for attempt_model in models_to_try:
+        payload = {
+            "model": attempt_model,
+            "messages": [
+                {"role": "system", "content": system},
+                {"role": "user",   "content": user},
+            ],
+            "stream": False,
+            "options": {"temperature": 0.3, "num_predict": 8192},
+        }
+        for attempt in range(1, retries + 1):
+            with Progress(
+                SpinnerColumn(),
+                TextColumn(f"[bold cyan]{label}[/bold cyan] (model: {attempt_model}, attempt {attempt}/{retries}) ..."),
+                transient=True,
+                console=console,
+            ) as progress:
+                progress.add_task("", total=None)
+                try:
+                    resp = requests.post(
+                        f"{API_BASE}/chat/completions",
+                        headers=headers,
+                        json=payload,
+                        timeout=600,
+                    )
+                except requests.exceptions.Timeout:
+                    console.print(f"[yellow]Timeout on attempt {attempt}, retrying...[/yellow]")
+                    time.sleep(5 * attempt)
+                    continue
+
+            if resp.status_code == 200:
+                data = resp.json()
+                content = data["choices"][0]["message"]["content"]
+                # Strip <think>...</think> reasoning blocks if present
+                import re
+                content = re.sub(r"<think>.*?</think>", "", content, flags=re.DOTALL).strip()
+                return content
+
+            error_body = resp.text[:300]
+            if "overloaded" in error_body.lower() or resp.status_code in (503, 429):
+                wait = 10 * attempt
+                console.print(f"[yellow]Server overloaded (attempt {attempt}), waiting {wait}s...[/yellow]")
+                time.sleep(wait)
+            elif resp.status_code == 500:
+                console.print(f"[yellow]500 error with {attempt_model}, trying next model...[/yellow]")
+                break  # try fallback model
+            else:
+                console.print(f"[red]API error {resp.status_code}:[/red] {error_body}")
+                sys.exit(1)
+
+        console.print(f"[yellow]Exhausted retries for {attempt_model}, trying fallback...[/yellow]")
+
+    console.print("[red]All models failed. Aborting.[/red]")
+    sys.exit(1)
+
+
+# ---------------------------------------------------------------------------
+# Analysis passes
+# ---------------------------------------------------------------------------
+
+SYSTEM_BASE = """\
+You are an expert research analyst reviewing a cutting-edge research stack called OTOM \
+(One-Time Operations on Manifolds / Ultra-low-power zero-decimal data routing). \
+The stack spans Lean 4 formal proofs, FPGA hardware, distributed systems, genomics, \
+astrophysics, signal theory, and compression mathematics. \
+Be precise, technical, and honest. Do NOT hallucinate citations. \
+When you are uncertain, say so explicitly.\
+"""
+
+
+def pass_summarize(model: str, context: str) -> str:
+    system = SYSTEM_BASE + """
+
+Your task: SUMMARIZE.
+Produce a structured executive summary of this research stack covering:
+1. Core thesis and central claims
+2. Mathematical foundations (key equations, structures, proof techniques)
+3. Hardware targets and implementation status
+4. Applied domains (compression, genomics, astrophysics, etc.)
+5. Current maturity level — what is proven vs speculative
+Keep each section under 250 words. Use markdown headers.
+"""
+    user = f"Here is the research stack content:\n\n{context}\n\nProduce the structured summary now."
+    return chat(model, system, user, "Pass 1: Summarize")
+
+
+def pass_crosslink(model: str, context: str, summary: str) -> str:
+    system = SYSTEM_BASE + """
+
+Your task: CROSS-DOMAIN LINKING.
+Given the research content and the summary already produced, identify:
+1. Non-obvious connections between domains (e.g. genomics ↔ topology, signal theory ↔ FPGA routing)
+2. Concepts that appear in multiple domains under different names (unification opportunities)
+3. Mathematical structures that bridge multiple layers of the stack
+4. Any surprising overlaps with known external research (mention without fabricating citations)
+Format as a markdown table + narrative explanation for each link found.
+"""
+    user = f"Summary:\n{summary}\n\n---\nFull context:\n{context}\n\nIdentify cross-domain links now."
+    return chat(model, system, user, "Pass 2: Cross-link")
+
+
+def pass_critique(model: str, context: str, summary: str) -> str:
+    system = SYSTEM_BASE + """
+
+Your task: CRITIQUE AND GAP ANALYSIS.
+Be rigorous and honest. Identify:
+1. Claims that lack formal proof or empirical validation — flag each clearly
+2. Mathematical steps that appear hand-wavy or unjustified
+3. Research gaps: important questions the stack does not yet address
+4. Risks: places where the stack's assumptions could break down
+5. Recommended next experiments or proof targets
+Be constructive but unflinching. A weak critique is useless.
+Format with severity tags: [CRITICAL], [MODERATE], [MINOR].
+"""
+    user = f"Summary:\n{summary}\n\n---\nFull context:\n{context}\n\nDeliver the critique now."
+    return chat(model, system, user, "Pass 3: Critique")
+
+
+# ---------------------------------------------------------------------------
+# Main
+# ---------------------------------------------------------------------------
+
+def main():
+    parser = argparse.ArgumentParser(description="Adaptive Research Stack Analyzer")
+    parser.add_argument("--model", default=DEFAULT_MODEL,
+                        help=f"Ollama Cloud model to use (default: {DEFAULT_MODEL}, fallback chain: {FALLBACK_CHAIN})")
+    parser.add_argument("--out", default=None,
+                        help="Output markdown file path (default: auto-named in Research Stack)")
+    parser.add_argument("--list-models", action="store_true",
+                        help="List available Ollama Cloud models and exit")
+    args = parser.parse_args()
+
+    if not API_KEY:
+        console.print("[red]Set OLLAMA_API_KEY before calling the Ollama Cloud API.[/red]")
+        sys.exit(1)
+
+    if args.list_models:
+        resp = requests.get(
+            "https://ollama.com/api/tags",
+            headers={"Authorization": f"Bearer {API_KEY}"},
+            timeout=30,
+        )
+        models = [m["name"] for m in resp.json().get("models", [])]
+        console.print("\n".join(sorted(models)))
+        return
+
+    console.rule("[bold green]Adaptive Research Stack Analyzer[/bold green]")
+    console.print(f"Model: [bold]{args.model}[/bold]   Root: {RESEARCH_ROOT}\n")
+
+    # --- Gather context
+    console.print("[dim]Gathering research documents...[/dim]")
+    context = gather_context()
+    char_count = len(context)
+    console.print(f"[dim]Context: {char_count:,} chars across core docs + domain samples[/dim]\n")
+
+    # --- Three passes
+    summary   = pass_summarize(args.model, context)
+    crosslink = pass_crosslink(args.model, context, summary)
+    critique  = pass_critique(args.model, context, summary)
+
+    # --- Assemble report
+    timestamp = datetime.datetime.now().strftime("%Y-%m-%d %H:%M")
+    report = f"""# Adaptive Research Analysis Report
+*Generated: {timestamp} | Model: {args.model}*
+
+---
+
+## Pass 1 — Executive Summary
+
+{summary}
+
+---
+
+## Pass 2 — Cross-Domain Links
+
+{crosslink}
+
+---
+
+## Pass 3 — Critique & Gap Analysis
+
+{critique}
+
+---
+*Analysis performed by `scripts/adaptive_research_analysis.py` using Ollama Cloud API.*
+"""
+
+    # --- Output
+    if args.out:
+        out_path = Path(args.out)
+    else:
+        date_str = datetime.datetime.now().strftime("%Y-%m-%d")
+        out_path = RESEARCH_ROOT / "6-Documentation" / "docs" / "reports" / f"adaptive_analysis_{date_str}.md"
+        out_path.parent.mkdir(parents=True, exist_ok=True)
+
+    out_path.write_text(report)
+
+    console.rule("[bold green]Analysis Complete[/bold green]")
+    console.print(f"\nReport saved to: [bold]{out_path}[/bold]\n")
+    console.print(Markdown(report[:6000] + ("\n\n*[report truncated for display — see file for full output]*" if len(report) > 6000 else "")))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/5-Applications/scripts/eigengate_paradigm_analysis.py b/5-Applications/scripts/eigengate_paradigm_analysis.py
new file mode 100644
index 00000000..174b65c7
--- /dev/null
+++ b/5-Applications/scripts/eigengate_paradigm_analysis.py
@@ -0,0 +1,342 @@
+#!/usr/bin/env python3
+# /// script
+# requires-python = ">=3.10"
+# dependencies = ["requests", "rich"]
+# ///
+"""
+EigenGate Paradigm Analysis
+Re-runs the three-pass adaptive analysis (summarize / cross-link / critique)
+with the EigenGate as the central lens.
+
+Context loaded:
+  - Kernel/EigenGate.lean + GateChain.lean  (the new paradigm)
+  - HCMMR/Core.lean + Bridge.lean + Manifest.lean (the old Gate typeclass)
+  - HCMMR/Laws/ (14, 15, 15E, 16, 17, 18)
+  - HCMMR/Kernels/ (RecamanFieldStep, FAMMScarMemory, PrimeGearCache, SNRAnomalyDetector)
+  - HCMMR/v0_2_Roadmap.md
+  - Core/ layer (FoldedPointManifold, UnderverseZeroLayer, QuantumFoamBoundary,
+                 S3CProjectedGeodesicResolution, PathEpigeneticManifold)
+  - FAMM.lean, ReceiptCore.lean, FixedPoint.lean (substrate)
+
+The three passes ask:
+  1. SUMMARIZE  — what does the EigenGate paradigm actually unify?
+  2. CROSS-LINK — where does ∥G·s − s∥ ≤ τ naturally appear across all kernels/laws?
+  3. CRITIQUE   — what is still hand-wavy, what must be proven, what is the migration plan?
+"""
+
+import datetime
+import os
+import re
+import sys
+import time
+from pathlib import Path
+
+import requests
+from rich.console import Console
+from rich.markdown import Markdown
+from rich.progress import Progress, SpinnerColumn, TextColumn
+
+RESEARCH_ROOT = Path("/home/allaun/Documents/Research Stack")
+LEAN_ROOT = RESEARCH_ROOT / "0-Core-Formalism/lean/Semantics/Semantics"
+API_BASE   = "https://ollama.com/v1"
+API_KEY = os.environ.get("OLLAMA_API_KEY", "")
+DEFAULT_MODEL  = "cogito-2.1:671b"
+FALLBACK_CHAIN = ["qwen3-next:80b", "gemma4:31b", "deepseek-v4-flash"]
+
+MAX_PER_FILE   = 10_000   # chars per lean file (they're dense)
+MAX_CONTEXT    = 110_000  # total context chars
+
+console = Console()
+
+# ---------------------------------------------------------------------------
+# Files to load — ordered by conceptual priority
+# ---------------------------------------------------------------------------
+LEAN_FILES = [
+    # ── New paradigm kernel ──────────────────────────────────────────────
+    "Kernel/EigenGate.lean",
+    "Kernel/GateChain.lean",
+
+    # ── Old Gate typeclass (what needs migrating) ─────────────────────
+    "HCMMR/Core.lean",
+    "HCMMR/Bridge.lean",
+    "HCMMR/Manifest.lean",
+
+    # ── Laws (old Gate pattern) ──────────────────────────────────────────
+    "HCMMR/Laws/Law14_Motion.lean",
+    "HCMMR/Laws/Law15_Field.lean",
+    "HCMMR/Laws/Law15E_SignalDetection.lean",
+    "HCMMR/Laws/Law16_Entropy.lean",
+    "HCMMR/Laws/Law17_Observer.lean",
+    "HCMMR/Laws/Law18_Constants.lean",
+
+    # ── Kernels ──────────────────────────────────────────────────────────
+    "HCMMR/Kernels/RecamanFieldStep.lean",
+    "HCMMR/Kernels/FAMMScarMemory.lean",
+    "HCMMR/Kernels/PrimeGearCache.lean",
+    "HCMMR/Kernels/SNRAnomalyDetector.lean",
+
+    # ── Core substrate ───────────────────────────────────────────────────
+    "Core/FoldedPointManifold.lean",
+    "Core/UnderverseZeroLayer.lean",
+    "Core/QuantumFoamBoundary.lean",
+    "Core/S3CProjectedGeodesicResolution.lean",
+    "Core/PathEpigeneticManifold.lean",
+]
+
+EXTRA_DOCS = [
+    # Roadmap and substrate prose
+    "HCMMR/v0_2_Roadmap.md",
+    "0-Core-Formalism/lean/Semantics/Semantics/FAMM.lean",
+]
+
+# ---------------------------------------------------------------------------
+# Helpers
+# ---------------------------------------------------------------------------
+
+def load(path: Path, max_chars: int = MAX_PER_FILE) -> str:
+    try:
+        text = path.read_text(errors="replace")
+        if len(text) > max_chars:
+            text = text[:max_chars] + f"\n-- [truncated at {max_chars} chars]"
+        return text
+    except Exception as e:
+        return f"-- [could not read {path}: {e}]"
+
+
+def gather_context() -> str:
+    parts = []
+    for rel in LEAN_FILES:
+        p = LEAN_ROOT / rel
+        label = f"LEAN: {rel}"
+        parts.append(f"\n\n---\n## {label}\n\n```lean\n{load(p)}\n```")
+
+    for rel in EXTRA_DOCS:
+        p = RESEARCH_ROOT / rel
+        label = f"DOC: {rel}"
+        parts.append(f"\n\n---\n## {label}\n\n{load(p, 6000)}")
+
+    combined = "\n".join(parts)
+    if len(combined) > MAX_CONTEXT:
+        combined = combined[:MAX_CONTEXT] + "\n\n-- [context truncated]"
+    return combined
+
+
+def chat(model: str, system: str, user: str, label: str, retries: int = 3) -> str:
+    headers = {"Authorization": f"Bearer {API_KEY}", "Content-Type": "application/json"}
+    models_to_try = [model] + [m for m in FALLBACK_CHAIN if m != model]
+
+    for attempt_model in models_to_try:
+        payload = {
+            "model": attempt_model,
+            "messages": [
+                {"role": "system", "content": system},
+                {"role": "user",   "content": user},
+            ],
+            "stream": False,
+            "options": {"temperature": 0.2, "num_predict": 8192},
+        }
+        for attempt in range(1, retries + 1):
+            with Progress(SpinnerColumn(),
+                          TextColumn(f"[bold cyan]{label}[/bold cyan] ({attempt_model}, try {attempt}) ..."),
+                          transient=True, console=console) as p:
+                p.add_task("", total=None)
+                try:
+                    resp = requests.post(f"{API_BASE}/chat/completions",
+                                         headers=headers, json=payload, timeout=600)
+                except requests.exceptions.Timeout:
+                    console.print(f"[yellow]Timeout, retrying...[/yellow]")
+                    time.sleep(5 * attempt)
+                    continue
+
+            if resp.status_code == 200:
+                content = resp.json()["choices"][0]["message"]["content"]
+                content = re.sub(r"<think>.*?</think>", "", content, flags=re.DOTALL).strip()
+                return content
+
+            body = resp.text[:300]
+            if "overloaded" in body.lower() or resp.status_code in (429, 503):
+                wait = 12 * attempt
+                console.print(f"[yellow]Overloaded, waiting {wait}s...[/yellow]")
+                time.sleep(wait)
+            elif resp.status_code == 500:
+                console.print(f"[yellow]500 on {attempt_model}, trying fallback...[/yellow]")
+                break
+            else:
+                console.print(f"[red]API error {resp.status_code}:[/red] {body}")
+                sys.exit(1)
+        console.print(f"[yellow]Exhausted retries for {attempt_model}[/yellow]")
+
+    console.print("[red]All models failed.[/red]")
+    sys.exit(1)
+
+# ---------------------------------------------------------------------------
+# System prompt — shared across all three passes
+# ---------------------------------------------------------------------------
+SYSTEM = """\
+You are an expert in formal verification (Lean 4), type theory, and physics-informed \
+computation. You are reviewing the HCMMR (Hyper-Coherent Morphic Meta-Recursion) \
+research stack on its `distilled` branch.
+
+The stack is undergoing a PARADIGM SHIFT. The old system used a flat `Gate` struct \
+(name, required, score, verdict). The new paradigm is the `Eigengate`:
+
+    structure Eigengate (α : Type) where
+      operator  : α → α       -- G: the operator whose fixed points encode the law
+      residual  : α → Q0_16   -- ∥G·s − s∥, normalised to [0,1)
+      threshold : Q0_16       -- τ: max admissible residual
+
+The central doctrine: EVERY physical law, routing decision, and compression check \
+is an eigenstate condition ∥G·s − s∥ ≤ τ. The full physical universe is the \
+intersection of λ=1 eigenspaces for all required gate operators simultaneously.
+
+The migration is INCOMPLETE. EigenGate.lean and GateChain.lean exist but are not \
+imported by anything. All Laws (14–18) still use the old Gate struct. The kernels \
+(RecamanFieldStep, FAMMScarMemory, PrimeGearCache, SNRAnomalyDetector) also use old Gate. \
+LawRecovery.lean (concrete eigengate constructors for each physical law) was never written.
+
+Be precise, rigorous, and honest. Do not hallucinate. Flag uncertainty explicitly.\
+"""
+
+# ---------------------------------------------------------------------------
+# Pass 1 — Summarize what the EigenGate paradigm actually unifies
+# ---------------------------------------------------------------------------
+PASS1_SYS = SYSTEM + """
+
+YOUR TASK: PARADIGM SUMMARY.
+Given all the Lean source files, answer:
+1. What does the Eigengate pattern (`∥G·s − s∥ ≤ τ`) actually unify across the stack?
+   List every law/kernel and state what G, s, and the residual would be in each case.
+2. What is the relationship between the old `Gate` struct and `Eigengate`?
+   Are they isomorphic? Can one be mechanically derived from the other?
+3. What does `Semantics.Kernel.EigenGate` currently prove that the old HCMMR/Core does not?
+4. What is the correct `α` type for each of the six laws (14, 15K, 15A-D, 15E, 16, 17, 18)?
+   Be specific — what Lean type carries the state?
+5. Where does the Recamán kernel fit in the eigengate picture?
+   What is G for a Recamán field step?
+
+Use markdown headers per section. Be concrete — reference actual line numbers and
+struct fields from the source files where relevant.
+"""
+
+# ---------------------------------------------------------------------------
+# Pass 2 — Cross-link: where does ∥G·s − s∥ naturally appear already?
+# ---------------------------------------------------------------------------
+PASS2_SYS = SYSTEM + """
+
+YOUR TASK: CROSS-DOMAIN EIGENGATE DETECTION.
+Scan all the Lean files in the context. For each file/module, identify:
+1. Any existing computation that already computes something of the form ∥G·s − s∥
+   (even if not named that way). What is G? What is s? What is the residual value?
+2. Any existing `residual`, `score`, `epsilon`, or `delta` computation that could
+   directly become the `residual : α → Q0_16` field of an Eigengate.
+3. Any existing operator/transform that maps a state to a new state — these are
+   candidate `operator : α → α` fields.
+4. Places where the old Gate struct's `score` field is set to a formula (not just
+   a constant `Q16_16.one`) — these are the richest migration candidates.
+
+Format as a table: | Module | Existing computation | Candidate G | Candidate residual | Migration difficulty |
+Then give a prioritized migration order (easiest → hardest) with reasoning.
+"""
+
+# ---------------------------------------------------------------------------
+# Pass 3 — Critique and concrete migration plan
+# ---------------------------------------------------------------------------
+PASS3_SYS = SYSTEM + """
+
+YOUR TASK: CRITIQUE AND CONCRETE MIGRATION PLAN.
+Be rigorous. Identify:
+
+A) ARCHITECTURAL CRITIQUE
+   [CRITICAL/MODERATE/MINOR] — what is wrong or incomplete in the current design?
+   Pay special attention to:
+   - The type parameter `α` in `Eigengate (α : Type)` — is it flexible enough?
+     The Laws need different α types (TrajectoryPoint, KahlerState, MaxwellField, etc.)
+     Can a single GateChain hold gates over different α? If not, how must GateChain change?
+   - The `score` function `1/(1+r)` — is this the right proximity measure for all laws?
+   - FAMM's `expNeg` — if it's a stub, what breaks?
+   - PrimeGearCache's silent cache-miss (returns Q16_16.one with no receipt) — severity?
+   - RecamanFieldStep's untested gate-reject path — what scenario does this cover?
+   - SNRAnomalyDetector's dead `dopplerDrift` branch — is it needed?
+
+B) CONCRETE MIGRATION PLAN
+   Write the exact 5-step plan to complete the paradigm migration:
+   Step 1: What to add to Semantics.lean (exact import lines)
+   Step 2: What LawRecovery.lean must contain (list each law's G, α, residual formula)
+   Step 3: Which kernels need a new `toEigengate` adapter function and what it looks like
+   Step 4: What new theorems are needed to prove the old Gate and new Eigengate are equivalent
+   Step 5: What the v0.2 build should look like when complete (job count, zero errors)
+
+C) WHAT NOT TO DO
+   Flag any tempting-but-wrong approaches that the previous agent sessions considered
+   and should be avoided.
+"""
+
+# ---------------------------------------------------------------------------
+# Main
+# ---------------------------------------------------------------------------
+def main():
+    if not API_KEY:
+        console.print("[red]Set OLLAMA_API_KEY before calling the Ollama Cloud API.[/red]")
+        sys.exit(1)
+
+    console.rule("[bold green]EigenGate Paradigm Analysis[/bold green]")
+    console.print(f"Model: [bold]{DEFAULT_MODEL}[/bold]  Fallbacks: {FALLBACK_CHAIN}\n")
+
+    console.print("[dim]Loading Lean source files and docs...[/dim]")
+    context = gather_context()
+    console.print(f"[dim]Context: {len(context):,} chars[/dim]\n")
+
+    summary   = chat(DEFAULT_MODEL, PASS1_SYS,
+                     f"Lean source files:\n\n{context}\n\nProduce the paradigm summary.",
+                     "Pass 1: Paradigm Summary")
+
+    crosslink = chat(DEFAULT_MODEL, PASS2_SYS,
+                     f"Summary from Pass 1:\n{summary}\n\n---\nLean source files:\n\n{context}\n\nDetect eigengate patterns.",
+                     "Pass 2: Cross-link Detection")
+
+    critique  = chat(DEFAULT_MODEL, PASS3_SYS,
+                     f"Summary:\n{summary}\n\nCross-links:\n{crosslink}\n\n---\nLean source files:\n\n{context}\n\nDeliver critique and migration plan.",
+                     "Pass 3: Critique + Migration Plan")
+
+    timestamp = datetime.datetime.now().strftime("%Y-%m-%d %H:%M")
+    report = f"""# EigenGate Paradigm Analysis
+*Generated: {timestamp} | Model: {DEFAULT_MODEL}*
+
+> **Context:** This analysis re-examines the HCMMR `distilled` branch through the lens
+> of the incomplete `Eigengate (α : Type)` paradigm migration. The old `Gate` struct
+> (HCMMR/Core.lean) and the new `Eigengate` (Kernel/EigenGate.lean) coexist but are
+> disconnected. This report determines what the migration requires and how to complete it.
+
+---
+
+## Pass 1 — What the EigenGate Paradigm Unifies
+
+{summary}
+
+---
+
+## Pass 2 — Where ∥G·s − s∥ Already Appears in the Codebase
+
+{crosslink}
+
+---
+
+## Pass 3 — Critique & Concrete Migration Plan
+
+{critique}
+
+---
+*Generated by `scripts/eigengate_paradigm_analysis.py`*
+"""
+
+    date_str = datetime.datetime.now().strftime("%Y-%m-%d")
+    out = RESEARCH_ROOT / "6-Documentation" / "docs" / "reports" / f"eigengate_paradigm_analysis_{date_str}.md"
+    out.parent.mkdir(parents=True, exist_ok=True)
+    out.write_text(report)
+
+    console.rule("[bold green]Complete[/bold green]")
+    console.print(f"\nReport: [bold]{out}[/bold]\n")
+    console.print(Markdown(report[:8000] + ("\n\n*[truncated — see file]*" if len(report) > 8000 else "")))
+
+if __name__ == "__main__":
+    main()