feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems

- 24/24 processed, 0 errors (12 verified, 12 failed)
- Average 2.0 steps per proof (max 5 steps)
- 11 tactic families detected
- Verified proofs: avg gap=2.50 vs Failed: avg gap=1.50
- proof_traces/*.trace.json + *.decomp.json stored per theorem

4-Infrastructure/shim/pist_trace_decompose.py

@@ -269,6 +269,7 @@ def main():
             json.dump(result, f, indent=2)
         print(f"\nDecomposition: {out_path}", flush=True)
     
+    print(json.dumps(result))
     return 0
 
 

4-Infrastructure/shim/run_trace_canary.py

@@ -0,0 +1,132 @@
+#!/usr/bin/env python3
+"""Multi-tactic canary batch for Tier 2 trace pipeline."""
+import json
+import os
+import sys
+import time
+import subprocess
+from pathlib import Path
+from collections import Counter
+
+from trace_canary_theorems import CANARY_THEOREMS
+
+TRACES_DIR = os.path.join(os.path.dirname(__file__), "../..", "shared-data/proof_traces")
+VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_canary_vectors.jsonl")
+REPORT_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_canary_report.json")
+BRIDGE = os.path.join(os.path.dirname(__file__), "lean_trace_bridge.py")
+DECOMPOSE = os.path.join(os.path.dirname(__file__), "pist_trace_decompose.py")
+
+PROOF_SERVER_TOKEN = os.environ.get("PROOF_SERVER_TOKEN", "")
+if not PROOF_SERVER_TOKEN:
+    tf = os.environ.get("PROOF_SERVER_TOKEN_FILE", os.path.expanduser("~/.config/ene/language-proof-server.token"))
+    try:
+        PROOF_SERVER_TOKEN = Path(tf).read_text().strip()
+    except (FileNotFoundError, OSError):
+        PROOF_SERVER_TOKEN = ""
+
+
+def run_pipeline(theorem: dict) -> dict:
+    name = theorem["name"]
+    code = theorem["code"]
+    trace_path = os.path.join(TRACES_DIR, f"canary_{name}.trace.json")
+    decomp_path = os.path.join(TRACES_DIR, f"canary_{name}.decomp.json")
+    os.makedirs(TRACES_DIR, exist_ok=True)
+
+    t0 = time.time()
+    r1 = subprocess.run(
+        [sys.executable, BRIDGE, "--code", code, "--name", name, "--out", trace_path],
+        capture_output=True, text=True, timeout=120,
+        env={**os.environ, "PROOF_SERVER_TOKEN": PROOF_SERVER_TOKEN},
+    )
+    if r1.returncode != 0:
+        return {"error": f"bridge: {r1.stderr[:200]}", "name": name}
+
+    r2 = subprocess.run(
+        [sys.executable, DECOMPOSE, trace_path, "--out", decomp_path],
+        capture_output=True, text=True, timeout=30,
+    )
+    if r2.returncode != 0 or not os.path.exists(decomp_path):
+        return {"error": f"decomp: {r2.stderr[:200]}", "name": name}
+
+    with open(decomp_path) as f:
+        decomposition = json.load(f)
+
+    return {"name": name, "trace_file": trace_path, "wall_s": round(time.time() - t0, 2),
+            "decomposition": decomposition}
+
+
+def report(results, errors):
+    good = [r for r in results if "error" not in r]
+    n = len(good)
+    print(f"\n{'='*60}\nTIER 2 TRACE CANARY REPORT\n{'='*60}", flush=True)
+    print(f"Total: {len(results)} ({n} ok, {len(errors)} errors)", flush=True)
+
+    steps = [len(r["decomposition"].get("flexure_joints", [])) for r in good]
+    if steps:
+        print(f"Steps: mean={sum(steps)/len(steps):.1f} max={max(steps)} min={min(steps)}", flush=True)
+    statuses = Counter(r["decomposition"]["trace_summary"]["status"] for r in good)
+    print(f"Status: {dict(statuses)}", flush=True)
+
+    families = Counter()
+    for r in good:
+        for f, c in r["decomposition"].get("tactic_family_distribution", {}).items():
+            families[f] += c
+    print(f"Families: {dict(families)}", flush=True)
+
+    u_mat = len(set(r["decomposition"]["spectral"]["n_states"] for r in good))
+    u_rank = len(set(r["decomposition"]["spectral"]["rank_estimate"] for r in good))
+    u_gap = len(set(round(r["decomposition"]["spectral"]["spectral_gap"], 4) for r in good))
+    print(f"Unique states: {u_mat}/{n}  ranks: {u_rank}  gaps: {u_gap}/{n}", flush=True)
+
+    v_gaps = [r for r in good if r["decomposition"]["trace_summary"]["status"] == "verified"]
+    f_gaps = [r for r in good if r["decomposition"]["trace_summary"]["status"] == "failed"]
+    for label, group in [("verified", v_gaps), ("failed", f_gaps)]:
+        if group:
+            gaps = [r["decomposition"]["spectral"]["spectral_gap"] for r in group]
+            print(f"{label} (n={len(group)}): gap={sum(gaps)/len(gaps):.4f} [{min(gaps):.4f},{max(gaps):.4f}]", flush=True)
+
+    with open(VECTORS_PATH, "w") as f:
+        for r in good:
+            row = {
+                "name": r["name"], "status": r["decomposition"]["trace_summary"]["status"],
+                "n_steps": len(r["decomposition"].get("flexure_joints", [])),
+                "n_states": r["decomposition"]["spectral"]["n_states"],
+                "spectral_gap": r["decomposition"]["spectral"]["spectral_gap"],
+                "rank_estimate": r["decomposition"]["spectral"]["rank_estimate"],
+                "density": r["decomposition"]["spectral"]["density"],
+                "feature_vector": r["decomposition"]["feature_vector"],
+                "tactic_family_distribution": r["decomposition"]["tactic_family_distribution"],
+            }
+            f.write(json.dumps(row) + "\n")
+    print(f"Vectors: {VECTORS_PATH}", flush=True)
+
+    with open(REPORT_PATH, "w") as f:
+        json.dump({"n": n, "n_errors": len(errors), "status_distribution": dict(statuses),
+                    "tactic_family_distribution": dict(families),
+                    "unique_spectral_gaps": u_gap, "unique_rank_estimates": u_rank}, f, indent=2)
+    print(f"Report: {REPORT_PATH}", flush=True)
+
+
+def main():
+    theorems = CANARY_THEOREMS
+    print(f"Trace canary: {len(theorems)} theorems\n", flush=True)
+    results, errors = [], []
+    for i, theorem in enumerate(theorems):
+        name = theorem["name"]
+        print(f"  [{i+1}/{len(theorems)}] {name:30s} ... ", end="", flush=True)
+        r = run_pipeline(theorem)
+        if "error" in r:
+            print(f"ERROR: {r['error'][:60]}", flush=True)
+            errors.append(r)
+        else:
+            st = r["decomposition"]["trace_summary"]["status"]
+            ns = len(r["decomposition"].get("flexure_joints", []))
+            gap = r["decomposition"]["spectral"]["spectral_gap"]
+            print(f"{st:10s} steps={ns:2d} gap={gap:.4f} rank={r['decomposition']['spectral']['rank_estimate']}", flush=True)
+            results.append(r)
+    report(results, errors)
+    return 0 if len(errors) < len(theorems) / 2 else 1
+
+
+if __name__ == "__main__":
+    main()

4-Infrastructure/shim/trace_canary_theorems.py

@@ -0,0 +1,157 @@
+CANARY_THEOREMS = [
+    # ── 1. rewrite chains (each step necessary) ──
+    {
+        "name": "rw_chain_eq",
+        "code": 'theorem rw_chain_eq (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by\n  rw [h1]\n  rw [h2]',
+        "domain": "equality", "proof_method": "rewrite", "joint": "equality_chaining_2step",
+        "obstruction": None, "rrc_shape": "CadForceProbeReceipt",
+    },
+    {
+        "name": "rw_chain_mixed",
+        "code": 'theorem rw_chain_mixed (a b : Nat) (h : a = b) : a + 0 = b := by\n  rw [h]\n  simp',
+        "domain": "arithmetic", "proof_method": "rewrite", "joint": "rw_then_simp",
+        "obstruction": None, "rrc_shape": "CadForceProbeReceipt",
+    },
+    {
+        "name": "rw_chain_3step",
+        "code": 'theorem rw_chain_3step (a b c d : Nat) (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by\n  rw [h1]\n  rw [h2]\n  rw [h3]',
+        "domain": "equality", "proof_method": "rewrite", "joint": "equality_chaining_3step",
+        "obstruction": None, "rrc_shape": "CadForceProbeReceipt",
+    },
+    {
+        "name": "rw_then_omega",
+        "code": 'theorem rw_then_omega (a b c : Nat) (h : a = b + c) : a * 2 = (b + c) * 2 := by\n  rw [h]\n  omega',
+        "domain": "arithmetic", "proof_method": "rewrite", "joint": "rw_then_arithmetic",
+        "obstruction": None, "rrc_shape": "CadForceProbeReceipt",
+    },
+
+    # ── 2. case analysis chains ──
+    {
+        "name": "cases_or_swap",
+        "code": 'theorem cases_or_swap (A B : Prop) (h : A ∨ B) : B ∨ A := by\n  cases h\n  · right; exact h\n  · left; exact h',
+        "domain": "logic", "proof_method": "cases", "joint": "disjunction_swap",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "cases_and_elim",
+        "code": 'theorem cases_and_elim (A B C : Prop) (h : A ∧ B) (h2 : A → C) : C := by\n  cases h\n  apply h2\n  assumption',
+        "domain": "logic", "proof_method": "cases", "joint": "conjunction_elim_then_apply",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "constructor_example",
+        "code": 'theorem constructor_example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by\n  constructor\n  · exact hA\n  · exact hB',
+        "domain": "logic", "proof_method": "constructor", "joint": "conjunction_intro",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "apply_chain",
+        "code": 'theorem apply_chain (A B C : Prop) (h1 : A → B) (h2 : B → C) (hA : A) : C := by\n  apply h2\n  apply h1\n  exact hA',
+        "domain": "logic", "proof_method": "apply", "joint": "implication_chaining",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+
+    # ── 3. omega with multiple constraints ──
+    {
+        "name": "omega_chain_ineq",
+        "code": 'theorem omega_chain_ineq (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by\n  omega',
+        "domain": "order", "proof_method": "omega", "joint": "transitivity_closure",
+        "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler",
+    },
+    {
+        "name": "omega_reorder_sum",
+        "code": 'theorem omega_reorder_sum (a b c : Nat) : a + b + c = a + c + b := by\n  omega',
+        "domain": "arithmetic", "proof_method": "omega", "joint": "reorder_summands",
+        "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler",
+    },
+    {
+        "name": "omega_distrib",
+        "code": 'theorem omega_distrib (a b c : Nat) : a * (b + c) = a * b + a * c := by\n  omega',
+        "domain": "algebra", "proof_method": "omega", "joint": "distributivity",
+        "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler",
+    },
+    {
+        "name": "omega_chain_unsat",
+        "code": 'theorem omega_chain_unsat (x : Nat) : x < x := by\n  omega',
+        "domain": "order", "proof_method": "omega", "joint": "unsatisfiable_linear",
+        "obstruction": "unsatisfiable_goal", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape",
+    },
+
+    # ── 4. induction chains ──
+    {
+        "name": "induct_add_zero",
+        "code": 'theorem induct_add_zero (n : Nat) : n + 0 = n := by\n  induction n with\n  | zero => simp\n  | succ n ih => simp [add_succ, ih]',
+        "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_proof",
+        "obstruction": None, "rrc_shape": "ProjectableGeometryTopology",
+    },
+    {
+        "name": "induct_add_succ",
+        "code": 'theorem induct_add_succ (n m : Nat) : n + m.succ = (n + m).succ := by\n  induction n with\n  | zero => simp\n  | succ k ih => simp [add_succ, ih]',
+        "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_succ",
+        "obstruction": None, "rrc_shape": "ProjectableGeometryTopology",
+    },
+    {
+        "name": "induct_mul_zero",
+        "code": 'theorem induct_mul_zero (n : Nat) : n * 0 = 0 := by\n  induction n with\n  | zero => simp\n  | succ k ih => simp [mul_add, add_comm, ih]',
+        "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_mul",
+        "obstruction": None, "rrc_shape": "ProjectableGeometryTopology",
+    },
+    {
+        "name": "induct_factorial",
+        "code": 'def fac : Nat → Nat\n  | 0 => 1\n  | n+1 => fac n * (n+1)\ntheorem induct_fact (n : Nat) : fac 0 = 1 := by\n  simp [fac]',
+        "domain": "arithmetic", "proof_method": "simp", "joint": "definitional_unfold",
+        "obstruction": None, "rrc_shape": "CognitiveLoadField",
+    },
+
+    # ── 5. intro + apply chains ──
+    {
+        "name": "intro_all",
+        "code": 'theorem intro_all (A B C : Prop) : A → B → C → A := by\n  intro hA\n  intro hB\n  intro hC\n  exact hA',
+        "domain": "logic", "proof_method": "intro", "joint": "multiple_introductions",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "intro_apply",
+        "code": 'theorem intro_apply (A B : Prop) : (A → B) → A → B := by\n  intro h\n  intro hA\n  apply h\n  exact hA',
+        "domain": "logic", "proof_method": "apply", "joint": "intro_then_apply",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "have_chain",
+        "code": 'theorem have_chain (A B C : Prop) (hAB : A → B) (hBC : B → C) (hA : A) : C := by\n  have hB : B := hAB hA\n  have hC : C := hBC hB\n  exact hC',
+        "domain": "logic", "proof_method": "have", "joint": "lemma_chaining",
+        "obstruction": None, "rrc_shape": "LogogramProjection",
+    },
+    {
+        "name": "calc_chain",
+        "code": 'theorem calc_chain (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by\n  ring\n  omega',
+        "domain": "algebra", "proof_method": "ring", "joint": "ring_then_omega",
+        "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler",
+    },
+
+    # ── 6. failure cases ──
+    {
+        "name": "fail_type_mismatch",
+        "code": 'theorem fail_type_mismatch (n : Nat) : n = (\"hello\" : String) := by\n  rfl',
+        "domain": "type_error", "proof_method": "rfl", "joint": "type_mismatch",
+        "obstruction": "type_mismatch", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape",
+    },
+    {
+        "name": "fail_missing_lemma",
+        "code": 'theorem fail_missing_lemma (n : Nat) : n = n + 0 := by\n  rw [imaginary_lemma]',
+        "domain": "arithmetic", "proof_method": "rewrite", "joint": "missing_dependency",
+        "obstruction": "missing_lemma", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape",
+    },
+    {
+        "name": "fail_unsat",
+        "code": 'theorem fail_unsat (x : Nat) (h : x > 0) : x = 0 := by\n  omega',
+        "domain": "order", "proof_method": "omega", "joint": "contradictory_goal",
+        "obstruction": "unsatisfiable_goal", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape",
+    },
+    {
+        "name": "fail_bad_coercion",
+        "code": 'theorem fail_bad_coercion (n : Float) : (n : Nat) = (n : Int) := by\n  rfl',
+        "domain": "type_error", "proof_method": "rfl", "joint": "coercion_mismatch",
+        "obstruction": "type_mismatch", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape",
+    },
+]

shared-data/pist_trace_canary_report.json

@@ -0,0 +1,23 @@
+{
+  "n": 24,
+  "n_errors": 0,
+  "status_distribution": {
+    "verified": 12,
+    "failed": 12
+  },
+  "tactic_family_distribution": {
+    "rewrite": 8,
+    "normalization": 5,
+    "arithmetic": 7,
+    "case_analysis": 2,
+    "unknown": 3,
+    "discharge": 12,
+    "constructor": 1,
+    "introduction": 5,
+    "lemma_introduction": 2,
+    "algebraic": 1,
+    "reflexivity": 2
+  },
+  "unique_spectral_gaps": 5,
+  "unique_rank_estimates": 1
+}

shared-data/pist_trace_canary_vectors.jsonl

@@ -0,0 +1,24 @@
+{"name": "rw_chain_eq", "status": "verified", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.5, 2524], "tactic_family_distribution": {"rewrite": 2}}
+{"name": "rw_chain_mixed", "status": "verified", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.5, 2194], "tactic_family_distribution": {"rewrite": 1, "normalization": 1}}
+{"name": "rw_chain_3step", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.3333333333333333, 3279], "tactic_family_distribution": {"rewrite": 3}}
+{"name": "rw_then_omega", "status": "failed", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.5, 2137], "tactic_family_distribution": {"rewrite": 1, "arithmetic": 1}}
+{"name": "cases_or_swap", "status": "failed", "n_steps": 5, "n_states": 1, "spectral_gap": 5.0, "rank_estimate": 1, "density": 5.0, "feature_vector": [5, 1, 5.0, 5.0, 0, 1, 0.0, 0.0, 0.0, 1.5219, 0.0, 5552], "tactic_family_distribution": {"case_analysis": 1, "unknown": 2, "discharge": 2}}
+{"name": "cases_and_elim", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 1.585, 0.3333333333333333, 3345], "tactic_family_distribution": {"case_analysis": 1, "discharge": 1, "unknown": 1}}
+{"name": "constructor_example", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 0.9183, 0.3333333333333333, 3311], "tactic_family_distribution": {"constructor": 1, "discharge": 2}}
+{"name": "apply_chain", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.3333333333333333, 3548], "tactic_family_distribution": {"discharge": 3}}
+{"name": "omega_chain_ineq", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1082], "tactic_family_distribution": {"arithmetic": 1}}
+{"name": "omega_reorder_sum", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1056], "tactic_family_distribution": {"arithmetic": 1}}
+{"name": "omega_distrib", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1071], "tactic_family_distribution": {"arithmetic": 1}}
+{"name": "omega_chain_unsat", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1141], "tactic_family_distribution": {"arithmetic": 1}}
+{"name": "induct_add_zero", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1042], "tactic_family_distribution": {"normalization": 1}}
+{"name": "induct_add_succ", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1076], "tactic_family_distribution": {"normalization": 1}}
+{"name": "induct_mul_zero", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1076], "tactic_family_distribution": {"normalization": 1}}
+{"name": "induct_factorial", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1061], "tactic_family_distribution": {"normalization": 1}}
+{"name": "intro_all", "status": "verified", "n_steps": 4, "n_states": 1, "spectral_gap": 4.0, "rank_estimate": 1, "density": 4.0, "feature_vector": [4, 1, 4.0, 4.0, 0, 1, 0.0, 0.0, 0.0, 0.8113, 0.25, 4316], "tactic_family_distribution": {"introduction": 3, "discharge": 1}}
+{"name": "intro_apply", "status": "verified", "n_steps": 4, "n_states": 1, "spectral_gap": 4.0, "rank_estimate": 1, "density": 4.0, "feature_vector": [4, 1, 4.0, 4.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.25, 4532], "tactic_family_distribution": {"introduction": 2, "discharge": 2}}
+{"name": "have_chain", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 0.9183, 0.3333333333333333, 3427], "tactic_family_distribution": {"lemma_introduction": 2, "discharge": 1}}
+{"name": "calc_chain", "status": "failed", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.0, 2270], "tactic_family_distribution": {"algebraic": 1, "arithmetic": 1}}
+{"name": "fail_type_mismatch", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1170], "tactic_family_distribution": {"reflexivity": 1}}
+{"name": "fail_missing_lemma", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1198], "tactic_family_distribution": {"rewrite": 1}}
+{"name": "fail_unsat", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1112], "tactic_family_distribution": {"arithmetic": 1}}
+{"name": "fail_bad_coercion", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1108], "tactic_family_distribution": {"reflexivity": 1}}

shared-data/proof_traces/canary_apply_chain.decomp.json

@@ -0,0 +1,95 @@
+{
+  "trace_summary": {
+    "theorem_name": "apply_chain",
+    "status": "verified",
+    "n_steps": 3,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 3
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 3.0,
+    "spectral_gap": 3.0,
+    "laplacian_eigenvalue_max": 3.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 3.0,
+    "trace": 3,
+    "density": 3.0
+  },
+  "feature_vector": [
+    3,
+    1,
+    3.0,
+    3.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.3333333333333333,
+    3548
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "discharge": 3
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "apply h2",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "apply h1",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_apply_chain.trace.json

@@ -0,0 +1,122 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "ea1cebff0a2f62a9dc7d1cc85661f9c790c7ae51895a98436d7811135006f54f",
+  "theorem_name": "apply_chain",
+  "status": "verified",
+  "tactic_count": 3,
+  "total_elapsed_ms": 3548,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "apply h2",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1263,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "apply h1",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1199,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "exact hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1086,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      3
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "apply h2",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "apply h1",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_calc_chain.decomp.json

@@ -0,0 +1,84 @@
+{
+  "trace_summary": {
+    "theorem_name": "calc_chain",
+    "status": "failed",
+    "n_steps": 2,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 2
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 2.0,
+    "spectral_gap": 2.0,
+    "laplacian_eigenvalue_max": 2.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 2.0,
+    "trace": 2,
+    "density": 2.0
+  },
+  "feature_vector": [
+    2,
+    1,
+    2.0,
+    2.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.0,
+    0.0,
+    2270
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "algebraic": 1,
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "ring",
+      "tactic_family": "algebraic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_calc_chain.trace.json

@@ -0,0 +1,87 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "ffc91916d335aac079945c103d27ef03412d0a551b8c8b7e11d5195fe925c39b",
+  "theorem_name": "calc_chain",
+  "status": "failed",
+  "tactic_count": 2,
+  "total_elapsed_ms": 2270,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "ring",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1104,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1166,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      2
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "ring",
+      "tactic_family": "algebraic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_cases_and_elim.decomp.json

@@ -0,0 +1,97 @@
+{
+  "trace_summary": {
+    "theorem_name": "cases_and_elim",
+    "status": "verified",
+    "n_steps": 3,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 3
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 3.0,
+    "spectral_gap": 3.0,
+    "laplacian_eigenvalue_max": 3.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 3.0,
+    "trace": 3,
+    "density": 3.0
+  },
+  "feature_vector": [
+    3,
+    1,
+    3.0,
+    3.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.585,
+    0.3333333333333333,
+    3345
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "case_analysis": 1,
+    "discharge": 1,
+    "unknown": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "tactic_family": "case_analysis",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "apply h2",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "assumption",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_cases_and_elim.trace.json

@@ -0,0 +1,122 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "b9e3ed9d2456aff7773a8aa63c814a443e4fd9ace06630c76776b25ba0885d37",
+  "theorem_name": "cases_and_elim",
+  "status": "verified",
+  "tactic_count": 3,
+  "total_elapsed_ms": 3345,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1072,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "apply h2",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1148,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "assumption",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1125,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      3
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "tactic_family": "case_analysis",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "apply h2",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "assumption",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_cases_or_swap.decomp.json

@@ -0,0 +1,121 @@
+{
+  "trace_summary": {
+    "theorem_name": "cases_or_swap",
+    "status": "failed",
+    "n_steps": 5,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 5
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 5.0,
+    "spectral_gap": 5.0,
+    "laplacian_eigenvalue_max": 5.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 5.0,
+    "trace": 5,
+    "density": 5.0
+  },
+  "feature_vector": [
+    5,
+    1,
+    5.0,
+    5.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.5219,
+    0.0,
+    5552
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "case_analysis": 1,
+    "unknown": 2,
+    "discharge": 2
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "tactic_family": "case_analysis",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 right",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "\u00b7 left",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 4,
+      "tactic": "exact h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_cases_or_swap.trace.json

@@ -0,0 +1,192 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "a5d1516151f774e41626c35fdc80c48b283ebce812be3114261e2a0022ee7f34",
+  "theorem_name": "cases_or_swap",
+  "status": "failed",
+  "tactic_count": 5,
+  "total_elapsed_ms": 5552,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1138,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 right",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1140,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "exact h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1115,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 3,
+      "tactic": "\u00b7 left",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1106,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 4,
+      "tactic": "exact h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1053,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      5
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "cases h",
+      "tactic_family": "case_analysis",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 right",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "\u00b7 left",
+      "tactic_family": "unknown",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 4,
+      "tactic": "exact h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_constructor_example.decomp.json

@@ -0,0 +1,96 @@
+{
+  "trace_summary": {
+    "theorem_name": "constructor_example",
+    "status": "verified",
+    "n_steps": 3,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 3
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 3.0,
+    "spectral_gap": 3.0,
+    "laplacian_eigenvalue_max": 3.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 3.0,
+    "trace": 3,
+    "density": 3.0
+  },
+  "feature_vector": [
+    3,
+    1,
+    3.0,
+    3.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    0.9183,
+    0.3333333333333333,
+    3311
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "constructor": 1,
+    "discharge": 2
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "constructor",
+      "tactic_family": "constructor",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "\u00b7 exact hB",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_constructor_example.trace.json

@@ -0,0 +1,122 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "2eb590d2a9b457143e96ac5f046833f24ab5f93ff05ae6944cce0b81ddf6740e",
+  "theorem_name": "constructor_example",
+  "status": "verified",
+  "tactic_count": 3,
+  "total_elapsed_ms": 3311,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "constructor",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1096,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 exact hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1107,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "\u00b7 exact hB",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1108,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      3
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "constructor",
+      "tactic_family": "constructor",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "\u00b7 exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "\u00b7 exact hB",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_bad_coercion.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "fail_bad_coercion",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1108
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "reflexivity": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "tactic_family": "reflexivity",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_bad_coercion.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "0361d21827da4cd215292e606e203e24b1d862d7fc08075d6cae898b04824cc7",
+  "theorem_name": "fail_bad_coercion",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1108,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1108,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "tactic_family": "reflexivity",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_missing_lemma.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "fail_missing_lemma",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1198
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "rewrite": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [imaginary_lemma]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_missing_lemma.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "695a8dc0a0b929b09b6f795eaebb82982558d7e6da2addd6d88472a26ed7bf0f",
+  "theorem_name": "fail_missing_lemma",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1198,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rw [imaginary_lemma]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1198,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [imaginary_lemma]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_type_mismatch.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "fail_type_mismatch",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1170
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "reflexivity": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "tactic_family": "reflexivity",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_type_mismatch.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "0f481ab618a4e39cd28480436a43bf0dcf541fa62801d3e58588d66f355f54c6",
+  "theorem_name": "fail_type_mismatch",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1170,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1170,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rfl",
+      "tactic_family": "reflexivity",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_unsat.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "fail_unsat",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1112
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_fail_unsat.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "ea07e0d3bd2e3d976b55b4cf94201957550a8733b53e3f84725d2d67b46d4cfc",
+  "theorem_name": "fail_unsat",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1112,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1112,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_have_chain.decomp.json

@@ -0,0 +1,96 @@
+{
+  "trace_summary": {
+    "theorem_name": "have_chain",
+    "status": "verified",
+    "n_steps": 3,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 3
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 3.0,
+    "spectral_gap": 3.0,
+    "laplacian_eigenvalue_max": 3.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 3.0,
+    "trace": 3,
+    "density": 3.0
+  },
+  "feature_vector": [
+    3,
+    1,
+    3.0,
+    3.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    0.9183,
+    0.3333333333333333,
+    3427
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "lemma_introduction": 2,
+    "discharge": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "have hB : B := hAB hA",
+      "tactic_family": "lemma_introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "have hC : C := hBC hB",
+      "tactic_family": "lemma_introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact hC",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_have_chain.trace.json

@@ -0,0 +1,122 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "555b7633b2fe1f0fd58e666ef2d03da6f4f7ac5b6be0eefbe32dcf7af342eae3",
+  "theorem_name": "have_chain",
+  "status": "verified",
+  "tactic_count": 3,
+  "total_elapsed_ms": 3427,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "have hB : B := hAB hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1113,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "have hC : C := hBC hB",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1214,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "exact hC",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1100,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      3
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "have hB : B := hAB hA",
+      "tactic_family": "lemma_introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "have hC : C := hBC hB",
+      "tactic_family": "lemma_introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "exact hC",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_add_succ.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "induct_add_succ",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1076
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "normalization": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_add_succ.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "198197fa574402142bbac958dc8944df994bd2c010f5b163adc6567ba7e849df",
+  "theorem_name": "induct_add_succ",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1076,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1076,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_add_zero.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "induct_add_zero",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1042
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "normalization": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_add_zero.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "58308f000c8cf3b7a19c12f46a40a8b8822f5f84a5860e100bf5d93bac55ad16",
+  "theorem_name": "induct_add_zero",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1042,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1042,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_factorial.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "induct_factorial",
+    "status": "verified",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    1.0,
+    1061
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "normalization": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "simp [fac]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_factorial.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "16f00e21118bd73911fcb21b83283770989bdafebd84f2ab69243ffefb66fe66",
+  "theorem_name": "induct_factorial",
+  "status": "verified",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1061,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "simp [fac]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1061,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "simp [fac]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_mul_zero.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "induct_mul_zero",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1076
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "normalization": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_induct_mul_zero.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "aaf9644978fbd40566dc96f63d1cf70c7086d5eaedaeb70fdb348ee3228a430e",
+  "theorem_name": "induct_mul_zero",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1076,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1076,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_intro_all.decomp.json

@@ -0,0 +1,108 @@
+{
+  "trace_summary": {
+    "theorem_name": "intro_all",
+    "status": "verified",
+    "n_steps": 4,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 4
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 4.0,
+    "spectral_gap": 4.0,
+    "laplacian_eigenvalue_max": 4.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 4.0,
+    "trace": 4,
+    "density": 4.0
+  },
+  "feature_vector": [
+    4,
+    1,
+    4.0,
+    4.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    0.8113,
+    0.25,
+    4316
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "introduction": 3,
+    "discharge": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "intro hA",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "intro hB",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "intro hC",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_intro_all.trace.json

@@ -0,0 +1,157 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "6cd826b82467f96a11c9c1730a2b5b7c71d8caa4b34805110a2b51c99c00651c",
+  "theorem_name": "intro_all",
+  "status": "verified",
+  "tactic_count": 4,
+  "total_elapsed_ms": 4316,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "intro hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1004,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "intro hB",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1122,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "intro hC",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1029,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1161,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      4
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "intro hA",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "intro hB",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "intro hC",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_intro_apply.decomp.json

@@ -0,0 +1,108 @@
+{
+  "trace_summary": {
+    "theorem_name": "intro_apply",
+    "status": "verified",
+    "n_steps": 4,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 4
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 4.0,
+    "spectral_gap": 4.0,
+    "laplacian_eigenvalue_max": 4.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 4.0,
+    "trace": 4,
+    "density": 4.0
+  },
+  "feature_vector": [
+    4,
+    1,
+    4.0,
+    4.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.0,
+    0.25,
+    4532
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "introduction": 2,
+    "discharge": 2
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "intro h",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "intro hA",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "apply h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_intro_apply.trace.json

@@ -0,0 +1,157 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "da21735150a22821368a9558b2a064c574b7f822a59c9112146f9728140733f1",
+  "theorem_name": "intro_apply",
+  "status": "verified",
+  "tactic_count": 4,
+  "total_elapsed_ms": 4532,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "intro h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1149,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "intro hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1065,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "apply h",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1229,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1089,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      4
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "intro h",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "intro hA",
+      "tactic_family": "introduction",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "apply h",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 3,
+      "tactic": "exact hA",
+      "tactic_family": "discharge",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_chain_ineq.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "omega_chain_ineq",
+    "status": "verified",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    1.0,
+    1082
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_chain_ineq.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "28b82a6c260edf2bb49330f7b550dad25dc4f52e9b05458ea3e359db543f1636",
+  "theorem_name": "omega_chain_ineq",
+  "status": "verified",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1082,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1082,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_chain_unsat.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "omega_chain_unsat",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1141
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_chain_unsat.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "5230b5bd4815dd0b78eb21b270ff11d3ea24bfeeb0c6c1437837a5ce968259cf",
+  "theorem_name": "omega_chain_unsat",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1141,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1141,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_distrib.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "omega_distrib",
+    "status": "failed",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.0,
+    1071
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_distrib.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "caa088677ed4572fe89029b07d4184a54d71729acd710ec218f8ff1083cd390d",
+  "theorem_name": "omega_distrib",
+  "status": "failed",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1071,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1071,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_reorder_sum.decomp.json

@@ -0,0 +1,71 @@
+{
+  "trace_summary": {
+    "theorem_name": "omega_reorder_sum",
+    "status": "verified",
+    "n_steps": 1,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 1
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 1.0,
+    "spectral_gap": 1.0,
+    "laplacian_eigenvalue_max": 1.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 1.0,
+    "trace": 1,
+    "density": 1.0
+  },
+  "feature_vector": [
+    1,
+    1,
+    1.0,
+    1.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    1.0,
+    1056
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_omega_reorder_sum.trace.json

@@ -0,0 +1,52 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "34eb1411ee65a817e73e1a0fd58cabc6a85f959f966b031b0508cafe7779e660",
+  "theorem_name": "omega_reorder_sum",
+  "status": "verified",
+  "tactic_count": 1,
+  "total_elapsed_ms": 1056,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1056,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      1
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_3step.decomp.json

@@ -0,0 +1,95 @@
+{
+  "trace_summary": {
+    "theorem_name": "rw_chain_3step",
+    "status": "verified",
+    "n_steps": 3,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 3
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 3.0,
+    "spectral_gap": 3.0,
+    "laplacian_eigenvalue_max": 3.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 3.0,
+    "trace": 3,
+    "density": 3.0
+  },
+  "feature_vector": [
+    3,
+    1,
+    3.0,
+    3.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.3333333333333333,
+    3279
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "rewrite": 3
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "rw [h3]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_3step.trace.json

@@ -0,0 +1,122 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "1ff8b91260cbf4e62acd45fa1114b20dc0dd3e94bed90241654673aed39d1246",
+  "theorem_name": "rw_chain_3step",
+  "status": "verified",
+  "tactic_count": 3,
+  "total_elapsed_ms": 3279,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1066,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1094,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 2,
+      "tactic": "rw [h3]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1119,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      3
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 2,
+      "tactic": "rw [h3]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_eq.decomp.json

@@ -0,0 +1,83 @@
+{
+  "trace_summary": {
+    "theorem_name": "rw_chain_eq",
+    "status": "verified",
+    "n_steps": 2,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 2
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 2.0,
+    "spectral_gap": 2.0,
+    "laplacian_eigenvalue_max": 2.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 2.0,
+    "trace": 2,
+    "density": 2.0
+  },
+  "feature_vector": [
+    2,
+    1,
+    2.0,
+    2.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    -0.0,
+    0.5,
+    2524
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "rewrite": 2
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_eq.trace.json

@@ -0,0 +1,87 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "fb9ee92a7900d8987e1e38d4dfadb08e55ab3c4cc759243fe3f83aa945e87789",
+  "theorem_name": "rw_chain_eq",
+  "status": "verified",
+  "tactic_count": 2,
+  "total_elapsed_ms": 2524,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1243,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1281,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      2
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h1]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "rw [h2]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_mixed.decomp.json

@@ -0,0 +1,84 @@
+{
+  "trace_summary": {
+    "theorem_name": "rw_chain_mixed",
+    "status": "verified",
+    "n_steps": 2,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 2
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 2.0,
+    "spectral_gap": 2.0,
+    "laplacian_eigenvalue_max": 2.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 2.0,
+    "trace": 2,
+    "density": 2.0
+  },
+  "feature_vector": [
+    2,
+    1,
+    2.0,
+    2.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.0,
+    0.5,
+    2194
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "rewrite": 1,
+    "normalization": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "simp",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_chain_mixed.trace.json

@@ -0,0 +1,87 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "862ef6b1cf0e2eda6faf9968f33fc8e4147b48e614911bc996d1fb1258d23b39",
+  "theorem_name": "rw_chain_mixed",
+  "status": "verified",
+  "tactic_count": 2,
+  "total_elapsed_ms": 2194,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1105,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "simp",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1089,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      2
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    },
+    {
+      "step": 1,
+      "tactic": "simp",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_then_omega.decomp.json

@@ -0,0 +1,84 @@
+{
+  "trace_summary": {
+    "theorem_name": "rw_then_omega",
+    "status": "failed",
+    "n_steps": 2,
+    "n_unique_goal_states": 1,
+    "n_flexure_joints": 2
+  },
+  "spectral": {
+    "n_states": 1,
+    "eigenvalue_max": 2.0,
+    "spectral_gap": 2.0,
+    "laplacian_eigenvalue_max": 2.0,
+    "rank_estimate": 1,
+    "zero_rows": 0,
+    "frobenius_norm": 2.0,
+    "trace": 2,
+    "density": 2.0
+  },
+  "feature_vector": [
+    2,
+    1,
+    2.0,
+    2.0,
+    0,
+    1,
+    0.0,
+    0.0,
+    0.0,
+    1.0,
+    0.5,
+    2137
+  ],
+  "feature_names": [
+    "n_steps",
+    "n_unique_goal_states",
+    "transition_density",
+    "spectral_gap",
+    "laplacian_zero_count",
+    "rank_estimate",
+    "avg_delta_goal_count",
+    "avg_delta_hypothesis",
+    "avg_delta_symbol",
+    "tactic_family_entropy",
+    "verified_ratio",
+    "total_elapsed"
+  ],
+  "tactic_family_distribution": {
+    "rewrite": 1,
+    "arithmetic": 1
+  },
+  "delta_stats": {
+    "avg_goal_delta": 0.0,
+    "avg_hypothesis_delta": 0.0,
+    "avg_symbol_delta": 0.0,
+    "max_delta_score": 0
+  },
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_rw_then_omega.trace.json

@@ -0,0 +1,87 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "d1beb5b4ad2dc2941198c6d14e781358d6d6161d7f4f9e8c4a94fc934ca5d656",
+  "theorem_name": "rw_then_omega",
+  "status": "failed",
+  "tactic_count": 2,
+  "total_elapsed_ms": 2137,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1003,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1134,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      2
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "rw [h]",
+      "tactic_family": "rewrite",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    },
+    {
+      "step": 1,
+      "tactic": "omega",
+      "tactic_family": "arithmetic",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}

shared-data/proof_traces/canary_simp_chain_simple.trace.json

@@ -0,0 +1,87 @@
+{
+  "trace_version": "proof-trace-v1",
+  "receipt_hash": "974cd133f3c42af1013f13bfb435cc55fb31c57fb7674ac6948542aa2ae8aeaf",
+  "theorem_name": "simp_chain_simple",
+  "status": "failed",
+  "tactic_count": 2,
+  "total_elapsed_ms": 2227,
+  "steps": [
+    {
+      "step": 0,
+      "tactic": "simp",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1163,
+      "result": "success",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    },
+    {
+      "step": 1,
+      "tactic": "rfl",
+      "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b",
+      "before_goal_text": "\n",
+      "after_goal_text": "\n",
+      "goal_count_before": 1,
+      "goal_count_after": 1,
+      "hypothesis_count_before": 0,
+      "hypothesis_count_after": 0,
+      "operator_count_before": 0,
+      "operator_count_after": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "elapsed_ms": 1064,
+      "result": "failure",
+      "stdout_preview": "",
+      "stderr_preview": ""
+    }
+  ],
+  "goal_transition_matrix": [
+    [
+      2
+    ]
+  ],
+  "flexure_joints": [
+    {
+      "step": 0,
+      "tactic": "simp",
+      "tactic_family": "normalization",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "success"
+    },
+    {
+      "step": 1,
+      "tactic": "rfl",
+      "tactic_family": "reflexivity",
+      "delta_score": 0,
+      "delta": {
+        "symbol_delta": 0,
+        "hypothesis_delta": 0,
+        "goal_count_delta": 0
+      },
+      "result": "failure"
+    }
+  ]
+}