CUBIE TEP DETECTOR - LIVE DEMO  (v2)
====================================

WHAT THE AUDIENCE SEES
----------------------
  STEP 0   Environment check + auto-stages TEP CSV data if missing
  STEP 1   Build cubie-tep::tep_layout_search (cargo --release)
  STEP 2a  ONE verbose run with FULL stdout: iter-by-iter swap traces showing
           FAR / IDV-3 / IDV-9 / IDV-15 / score / accept-reject, then
           *** GOAL REACHED at iter NN *** when it finds the saturation peak.
           This is the part where the audience SEES the algorithm crunching.
  STEP 2b  Full 60-run sweep (20 seeds x 3 algorithms x 1000 iters),
           one color-coded Best: line per run, live running tally.
           Each line shows: seed, algo, FAR, IDV-3, IDV-9, IDV-15, score,
           and iter@goal (how many iterations the search needed to saturate).
  STEP 3   Independent JSON re-grep: re-reads the 60 just-written output files
           and confirms FAR=0 + all-3-IDVs at 100%. Shows a sample JSON dump.
  STEP 4   Triple-kernel formal verification (27 CUBs x 3 = 81 proofs)
           First shows a snippet of CUB-1952 spec so the audience sees real
           proof code, then runs Verus + Lean + Coq with progress dots.
  STEP 5   Rust runtime tests (CUB-1940 Layer-1 input validation)
           Shows the actual validate() function from cubie-core, then runs
           the 10 unit tests live.
  STEP 6   Mic-drop summary

HOW TO RUN
----------
  1. Double-click Cubie_TEP_Demo.bat
     (or right-click Cubie_TEP_Demo.ps1 -> "Run with PowerShell")
  2. Press any key at each pause to advance.

WALLTIME
--------
  ~3 minutes   default: skip Coq Docker, runs Verus + Lean
  ~6 minutes   full: includes Coq via Docker (pulls coqorg/coq:8.18 first run)
  ~90 seconds  fast: $env:SKIP_KERNELS = "1"  (sweep + Rust only)

REQUIREMENTS
------------
  Always:        PowerShell 5.1+, Rust 1.95+ (cargo), the cubie-tf repo cloned
  Step 0 data:   TEP CSVs (d00/d03/d09/d15_test.csv) - script auto-copies them
                 from $env:DATA_DONOR (default: C:\Users\NickV\cubie-math\data\tep)
                 if absent. If donor missing, get them from:
                 https://github.com/camaramm/tennessee-eastman-profBraatz
  Step 4 Verus:  verus.exe binary  (set $env:VERUS_BIN if not at default)
  Step 4 Lean:   lean on PATH       (install: elan default leanprover/lean4:v4.10.0)
                 Note: 1 of 27 specs (CUB-1952) requires Mathlib and is
                 verified in CI via lakefile, not locally. The demo
                 correctly marks that one as "M" (Mathlib-required).
  Step 4 Coq:    docker on PATH     (pulls coqorg/coq:8.18 first run)

  Default repo:  C:\Users\NickV\cubie-tf-completion
  Override:      $env:REPO_DIR = "D:\path\to\cubie-tf"

ENV VAR OVERRIDES
-----------------
  $env:REPO_DIR        Path to the cubie-tf repo
  $env:DATA_DONOR      Path to dir containing d00_test.csv etc. for auto-staging
  $env:VERUS_BIN       Full path to verus.exe
  $env:SKIP_KERNELS    "1" to skip Verus/Lean/Coq (faster demo)
  $env:QUIET_RUN1      "1" to suppress the Step 2a verbose first-run trace
  $env:NO_PAUSE        "1" for unattended end-to-end run

PUNCHLINE
---------
  * 60 / 60 search runs reach saturation peak (live, just-now)
  * Audience SEES the iter-by-iter swap traces + GOAL REACHED + Best lines
  * 81 / 81 formal proofs check across Verus + Coq + Lean
  * 10 / 10 Rust runtime unit tests pass
  * FAR=0 is a CALIBRATION IDENTITY (CUB-1921), not a stochastic bound

WHAT CHANGED FROM v1
--------------------
  v1 silenced binary output (2>&1 | Out-Null), so the audience never saw the
  algorithm crunch numbers. v2 captures binary stdout and prints a parsed
  one-liner per run AND shows the full verbose trace for run #1.
  v1 also assumed TEP CSVs were present; v2 auto-stages them.

PROVENANCE
----------
  Whitepaper:   docs\whitepaper\cubie_tep_whitepaper.pdf
  Exec summary: docs\whitepaper\EXECUTIVE_SUMMARY_2026-05-27.md
  Evidence:     docs\whitepaper\evidence-pack\
  Repo:         github.com/iamdatanick/cubie-tf
