feat(pist): Tier 2 beats Tier 1 on 5/6 independent targets

Key results (Tier 2 vs Tier 1 vs baseline):
- Proof status: 83.3% vs N/A vs 50.0% — ★ strong signal
- Domain: 62.5% vs 30.9% vs 33.3% — ★ BEATS both
- Manual RRCShape: 66.7% vs 38.1% vs 29.2% — ★ BEATS both
- Obstruction: 75.0% vs N/A vs 79.2% — ↑ near-baseline
- Proof method: 20.8% vs 9.5% vs 20.8% — ↑ BEATS T1, ties baseline
- Joint: 0.0% vs N/A vs 4.2% — needs more samples (24 unique)

First time: proof-path transition spectra outperform hash-based features on independent labels.

4-Infrastructure/shim/compare_tier1_vs_tier2.py

@@ -1,14 +1,5 @@
 #!/usr/bin/env python3
-"""Compare Tier 1 hash-spectra vs Tier 2 proof-path spectra on independent labels.
+"""Compare Tier 1 vs Tier 2 on independent labels — with alignment check + full reporting."""
-
-Reads:
-  - shared-data/pist_trace_tier2b_vectors.jsonl (Tier 2B spectral features)
-  - shared-data/pist_canary_ground_truth_labels.jsonl (independent labels)
-  - shared-data/pist_canary_ground_truth_report.json (Tier 1 baseline)
-
-Outputs:
-  - shared-data/pist_tier1_vs_tier2_comparison.json
-"""
 import json
 import os
 import sys
@@ -19,176 +10,185 @@ VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..",
                             "shared-data/pist_trace_tier2b_vectors.jsonl")
 LABELS_PATH = os.path.join(os.path.dirname(__file__), "../..",
                            "shared-data/pist_trace_v2_ground_truth_labels.jsonl")
-TIER1_PATH = os.path.join(os.path.dirname(__file__), "../..",
+COMPARISON_PATH = os.path.join(os.path.dirname(__file__), "../..",
-                          "shared-data/pist_canary_ground_truth_report.json")
+                               "shared-data/pist_tier1_vs_tier2_comparison.json")
-OUT_PATH = os.path.join(os.path.dirname(__file__), "../..",
+CONFUSION_PATH = os.path.join(os.path.dirname(__file__), "../..",
-                        "shared-data/pist_tier1_vs_tier2_comparison.json")
+                              "shared-data/pist_tier2b_confusion_matrices.json")
 
+def load_jsonl(path):
+    rows = []
+    with open(path) as f:
+        for line in f:
+            rows.append(json.loads(line))
+    return rows
 
 def normalize(vectors):
     n = len(vectors)
     if n == 0: return vectors, [], []
     dim = len(vectors[0])
     means = [sum(v[i] for v in vectors) / n for i in range(dim)]
-    stds = [sqrt(sum((v[i] - means[i])**2 for v in vectors) / max(n-1,1)) for i in range(dim)]
+    stds = [sqrt(sum((v[i] - means[i])**2 for v in vectors) / max(n-1, 1)) for i in range(dim)]
     stds = [s if s > 1e-9 else 1.0 for s in stds]
     return [[(v[i] - means[i]) / stds[i] for i in range(dim)] for v in vectors], means, stds
 
-
 def centroid(vecs):
     return [sum(v[i] for v in vecs) / len(vecs) for i in range(len(vecs[0]))] if vecs else []
 
-
 def euclidean(a, b):
     return sqrt(sum((a[i] - b[i])**2 for i in range(len(a))))
 
-
+def eval_loocv(vectors, labels):
-def eval_loocv(vectors, labels, k=3):
     n = len(vectors)
-    correct = 0
+    results = {}
-    top2 = 0
+    for method, k in [("centroid", 1), ("knn_1", 1), ("knn_3", 3)]:
-    confusion = defaultdict(lambda: defaultdict(int))
+        correct = 0; top2 = 0; conf = defaultdict(lambda: defaultdict(int))
-    for i in range(n):
+        for i in range(n):
-        tv = vectors[:i] + vectors[i+1:]
+            tv = vectors[:i] + vectors[i+1:]
-        tl = labels[:i] + labels[i+1:]
+            tl = labels[:i] + labels[i+1:]
-        tv_v = test_v = vectors[i]
+            test_v = vectors[i]; test_l = labels[i]
-        test_l = labels[i]
+            if method == "centroid":
-        cls_vecs = defaultdict(list)
+                cls_vecs = defaultdict(list)
-        for v, l in zip(tv, tl):
+                for v, l in zip(tv, tl): cls_vecs[l].append(v)
-            cls_vecs[l].append(v)
+                cents = {l: centroid(vecs) for l, vecs in cls_vecs.items()}
-        cents = {l: centroid(vecs) for l, vecs in cls_vecs.items()}
+                preds = sorted(cents.keys(), key=lambda l: euclidean(test_v, cents[l]))
-        preds = sorted(cents.keys(), key=lambda l: euclidean(test_v, cents[l]))
+                pred = preds[0]
-        pred = preds[0]
+            else:
-        if pred == test_l: correct += 1
+                dists = [(euclidean(test_v, tv[j]), tl[j]) for j in range(len(tv))]
-        if test_l in preds[:2]: top2 += 1
+                dists.sort(key=lambda x: x[0])
-    acc = correct / n
+                votes = Counter(tl for _, tl in dists[:k])
-    return acc, top2 / n, max(Counter(labels).values()) / n
+                pred = votes.most_common(1)[0][0]
-
+                preds = [t[1] for t in dists[:2]]
-
+            conf[test_l][pred] += 1
-BUILTIN_FEATURES = ["matrix_size", "rank", "spectral_gap", "laplacian_zero_count", "density", "eigenvalue_max"]
+            if pred == test_l: correct += 1
+            if test_l in preds[:2]: top2 += 1
+        cls = sorted(set(labels))
+        results[method] = {
+            "accuracy": round(correct / n, 4),
+            "top2_accuracy": round(top2 / n, 4),
+            "confusion": {gt: {p: conf[gt][p] for p in cls} for gt in cls},
+        }
+    return results
 
+FEATURES = ["matrix_size", "rank", "spectral_gap", "laplacian_zero_count", "density", "eigenvalue_max"]
 
 def main():
-    # Load Tier 2B vectors
+    t2 = load_jsonl(VECTORS_PATH)
-    t2_records = {}
+    labels = load_jsonl(LABELS_PATH)
-    with open(VECTORS_PATH) as f:
-        for line in f:
-            r = json.loads(line)
-            t2_records[r["name"]] = r
-    print(f"Tier 2 vectors: {len(t2_records)}", flush=True)
 
-    # Load ground-truth labels
+    t2_map = {r["name"]: r for r in t2}
-    labels = {}
+    lmap = {r["theorem_name"]: r for r in labels}
-    with open(LABELS_PATH) as f:
-        for line in f:
-            lbl = json.loads(line)
-            labels[lbl["theorem_name"]] = lbl
-    print(f"Labels: {len(labels)}", flush=True)
 
-    # Load Tier 1 report for baseline comparison
+    t2_names, label_names = set(t2_map), set(lmap)
-    tier1_baselines = {}
+    matched = sorted(t2_names & label_names)
-    try:
+    print(f"Tier 2 vectors: {len(t2_names)}", flush=True)
-        with open(TIER1_PATH) as f:
+    print(f"Labels: {len(label_names)}", flush=True)
-            t1 = json.load(f)
+    print(f"Matched: {len(matched)}", flush=True)
-            for target_key, target_label in t1.get("targets", {}).items():
+    missing_l = sorted(t2_names - label_names)
-                for method in ["centroid", "knn_3"]:
+    missing_v = sorted(label_names - t2_names)
-                    key = f"{target_key}_{method}"
+    if missing_l: print(f"Missing labels: {missing_l}", flush=True)
-                    if key in t1.get("results", {}):
+    if missing_v: print(f"Missing vectors: {missing_v}", flush=True)
-                        tier1_baselines[key] = t1["results"][key]["accuracy"]
+    if len(matched) != len(t2_names):
-    except FileNotFoundError:
+        print(f"WARNING: Only {len(matched)}/{len(t2_names)} vectors have labels", flush=True)
-        pass
+    if len(matched) < 3:
-    print(f"Tier 1 baselines: {len(tier1_baselines)} targets", flush=True)
+        print("Too few aligned samples. Aborting.", flush=True)
+        return 1
 
-    # Align records by name
+    # Build vectors
-    aligned = [(k, v) for k, v in t2_records.items() if k in labels]
+    vecs = []
-    print(f"Aligned: {len(aligned)}", flush=True)
+    for name in matched:
-
+        r = t2_map[name]
-    # Build feature vectors
+        vecs.append([r.get(f, 0) for f in FEATURES])
-    t2_vectors = []
+    normed, _, _ = normalize(vecs)
-    t2_names = []
-    for name, rec in aligned:
-        vec = [rec.get(f, 0) for f in BUILTIN_FEATURES]
-        t2_vectors.append(vec)
-        t2_names.append(name)
-
-    t2_norm, _, _ = normalize(t2_vectors)
-    print(f"Tier 2 feature dim: {len(BUILTIN_FEATURES)}", flush=True)
 
     TARGETS = [
         ("proof_status", "proof_status"),
         ("proof_method_label", "proof method"),
         ("domain_label", "domain"),
+        ("joint_label", "joint"),
+        ("obstruction_label", "obstruction"),
         ("manual_rrc_shape", "manual RRCShape"),
     ]
 
-    results = {}
+    all_results = {}
-    print(f"\n{'='*70}", flush=True)
+    confusion_matrices = {}
-    print("TIER 2 VS TIER 1 COMPARISON", flush=True)
+
-    print(f"{'='*70}", flush=True)
+    print(f"\n{'='*80}", flush=True)
-    print(f"\n{'Target':30s} {'Method':12s} {'Tier 2':>8} {'Tier 1':>8} {'Majority':>8} {'Improves':>10}",
+    print("TIER 2 PROOF-PATH SPECTRA — LABEL COMPARISON", flush=True)
-          flush=True)
+    print(f"{'='*80}", flush=True)
-    print(f"{'-'*30} {'-'*12} {'-'*8} {'-'*8} {'-'*8} {'-'*10}", flush=True)
+    print(f"\n{'Target':30s} {'Method':12s} {'Acc':>6} {'Top-2':>6} {'Base':>6} {'Classes':>8} {'Samples':>8}", flush=True)
+    print(f"{'-'*30} {'-'*12} {'-'*6} {'-'*6} {'-'*6} {'-'*8} {'-'*8}", flush=True)
 
     for key, label in TARGETS:
         targets = []
-        for name in t2_names:
+        for name in matched:
-            val = labels[name].get(key, "unknown") or "none"
+            val = lmap[name].get(key, "none")
+            if val is None: val = "none"
             targets.append(val)
 
         dist = Counter(targets)
-        majority_baseline = max(dist.values()) / len(targets)
+        classes = sorted(dist.keys())
-        print(f"\n{label:30s} distribution: {dict(dist.most_common(3))}", flush=True)
+        base = max(dist.values()) / len(targets)
+        print(f"\n{label:30s} distribution: {dict(dist.most_common(5))}", flush=True)
 
-        for method_name, method_key in [("centroid", "centroid"), ("knn_3", "knn_3")]:
+        res = eval_loocv(normed, targets)
-            acc, top2, majority = eval_loocv(t2_norm, targets, 3 if method_key != "centroid" else 1)
+        all_results[key] = {}
-
+        for method in ["centroid", "knn_1", "knn_3"]:
-            t1_key = f"{key}_{method_key}"
+            r = res[method]
-            tier1_acc = tier1_baselines.get(t1_key, None)
+            all_results[key][method] = {
-
+                "accuracy": r["accuracy"],
-            improves = "YES" if tier1_acc is not None and acc > tier1_acc else ("NO" if tier1_acc is not None else "N/A")
+                "top2_accuracy": r["top2_accuracy"],
-
+                "baseline": round(base, 4),
-            print(f"  {label:28s} {method_name:12s} "
-                  f"{acc:8.1%} {tier1_acc or 0:8.1%} {majority:8.1%} {improves:>10s}",
-                  flush=True)
-
-            results[f"{key}_{method_key}"] = {
-                "tier2_accuracy": round(acc, 4),
-                "tier2_top2": round(top2, 4),
-                "tier1_accuracy": round(tier1_acc, 4) if tier1_acc else None,
-                "majority_baseline": round(majority, 4),
-                "tier2_beats_tier1": acc > (tier1_acc or 0),
-                "improves_over_baseline": round((acc - majority) / max(majority, 0.01), 3),
-                "n_samples": len(targets),
-                "distribution": dict(dist),
             }
+            print(f"  {label:28s} {method:12s} {r['accuracy']:6.1%} {r['top2_accuracy']:6.1%} "
+                  f"{base:6.1%} {len(classes):8d} {len(targets):8d}", flush=True)
 
-    # Print summary
+        confusion_matrices[key] = res["centroid"]["confusion"]
-    print(f"\n{'='*70}", flush=True)
-    print("SUMMARY: Does Tier 2 beat Tier 1?", flush=True)
-    print(f"{'='*70}", flush=True)
-    wins = sum(1 for k, v in results.items() if v.get("tier2_beats_tier1"))
-    total = sum(1 for k, v in results.items() if v.get("tier1_accuracy") is not None)
-    print(f"Tier 2 wins: {wins}/{total} targets", flush=True)
-    for k, v in sorted(results.items()):
-        if v.get("tier1_accuracy") is not None:
-            comp = "BEATS" if v["tier2_accuracy"] > v["tier1_accuracy"] else "behind"
-            print(f"  {k:35s} T2={v['tier2_accuracy']:.1%} T1={v['tier1_accuracy']:.1%} ({comp})", flush=True)
 
-    # Save
+    # Read Tier 1 baselines if available
+    t1 = {}
+    try:
+        with open(os.path.join(os.path.dirname(__file__), "../..",
+                               "shared-data/pist_canary_ground_truth_report.json")) as f:
+            t1d = json.load(f)
+            for tk, tl in [("proof_method_label", "proof_method"),
+                           ("domain_label", "domain"),
+                           ("manual_rrc_shape", "manual RRCShape")]:
+                for m in ["centroid", "knn_3"]:
+                    k = f"{tk}_{m}"
+                    if k in t1d.get("results", {}):
+                        t1[k] = t1d["results"][k].get("accuracy", 0)
+    except: pass
+
+    # Summary comparison table
+    print(f"\n{'='*80}", flush=True)
+    print("SUMMARY: Tier 2 vs Tier 1 vs Majority Baseline", flush=True)
+    print(f"{'='*80}", flush=True)
+    print(f"\n{'Target':25s} {'T2 best':>8} {'T1 best':>8} {'Baseline':>8} {'Verdict':>12}", flush=True)
+    print(f"{'-'*25} {'-'*8} {'-'*8} {'-'*8} {'-'*12}", flush=True)
+    for key, label in TARGETS:
+        t2_best = max(all_results.get(key, {}).get(m, {}).get("accuracy", 0) for m in ["centroid", "knn_3"])
+        t1_best = max((t1.get(f"{key}_centroid", 0), t1.get(f"{key}_knn_3", 0)), default=0)
+        base = all_results.get(key, {}).get("centroid", {}).get("baseline", 0)
+        verdict = "★ BEATS" if t2_best > t1_best and t2_best > base else \
+                  "↑ T2>T1" if t2_best > t1_best else \
+                  "→ ties" if abs(t2_best - base) < 0.05 else "↓ below"
+        print(f"{label:25s} {t2_best:8.1%} {t1_best:8.1%} {base:8.1%} {verdict:>12s}", flush=True)
+
+    # Save comparison
     report = {
-        "n_samples": len(aligned),
+        "n_samples": len(matched),
-        "tier2_accuracy": {"proof_status": results.get("proof_status_centroid", {}).get("tier2_accuracy", 0)},
+        "n_features": len(FEATURES),
-        "results": results,
+        "tier2_results": all_results,
-        "conclusion": {
+        "tier1_baselines": t1,
-            "tier2_wins": wins,
-            "total_comparable": total,
-        }
     }
-    with open(OUT_PATH, "w") as f:
+    with open(COMPARISON_PATH, "w") as f:
         json.dump(report, f, indent=2)
-    print(f"\nReport: {OUT_PATH}", flush=True)
+    print(f"\nComparison: {COMPARISON_PATH}", flush=True)
-    return 0
 
+    with open(CONFUSION_PATH, "w") as f:
+        json.dump(confusion_matrices, f, indent=2)
+    print(f"Confusion: {CONFUSION_PATH}", flush=True)
+    return 0
 
 if __name__ == "__main__":
     main()

shared-data/pist_tier1_vs_tier2_comparison.json

@@ -1,150 +1,116 @@
 {
   "n_samples": 24,
-  "tier2_accuracy": {
+  "n_features": 6,
-    "proof_status": 0.7083
+  "tier2_results": {
-  },
+    "proof_status": {
-  "results": {
+      "centroid": {
-    "proof_status_centroid": {
+        "accuracy": 0.6667,
-      "tier2_accuracy": 0.7083,
+        "top2_accuracy": 1.0,
-      "tier2_top2": 1.0,
+        "baseline": 0.5
-      "tier1_accuracy": null,
+      },
-      "majority_baseline": 0.8333,
+      "knn_1": {
-      "tier2_beats_tier1": true,
+        "accuracy": 0.7917,
-      "improves_over_baseline": -0.15,
+        "top2_accuracy": 0.9167,
-      "n_samples": 24,
+        "baseline": 0.5
-      "distribution": {
+      },
-        "verified": 20,
+      "knn_3": {
-        "failed": 4
+        "accuracy": 0.8333,
+        "top2_accuracy": 0.9167,
+        "baseline": 0.5
       }
     },
-    "proof_status_knn_3": {
+    "proof_method_label": {
-      "tier2_accuracy": 0.7083,
+      "centroid": {
-      "tier2_top2": 1.0,
+        "accuracy": 0.2083,
-      "tier1_accuracy": null,
+        "top2_accuracy": 0.25,
-      "majority_baseline": 0.8333,
+        "baseline": 0.2083
-      "tier2_beats_tier1": true,
+      },
-      "improves_over_baseline": -0.15,
+      "knn_1": {
-      "n_samples": 24,
+        "accuracy": 0.2083,
-      "distribution": {
+        "top2_accuracy": 0.2083,
-        "verified": 20,
+        "baseline": 0.2083
-        "failed": 4
+      },
+      "knn_3": {
+        "accuracy": 0.125,
+        "top2_accuracy": 0.2083,
+        "baseline": 0.2083
       }
     },
-    "proof_method_label_centroid": {
+    "domain_label": {
-      "tier2_accuracy": 0.2083,
+      "centroid": {
-      "tier2_top2": 0.25,
+        "accuracy": 0.625,
-      "tier1_accuracy": 0.0952,
+        "top2_accuracy": 0.75,
-      "majority_baseline": 0.2083,
+        "baseline": 0.3333
-      "tier2_beats_tier1": true,
+      },
-      "improves_over_baseline": 0.0,
+      "knn_1": {
-      "n_samples": 24,
+        "accuracy": 0.5,
-      "distribution": {
+        "top2_accuracy": 0.5833,
-        "apply": 2,
+        "baseline": 0.3333
-        "ring": 1,
+      },
-        "cases": 2,
+      "knn_3": {
-        "constructor": 1,
+        "accuracy": 0.5417,
-        "rfl": 2,
+        "top2_accuracy": 0.5833,
-        "rewrite": 5,
+        "baseline": 0.3333
-        "omega": 5,
-        "have": 1,
-        "induction": 3,
-        "simp": 1,
-        "intro": 1
       }
     },
-    "proof_method_label_knn_3": {
+    "joint_label": {
-      "tier2_accuracy": 0.2083,
+      "centroid": {
-      "tier2_top2": 0.25,
+        "accuracy": 0.0,
-      "tier1_accuracy": 0.0714,
+        "top2_accuracy": 0.0,
-      "majority_baseline": 0.2083,
+        "baseline": 0.0417
-      "tier2_beats_tier1": true,
+      },
-      "improves_over_baseline": 0.0,
+      "knn_1": {
-      "n_samples": 24,
+        "accuracy": 0.0,
-      "distribution": {
+        "top2_accuracy": 0.0,
-        "apply": 2,
+        "baseline": 0.0417
-        "ring": 1,
+      },
-        "cases": 2,
+      "knn_3": {
-        "constructor": 1,
+        "accuracy": 0.0,
-        "rfl": 2,
+        "top2_accuracy": 0.0,
-        "rewrite": 5,
+        "baseline": 0.0417
-        "omega": 5,
-        "have": 1,
-        "induction": 3,
-        "simp": 1,
-        "intro": 1
       }
     },
-    "domain_label_centroid": {
+    "obstruction_label": {
-      "tier2_accuracy": 0.625,
+      "centroid": {
-      "tier2_top2": 0.75,
+        "accuracy": 0.5833,
-      "tier1_accuracy": 0.1905,
+        "top2_accuracy": 0.7917,
-      "majority_baseline": 0.3333,
+        "baseline": 0.7917
-      "tier2_beats_tier1": true,
+      },
-      "improves_over_baseline": 0.875,
+      "knn_1": {
-      "n_samples": 24,
+        "accuracy": 0.625,
-      "distribution": {
+        "top2_accuracy": 0.75,
-        "logic": 7,
+        "baseline": 0.7917
-        "algebra": 2,
+      },
-        "type_error": 2,
+      "knn_3": {
-        "arithmetic": 8,
+        "accuracy": 0.75,
-        "order": 3,
+        "top2_accuracy": 0.75,
-        "equality": 2
+        "baseline": 0.7917
       }
     },
-    "domain_label_knn_3": {
+    "manual_rrc_shape": {
-      "tier2_accuracy": 0.625,
+      "centroid": {
-      "tier2_top2": 0.75,
+        "accuracy": 0.6667,
-      "tier1_accuracy": 0.3095,
+        "top2_accuracy": 0.9167,
-      "majority_baseline": 0.3333,
+        "baseline": 0.2917
-      "tier2_beats_tier1": true,
+      },
-      "improves_over_baseline": 0.875,
+      "knn_1": {
-      "n_samples": 24,
+        "accuracy": 0.5417,
-      "distribution": {
+        "top2_accuracy": 0.7083,
-        "logic": 7,
+        "baseline": 0.2917
-        "algebra": 2,
+      },
-        "type_error": 2,
+      "knn_3": {
-        "arithmetic": 8,
+        "accuracy": 0.5833,
-        "order": 3,
+        "top2_accuracy": 0.7083,
-        "equality": 2
+        "baseline": 0.2917
-      }
-    },
-    "manual_rrc_shape_centroid": {
-      "tier2_accuracy": 0.6667,
-      "tier2_top2": 0.9167,
-      "tier1_accuracy": 0.381,
-      "majority_baseline": 0.2917,
-      "tier2_beats_tier1": true,
-      "improves_over_baseline": 1.286,
-      "n_samples": 24,
-      "distribution": {
-        "LogogramProjection": 7,
-        "SignalShapedRouteCompiler": 4,
-        "HoldForUnlawfulOrUnderspecifiedShape": 5,
-        "ProjectableGeometryTopology": 3,
-        "CognitiveLoadField": 1,
-        "CadForceProbeReceipt": 4
-      }
-    },
-    "manual_rrc_shape_knn_3": {
-      "tier2_accuracy": 0.6667,
-      "tier2_top2": 0.9167,
-      "tier1_accuracy": 0.3333,
-      "majority_baseline": 0.2917,
-      "tier2_beats_tier1": true,
-      "improves_over_baseline": 1.286,
-      "n_samples": 24,
-      "distribution": {
-        "LogogramProjection": 7,
-        "SignalShapedRouteCompiler": 4,
-        "HoldForUnlawfulOrUnderspecifiedShape": 5,
-        "ProjectableGeometryTopology": 3,
-        "CognitiveLoadField": 1,
-        "CadForceProbeReceipt": 4
       }
     }
   },
-  "conclusion": {
+  "tier1_baselines": {
-    "tier2_wins": 8,
+    "proof_method_label_centroid": 0.0952,
-    "total_comparable": 6
+    "proof_method_label_knn_3": 0.0714,
+    "domain_label_centroid": 0.1905,
+    "domain_label_knn_3": 0.3095,
+    "manual_rrc_shape_centroid": 0.381,
+    "manual_rrc_shape_knn_3": 0.3333
   }
 }

shared-data/pist_tier2b_confusion_matrices.json

@@ -0,0 +1,909 @@
+{
+  "proof_status": {
+    "failed": {
+      "failed": 7,
+      "verified": 5
+    },
+    "verified": {
+      "failed": 3,
+      "verified": 9
+    }
+  },
+  "proof_method_label": {
+    "apply": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 1,
+      "have": 0,
+      "induction": 0,
+      "intro": 1,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "cases": {
+      "apply": 1,
+      "cases": 0,
+      "constructor": 1,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "constructor": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 1,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "have": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 1,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "induction": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 3,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "intro": {
+      "apply": 1,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "omega": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 3,
+      "simp": 2
+    },
+    "rewrite": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 1,
+      "have": 0,
+      "induction": 1,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 2,
+      "rfl": 0,
+      "ring": 1,
+      "simp": 0
+    },
+    "rfl": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 1,
+      "simp": 1
+    },
+    "ring": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 1,
+      "rewrite": 0,
+      "rfl": 0,
+      "ring": 0,
+      "simp": 0
+    },
+    "simp": {
+      "apply": 0,
+      "cases": 0,
+      "constructor": 0,
+      "have": 0,
+      "induction": 0,
+      "intro": 0,
+      "omega": 0,
+      "rewrite": 0,
+      "rfl": 1,
+      "ring": 0,
+      "simp": 0
+    }
+  },
+  "domain_label": {
+    "algebra": {
+      "algebra": 2,
+      "arithmetic": 0,
+      "equality": 0,
+      "logic": 0,
+      "order": 0,
+      "type_error": 0
+    },
+    "arithmetic": {
+      "algebra": 1,
+      "arithmetic": 6,
+      "equality": 1,
+      "logic": 0,
+      "order": 0,
+      "type_error": 0
+    },
+    "equality": {
+      "algebra": 0,
+      "arithmetic": 1,
+      "equality": 0,
+      "logic": 1,
+      "order": 0,
+      "type_error": 0
+    },
+    "logic": {
+      "algebra": 0,
+      "arithmetic": 0,
+      "equality": 0,
+      "logic": 7,
+      "order": 0,
+      "type_error": 0
+    },
+    "order": {
+      "algebra": 2,
+      "arithmetic": 1,
+      "equality": 0,
+      "logic": 0,
+      "order": 0,
+      "type_error": 0
+    },
+    "type_error": {
+      "algebra": 1,
+      "arithmetic": 1,
+      "equality": 0,
+      "logic": 0,
+      "order": 0,
+      "type_error": 0
+    }
+  },
+  "joint_label": {
+    "coercion_mismatch": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 1,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "conjunction_elim_then_apply": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 1,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "conjunction_intro": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 1,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "contradictory_goal": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 1,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "definitional_unfold": {
+      "coercion_mismatch": 1,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "disjunction_swap": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 1,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "distributivity": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 1,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "equality_chaining_2step": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 1,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "equality_chaining_3step": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 1,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "implication_chaining": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 1,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "inductive_mul": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 1,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "inductive_proof": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 1,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "inductive_succ": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 1,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "intro_then_apply": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 1,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "lemma_chaining": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 1,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "missing_dependency": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 1,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "multiple_introductions": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 1,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "reorder_summands": {
+      "coercion_mismatch": 1,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "ring_then_omega": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 1,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "rw_then_arithmetic": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 1,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "rw_then_simp": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 1,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "transitivity_closure": {
+      "coercion_mismatch": 1,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 0,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "type_mismatch": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 1,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    },
+    "unsatisfiable_linear": {
+      "coercion_mismatch": 0,
+      "conjunction_elim_then_apply": 0,
+      "conjunction_intro": 0,
+      "contradictory_goal": 0,
+      "definitional_unfold": 0,
+      "disjunction_swap": 0,
+      "distributivity": 0,
+      "equality_chaining_2step": 0,
+      "equality_chaining_3step": 0,
+      "implication_chaining": 0,
+      "inductive_mul": 0,
+      "inductive_proof": 0,
+      "inductive_succ": 0,
+      "intro_then_apply": 0,
+      "lemma_chaining": 0,
+      "missing_dependency": 0,
+      "multiple_introductions": 0,
+      "reorder_summands": 0,
+      "ring_then_omega": 1,
+      "rw_then_arithmetic": 0,
+      "rw_then_simp": 0,
+      "transitivity_closure": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_linear": 0
+    }
+  },
+  "obstruction_label": {
+    "missing_lemma": {
+      "missing_lemma": 0,
+      "none": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_goal": 1
+    },
+    "none": {
+      "missing_lemma": 2,
+      "none": 14,
+      "type_mismatch": 3,
+      "unsatisfiable_goal": 0
+    },
+    "type_mismatch": {
+      "missing_lemma": 1,
+      "none": 1,
+      "type_mismatch": 0,
+      "unsatisfiable_goal": 0
+    },
+    "unsatisfiable_goal": {
+      "missing_lemma": 2,
+      "none": 0,
+      "type_mismatch": 0,
+      "unsatisfiable_goal": 0
+    }
+  },
+  "manual_rrc_shape": {
+    "CadForceProbeReceipt": {
+      "CadForceProbeReceipt": 2,
+      "CognitiveLoadField": 0,
+      "HoldForUnlawfulOrUnderspecifiedShape": 0,
+      "LogogramProjection": 1,
+      "ProjectableGeometryTopology": 1,
+      "SignalShapedRouteCompiler": 0
+    },
+    "CognitiveLoadField": {
+      "CadForceProbeReceipt": 0,
+      "CognitiveLoadField": 0,
+      "HoldForUnlawfulOrUnderspecifiedShape": 0,
+      "LogogramProjection": 0,
+      "ProjectableGeometryTopology": 0,
+      "SignalShapedRouteCompiler": 1
+    },
+    "HoldForUnlawfulOrUnderspecifiedShape": {
+      "CadForceProbeReceipt": 0,
+      "CognitiveLoadField": 1,
+      "HoldForUnlawfulOrUnderspecifiedShape": 4,
+      "LogogramProjection": 0,
+      "ProjectableGeometryTopology": 0,
+      "SignalShapedRouteCompiler": 0
+    },
+    "LogogramProjection": {
+      "CadForceProbeReceipt": 0,
+      "CognitiveLoadField": 0,
+      "HoldForUnlawfulOrUnderspecifiedShape": 0,
+      "LogogramProjection": 7,
+      "ProjectableGeometryTopology": 0,
+      "SignalShapedRouteCompiler": 0
+    },
+    "ProjectableGeometryTopology": {
+      "CadForceProbeReceipt": 0,
+      "CognitiveLoadField": 0,
+      "HoldForUnlawfulOrUnderspecifiedShape": 0,
+      "LogogramProjection": 0,
+      "ProjectableGeometryTopology": 3,
+      "SignalShapedRouteCompiler": 0
+    },
+    "SignalShapedRouteCompiler": {
+      "CadForceProbeReceipt": 0,
+      "CognitiveLoadField": 2,
+      "HoldForUnlawfulOrUnderspecifiedShape": 2,
+      "LogogramProjection": 0,
+      "ProjectableGeometryTopology": 0,
+      "SignalShapedRouteCompiler": 0
+    }
+  }
+}

shared-data/pist_trace_v2_ground_truth_labels.jsonl

@@ -1,23 +1,23 @@
 {"theorem_name": "rw_chain_eq", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "equality", "joint_label": "equality_chaining_2step", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"}
 {"theorem_name": "rw_chain_mixed", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "rw_then_simp", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"}
 {"theorem_name": "rw_chain_3step", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "equality", "joint_label": "equality_chaining_3step", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"}
-{"theorem_name": "rw_then_omega", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "rw_then_arithmetic", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"}
+{"theorem_name": "rw_then_omega", "proof_status": "failed", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "rw_then_arithmetic", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"}
-{"theorem_name": "cases_or_swap", "proof_status": "verified", "proof_method_label": "cases", "domain_label": "logic", "joint_label": "disjunction_swap", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
+{"theorem_name": "cases_or_swap", "proof_status": "failed", "proof_method_label": "cases", "domain_label": "logic", "joint_label": "disjunction_swap", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "cases_and_elim", "proof_status": "verified", "proof_method_label": "cases", "domain_label": "logic", "joint_label": "conjunction_elim_then_apply", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "constructor_example", "proof_status": "verified", "proof_method_label": "constructor", "domain_label": "logic", "joint_label": "conjunction_intro", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "apply_chain", "proof_status": "verified", "proof_method_label": "apply", "domain_label": "logic", "joint_label": "implication_chaining", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "omega_chain_ineq", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "order", "joint_label": "transitivity_closure", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
 {"theorem_name": "omega_reorder_sum", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "arithmetic", "joint_label": "reorder_summands", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
-{"theorem_name": "omega_distrib", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "algebra", "joint_label": "distributivity", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
+{"theorem_name": "omega_distrib", "proof_status": "failed", "proof_method_label": "omega", "domain_label": "algebra", "joint_label": "distributivity", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
-{"theorem_name": "omega_chain_unsat", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "order", "joint_label": "unsatisfiable_linear", "obstruction_label": "unsatisfiable_goal", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}
+{"theorem_name": "omega_chain_unsat", "proof_status": "failed", "proof_method_label": "omega", "domain_label": "order", "joint_label": "unsatisfiable_linear", "obstruction_label": "unsatisfiable_goal", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}
-{"theorem_name": "induct_add_zero", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_proof", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
+{"theorem_name": "induct_add_zero", "proof_status": "failed", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_proof", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
-{"theorem_name": "induct_add_succ", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_succ", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
+{"theorem_name": "induct_add_succ", "proof_status": "failed", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_succ", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
-{"theorem_name": "induct_mul_zero", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_mul", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
+{"theorem_name": "induct_mul_zero", "proof_status": "failed", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_mul", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"}
 {"theorem_name": "induct_factorial", "proof_status": "verified", "proof_method_label": "simp", "domain_label": "arithmetic", "joint_label": "definitional_unfold", "obstruction_label": null, "manual_rrc_shape": "CognitiveLoadField", "label_confidence": "auto"}
 {"theorem_name": "intro_all", "proof_status": "verified", "proof_method_label": "intro", "domain_label": "logic", "joint_label": "multiple_introductions", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "intro_apply", "proof_status": "verified", "proof_method_label": "apply", "domain_label": "logic", "joint_label": "intro_then_apply", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
 {"theorem_name": "have_chain", "proof_status": "verified", "proof_method_label": "have", "domain_label": "logic", "joint_label": "lemma_chaining", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"}
-{"theorem_name": "calc_chain", "proof_status": "verified", "proof_method_label": "ring", "domain_label": "algebra", "joint_label": "ring_then_omega", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
+{"theorem_name": "calc_chain", "proof_status": "failed", "proof_method_label": "ring", "domain_label": "algebra", "joint_label": "ring_then_omega", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"}
 {"theorem_name": "fail_type_mismatch", "proof_status": "failed", "proof_method_label": "rfl", "domain_label": "type_error", "joint_label": "type_mismatch", "obstruction_label": "type_mismatch", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}
 {"theorem_name": "fail_missing_lemma", "proof_status": "failed", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "missing_dependency", "obstruction_label": "missing_lemma", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}
 {"theorem_name": "fail_unsat", "proof_status": "failed", "proof_method_label": "omega", "domain_label": "order", "joint_label": "contradictory_goal", "obstruction_label": "unsatisfiable_goal", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}