# Learnings — honest scope, boundaries, and what to reproduce

This project publishes results *with their boundaries*. These are the load-bearing
distinctions a customer, auditor, or agent should internalize before citing anything.

## Proven vs. empirical vs. scaffold

There are three very different kinds of evidence here — don't conflate them:

1. **Formally proven** — a predicate machine-checked in a kernel (Coq `coqchk`, Lean
   `#print axioms`, Verus). Strongest, but scoped to *what the predicate says*, which is
   often a model, not the shipping code.
2. **Empirically measured** — a number computed from real data (e.g. the agentic-waste
   figures). Reproducible, but scoped to the dataset it was measured on.
3. **Scaffold / mapping** — compiling code that *structures* an obligation (e.g. the EU AI
   Act Annex IV generator) but carries placeholder values until populated.

Most overstatement comes from treating (3) as (1), or (2)-on-one-dataset as universal.

## The four claims and exactly how far they go

- **Triple-kernel proof corpus** — a **mixed snapshot**: closed proofs *and*
  statement-form/stub material coexist. It is **not** a blanket zero-axiom / proof-closure
  certificate. The specs are checked **standalone** (0/… Verus specs import the runtime
  crates), so the corpus does not, in general, formally verify the shipping Rust; binding is
  by CUB-ID cross-reference + behavioral tests + a growing set of in-crate `verus!` blocks.
- **TEP FAR=0** — a **calibration identity**, not held-out detection: the threshold is set
  to 1.5× the fault-free-baseline peak, so FAR=0 holds *by construction* on that set. The
  100/100/100 FDR is **in-sample** on the Braatz/Rieth d00/d03/d09/d15 data. Held-out
  transfer to unseen fault-free data has **not** been established. Honest negative result:
  the plain `--use-braatz-baseline` path underperforms PCA-T² on the canonical trio; the
  peak requires the search layout + the CUSUM OR-gate.
- **Agentic waste** — **re-measured** from committed traces, not a prior memory dossier:
  66.85% blast radius, 51.76% VRAM locked, ~99.47% output<input **scoped to Azure-2024**
  (44.1M of the ~45.3M analyzed rows). Only the 66.85% figure appears in a whitepaper; the
  rest are backed by the JSON result files + the evidence pack.
- **EU AI Act** — a compiling **scaffold**: per-article evidence structs + AnnexIvBuilder +
  a generator, with placeholder values (e.g. example.com kill-switch URL). High-risk
  conformity additionally needs a notified-body assessment (Annex VII); classification is
  Annex III (biometric/PUF device identity), and the CRA classifies it Annex IV (critical).

## Reproducibility model (what's public vs. gated)

- **Public data reproduction:** the agentic-waste result JSONs, the proof-corpus ZIP, the
  TEP dataset pack, and the whitepaper are all public downloads on
  <https://lib.trustfortress.ai>; the reproduce commands re-derive the numbers with no repo
  access. The `cubie-tep` and `cubie-eu-*` **source packs** are also published so the
  detector and EU crates can be read/audited.
- **Source-level build** needs the workspace (the crates depend on `cubie-core`), so a
  zero-repo `cargo run` of the full pipeline is not possible from a single crate pack.
- **Deeper internals** (hot-path engineering constants, patent-detailed mechanics, partner-
  confidential Intel material) are **not public** — by design.

## Engineering learnings worth stating

- **Three independent proof kernels beat one.** Coq, Lean, and Verus have separate trust
  bases; a soundness bug that slips one is unlikely to slip all three. The discipline that
  matters is *parity* (same CUB-ID across all three), not raw theorem counts.
- **Standalone specs are not runtime verification.** A `verus/*.rs` spec can pass while the
  real function is broken. To actually bind a proof to shipping code you must annotate the
  real exec function in place (`verus! { ensures … }`), not restate it in a separate file.
- **Explainable denials need distance, not just a flag.** Allow/deny codes are separated by
  a large Hamming distance so a few flipped bits can't turn a DENY into an ALLOW.
- **Numbers quantifying a moving repo go stale.** Don't cite prose counts (theorems, tests,
  CUB IDs); re-measure with the live tooling before publishing any external artifact.
- **Publish the boundary with the number.** "100/100/100" without "in-sample calibration
  identity" is misleading; the caveat is part of the claim.

## How to reproduce (pointers)

- **Claims:** each claim page at <https://lib.trustfortress.ai/claims/<id>> has pinned
  evidence + copy-paste reproduce commands.
- **Agentic waste:** download the 4 result JSONs, `sha256sum`, and re-derive 66.85% /
  51.76% / 99.47% — see `.../claims/agentic-waste`.
- **TEP:** build `cubie-tep`, run the detector over the d00/d03/d09/d15 CSVs — see
  `.../claims/tep-far0` and `docs/audit/empirical_peak.md`.
- **Proofs:** verify a closed file with `coqchk` / `#print axioms` / `verus --crate-type lib`
  on the published corpus ZIP — see `.../claims/proof-corpus`.