From e7525fb6f437aab73a73f9e0b0376b0f82db994e Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 02:09:08 -0500 Subject: [PATCH] =?UTF-8?q?feat(pist):=20canary=20batch=20=E2=80=94=2042?= =?UTF-8?q?=20real=20Lean=20theorems=20through=20full=20pipeline?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 42/42 unique matrix hashes (100%) - 42/42 unique canonical hashes (no collisions) - 42/42 unique spectral gaps (full diversity) - Rank estimate: 5 distinct values, range [4, 8] - Laplacian zero count: 3 distinct values, range [1, 3] - 1 outlier: omega_double classified as CadForceProbeReceipt (rank=4) - Classifier still collapses to LogogramProjection for rank>=5 Conclusion: spectral features are diverse. Classifier thresholds need training, not hand-tuning. --- 4-Infrastructure/shim/pist_canary_batch.py | 372 +++++++++++ shared-data/pist_canary_receipts.jsonl | 42 ++ shared-data/pist_canary_report.json | 703 +++++++++++++++++++++ shared-data/pist_canary_results.jsonl | 42 ++ 4 files changed, 1159 insertions(+) create mode 100644 4-Infrastructure/shim/pist_canary_batch.py create mode 100644 shared-data/pist_canary_receipts.jsonl create mode 100644 shared-data/pist_canary_report.json create mode 100644 shared-data/pist_canary_results.jsonl diff --git a/4-Infrastructure/shim/pist_canary_batch.py b/4-Infrastructure/shim/pist_canary_batch.py new file mode 100644 index 00000000..4ef3010b --- /dev/null +++ b/4-Infrastructure/shim/pist_canary_batch.py @@ -0,0 +1,372 @@ +#!/usr/bin/env python3 +"""Canary batch: run 20-50 Lean theorems through proof worker → PIST → classify. + +Generates: + shared-data/pist_canary_receipts.jsonl — structural receipts v2 + shared-data/pist_canary_results.jsonl — PIST classification results + shared-data/pist_canary_report.json — cluster/analysis report +""" + +import json +import math +import os +import random +import subprocess +import sys +import tempfile +import time +import uuid +from collections import Counter, defaultdict +from datetime import datetime, timezone +from pathlib import Path + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), ".")) +from validate_rrc_predictions import parse_equation, build_proof_metrics + +PIST_DECOMPOSE = os.environ.get( + "PIST_DECOMPOSE_BIN", + "/home/allaun/.local/share/opencode/worktree/" + "0b42981cf7f7d5e172b1e93f8d4bb64a3dd63962/Turn-and-Burn/infra/rust/" + "ene-rds/target/release/pist-decompose", +) + +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 = "" + +CANARY_THEOREMS = [ + # ── rfl / trivial ── + ("rfl_one", "theorem t (n : Nat) : n = n := by rfl"), + ("rfl_add", "theorem t (n : Nat) : n + 0 = n := by rfl"), + ("rfl_succ", "theorem t (n : Nat) : n.succ = n.succ := by rfl"), + + # ── simp ── + ("simp_add_zero", "theorem t (n : Nat) : n + 0 = n := by simp"), + ("simp_mul_one", "theorem t (n : Nat) : n * 1 = n := by simp"), + ("simp_add_comm", "theorem t (a b : Nat) : a + b = b + a := by simp [add_comm]"), + ("simp_add_assoc", "theorem t (a b c : Nat) : (a + b) + c = a + (b + c) := by simp [add_assoc]"), + ("simp_mul_comm", "theorem t (a b : Nat) : a * b = b * a := by simp [mul_comm]"), + + # ── omega / arithmetic ── + ("omega_add", "theorem t (a b c : Nat) : a + b + c = a + c + b := by omega"), + ("omega_mul", "theorem t (a b : Nat) : (a + b) * 2 = a*2 + b*2 := by omega"), + ("omega_ineq", "theorem t (a b : Nat) (h : a ≤ b) : a + 1 ≤ b + 1 := by omega"), + ("omega_mod", "theorem t (a : Nat) : a % 2 < 2 := by omega"), + ("omega_double", "theorem t (n : Nat) : n + n = 2 * n := by omega"), + + # ── ring ── + ("ring_sq", "theorem t (x y : Nat) : (x + y)^2 = x^2 + 2*x*y + y^2 := by nlinarith"), + ("ring_cube", "theorem t (x : Nat) : (x+1)^3 = x^3 + 3*x^2 + 3*x + 1 := by nlinarith"), + ("ring_expand", "theorem t (a b : Nat) : (a + b) * (a - b) = a^2 - b^2 := by omega"), + + # ── induction ── + ("induct_add_zero", "theorem t (n : Nat) : n + 0 = n := by induction n with k IH; rfl; simp [add_succ, IH]"), + ("induct_add_succ", "theorem t (n m : Nat) : n + m.succ = (n + m).succ := by induction n with k IH; rfl; simp [add_succ, IH]"), + ("induct_mul", "theorem t (n m : Nat) : n * m = m * n := by induction n with k IH; simp; simp [mul_add, IH, add_comm, add_left_comm, add_assoc]"), + + # ── rewrite-heavy ── + ("rw_add_comm", "theorem t (a b : Nat) : a + b = b + a := by rw [add_comm a b]"), + ("rw_mul_comm", "theorem t (a b : Nat) : a * b = b * a := by rw [mul_comm]"), + ("rw_add_assoc", "theorem t (a b c : Nat) : a + b + c = c + b + a := by rw [add_comm a b, add_comm (a+b) c, add_comm b a]; rfl"), + + # ── with imports ── + ("with_import_list", "import Mathlib.Data.List.Basic\ntheorem t (l : List Nat) : l.reverse.reverse = l := by simp"), + ("with_import_nat", "import Mathlib.Data.Nat.Basic\ntheorem t (a b : Nat) : a.gcd b = b.gcd a := Nat.gcd_comm a b"), + ("with_import_int", "import Mathlib.Data.Int.Basic\ntheorem t (a b : ℤ) : a + b = b + a := by omega"), + ("with_import_set", "import Mathlib.Data.Set.Basic\ntheorem t (s : Set Nat) : s ∪ s = s := Set.union_self s"), + + # ── algebra / ring ── + ("algebra_id", "theorem t (x : Nat) : x * 1 = x := by simp"), + ("algebra_distrib", "theorem t (a b c : Nat) : a * (b + c) = a * b + a * c := by omega"), + ("algebra_sq_diff", "theorem t (x y : Nat) : x^2 - y^2 = (x - y) * (x + y) := by omega"), + + # ── logic / boolean ── + ("logic_and", "theorem t (A B : Prop) : A ∧ B → A := by intro h; exact h.1"), + ("logic_or", "theorem t (A B : Prop) : A ∨ B → B ∨ A := by intro h; cases h; right; exact h; left; exact h"), + ("logic_not_not", "theorem t (P : Prop) : P → ¬¬P := by intro hp hnp; exact hnp hp"), + ("logic_impl_trans", "theorem t (A B C : Prop) : (A → B) → (B → C) → (A → C) := by intro h1 h2 ha; exact h2 (h1 ha)"), + + # ── lattice / order ── + ("order_refl", "theorem t (a : Nat) : a ≤ a := Nat.le_refl a"), + ("order_trans", "theorem t (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := Nat.le_trans h1 h2"), + ("order_antisymm", "theorem t (a b : Nat) (h1 : a ≤ b) (h2 : b ≤ a) : a = b := Nat.le_antisymm h1 h2"), + + # ── failure cases ── + ("expect_fail_type_mismatch", "theorem t : Nat → String := λ n => n"), + ("expect_fail_unsat", "theorem t (x : Nat) : x < x := by omega"), + ("expect_fail_axiom", "theorem t : 1 = 0 := by native_decide"), + ("expect_fail_timeout_like", "theorem t (a b : Nat) : a^10 + b^10 = (a+b)^10 := by nlinarith"), + + # ── deliberately complex ── + ("complex_fib", "def fib : Nat → Nat | 0 => 0 | 1 => 1 | n+2 => fib (n+1) + fib n\ntheorem t (n : Nat) : fib (n+2) = fib (n+1) + fib n := by rfl"), + ("complex_sum", "theorem t (n : Nat) : ∑ k in Finset.range n, k = n*(n-1)/2 := by sorry"), +] + + +def prove(code: str, name: str, url: str, timeout_s: int = 60) -> dict: + """Send a Lean proof to a worker and return the response.""" + result = subprocess.run( + ["curl", "-s", "--connect-timeout", "10", "-X", "POST", f"{url}/lean/check", + "-H", "Content-Type: application/json", + "-H", f"Authorization: Bearer {PROOF_SERVER_TOKEN}", + "-d", json.dumps({"code": code, "name": name})], + capture_output=True, text=True, timeout=timeout_s, + ) + if result.returncode != 0: + return {"error": f"curl exit {result.returncode}: {result.stderr[:200]}", "ok": False} + try: + return json.loads(result.stdout) + except json.JSONDecodeError as e: + return {"error": f"json: {e}", "raw": result.stdout[:300], "ok": False} + + +def build_receipt(response: dict, name: str, code: str, status: str) -> dict: + """Build structural receipt v2 from proof worker response.""" + receipt = response.get("receipt", response) + ok = response.get("ok", False) + elapsed = receipt.get("elapsed_ms", 0) + returncode = receipt.get("returncode", -1) + + struct = parse_equation(name) + struct["equation_text"] = name.replace("_", " ") + + lines = code.strip().split("\n") + imports = [l.split("import")[1].strip() for l in lines if l.strip().startswith("import")] + proof_lines = [l for l in lines if not l.strip().startswith("import") and not l.strip().startswith("def ")] + proof_script = proof_lines[0] if proof_lines else code + + shape_map = { + "verified": "CognitiveLoadField", + "failed": "HoldForUnlawfulOrUnderspecifiedShape", + "timeout": "HoldForUnlawfulOrUnderspecifiedShape", + } + shape = shape_map.get(status, "HoldForUnlawfulOrUnderspecifiedShape") + proof = build_proof_metrics(shape) + domain = shape.replace("CognitiveLoadField", "analysis") \ + .replace("HoldForUnlawfulOrUnderspecifiedShape", "unknown") + + return { + "receipt_version": "rrc-proof-receipt-v2", + "theorem_name": name, + **struct, + "domain": domain, + "theorem_statement": code, + "proof_script": proof_script, + "imports": imports, + "dependencies": imports, + "source_hash": receipt.get("input_sha256", str(uuid.uuid4())), + "environment_hash": receipt.get("generated_at_utc", datetime.now(timezone.utc).isoformat()), + "status": status, + "kernel_checked": ok, + "returncode": returncode, + "elapsed_ms": elapsed, + "proof_metrics": proof, + "metrics": { + "statement_chars": len(code), + "proof_chars": len(proof_script), + "dependency_count": proof["dependency_count"], + "import_count": len(imports), + "tactic_count": proof["tactic_count"], + "ast_depth_estimate": struct["ast_metrics"]["depth"], + }, + } + + +def pist_classify(receipt: dict) -> dict: + """Run pist-decompose on a structural receipt.""" + with tempfile.NamedTemporaryFile(mode="w", suffix=".json", delete=False) as f: + json.dump(receipt, f) + fpath = f.name + try: + result = subprocess.run( + [PIST_DECOMPOSE, fpath, "--num-leaves", "8"], + capture_output=True, text=True, timeout=30, + ) + if result.returncode != 0: + return {"error": result.stderr[:200], "ok": False} + return json.loads(result.stdout) + finally: + os.unlink(fpath) + + +def main(): + worker_url = os.environ.get("CANARY_WORKER_URL", + "http://100.110.163.82:8787") + theorems = [(n, c) for n, c in CANARY_THEOREMS] + print(f"Canary batch: {len(theorems)} theorems, worker={worker_url}", flush=True) + + receipts_path = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_canary_receipts.jsonl") + results_path = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_canary_results.jsonl") + report_path = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_canary_report.json") + + rfile = open(receipts_path, "w") + rslts = [] + + for i, (name, code) in enumerate(theorems): + print(f"\n[{i+1}/{len(theorems)}] {name:30s} ... ", end="", flush=True) + t0 = time.time() + + try: + resp = prove(code, name, worker_url) + dt = time.time() - t0 + except subprocess.TimeoutExpired: + resp = {"ok": False, "error": "timeout", "receipt": {"elapsed_ms": 60_000, "returncode": -1}} + dt = 60.0 + + ok = resp.get("ok", False) + receipt = resp.get("receipt", resp) + std = receipt.get("stdout", "") + err = receipt.get("stderr", "") + rc = receipt.get("returncode", -1) + elapsed = receipt.get("elapsed_ms", int(dt * 1000)) + + if "error" in resp and "timeout" in str(resp.get("error")): + status = "timeout" + elif ok and rc == 0: + status = "verified" + elif "error" in resp: + status = "worker_error" + elif not ok and "Lean" in str(std) or "error" in str(std): + status = "elaboration_error" + else: + status = "failed" + + # Verify the proof result actually makes sense + if status == "verified" and not std.strip() and not err.strip(): + status = "verified_empty_output" + + print(f"{status:25s} {dt:5.1f}s rc={rc}", flush=True) + + structural = build_receipt(resp, name, code, status) + + # Run PIST + pist_result = pist_classify(structural) + proxy = pist_result.get("rrc_shape", {}).get("proxy", {}).get("label", "?") + exact = pist_result.get("rrc_shape", {}).get("exact", {}).get("label", "?") + zmp = pist_result.get("spectral", {}).get("zero_mode_proxy_count", "?") + mhash = pist_result.get("braid", {}).get("matrix_hash", "?")[:16] + chash = pist_result.get("canonical_hash", "?")[:16] + gap = pist_result.get("spectral", {}).get("symmetric_spectral_gap", 0) + rank = pist_result.get("spectral", {}).get("rank_estimate", 0) + lap0 = pist_result.get("spectral", {}).get("laplacian_zero_count", 0) + + print(f" PIST→ proxy={proxy:30s} exact={exact:30s} ZMP={zmp} gap={gap:.3f}", flush=True) + + row = { + "name": name, "status": status, "ok": ok, "returncode": rc, + "elapsed_ms": elapsed, "wall_s": round(dt, 2), + "proxy_shape": proxy, "exact_shape": exact, + "zmp": zmp, "spectral_gap": gap, "rank_estimate": rank, + "laplacian_zero_count": lap0, + "matrix_hash": mhash, "canonical_hash": chash, + } + rslts.append(row) + + # Write receipt JSONL + rfile.write(json.dumps(structural) + "\n") + + rfile.close() + + # ── Analysis ── + print("\n" + "=" * 60, flush=True) + print("CANARY REPORT", flush=True) + print("=" * 60, flush=True) + + n = len(rslts) + verified = sum(1 for r in rslts if r["status"] == "verified") + failed = sum(1 for r in rslts if r["status"] != "verified") + + print(f"\nTotal: {n}", flush=True) + print(f"Verified: {verified} ({verified/n*100:.0f}%)", flush=True) + print(f"Failed/error: {failed} ({failed/n*100:.0f}%)", flush=True) + print() + + # Status distribution + statuses = Counter(r["status"] for r in rslts) + print("Status distribution:", flush=True) + for s, c in sorted(statuses.items()): + print(f" {s:30s}: {c:3d}", flush=True) + print() + + # Shape distribution + shape_counts = Counter(r["exact_shape"] for r in rslts) + print("RRCShape distribution (exact):", flush=True) + for s, c in sorted(shape_counts.items(), key=lambda x: -x[1]): + print(f" {s:35s}: {c:3d} ({c/n*100:.0f}%)", flush=True) + print() + + # Unique hashes + u_matrices = len(set(r["matrix_hash"] for r in rslts)) + u_canon = len(set(r["canonical_hash"] for r in rslts)) + u_spectra = len(set(json.dumps(r["spectral_gap"]) for r in rslts)) + print(f"Unique matrix hashes: {u_matrices}/{n} ({u_matrices/n*100:.0f}%)", flush=True) + print(f"Unique canonical hashes: {u_canon}/{n} ({u_canon/n*100:.0f}%)", flush=True) + print(f"Unique spectral gaps: {u_spectra}/{n}", flush=True) + print() + + # Feature diversity + gaps = [r["spectral_gap"] for r in rslts if isinstance(r["spectral_gap"], (int, float))] + ranks = [r["rank_estimate"] for r in rslts if isinstance(r["rank_estimate"], int)] + lap0s = [r["laplacian_zero_count"] for r in rslts if isinstance(r["laplacian_zero_count"], int)] + print(f"Spectral gap: mean={sum(gaps)/len(gaps):.3f} range=[{min(gaps):.3f},{max(gaps):.3f}] uniq={len(set(gaps))}", flush=True) + print(f"Rank estimate: mean={sum(ranks)/len(ranks):.1f} range=[{min(ranks)},{max(ranks)}] uniq={len(set(ranks))}", flush=True) + print(f"Laplacian zero count: range=[{min(lap0s)},{max(lap0s)}] uniq={len(set(lap0s))}", flush=True) + print() + + # Verified vs failed spectral comparison + for label, fn in [("verified", lambda r: r["status"] == "verified"), + ("failed", lambda r: r["status"] != "verified")]: + subset = [r for r in rslts if fn(r)] + if len(subset) < 2: + continue + avg_gap = sum(r["spectral_gap"] for r in subset) / len(subset) + print(f"{label} (n={len(subset)}): avg_gap={avg_gap:.3f}", flush=True) + + # Write results JSONL + with open(results_path, "w") as f: + for row in rslts: + f.write(json.dumps(row) + "\n") + + # Write report + report = { + "n": n, + "verified": verified, + "failed": failed, + "statuses": dict(statuses), + "shape_distribution": dict(shape_counts), + "unique_matrix_hashes": u_matrices, + "unique_canonical_hashes": u_canon, + "unique_spectral_gaps": u_spectra, + "spectral_gap_stats": { + "mean": round(sum(gaps)/len(gaps), 4), + "min": round(min(gaps), 4), + "max": round(max(gaps), 4), + "unique": len(set(round(g, 6) for g in gaps)), + }, + "rank_stats": { + "mean": round(sum(ranks)/len(ranks), 2), + "min": min(ranks), + "max": max(ranks), + "unique": len(set(ranks)), + }, + "results": rslts, + } + with open(report_path, "w") as f: + json.dump(report, f, indent=2) + + print(f"Receipts: {receipts_path}", flush=True) + print(f"Results: {results_path}", flush=True) + print(f"Report: {report_path}", flush=True) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/shared-data/pist_canary_receipts.jsonl b/shared-data/pist_canary_receipts.jsonl new file mode 100644 index 00000000..92f80b64 --- /dev/null +++ b/shared-data/pist_canary_receipts.jsonl @@ -0,0 +1,42 @@ +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rfl_one", "equation_text": "rfl one", "normalized_equation": "one_rfl", "operators": [], "variables": ["rfl", "one"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n = n := by rfl", "proof_script": "theorem t (n : Nat) : n = n := by rfl", "imports": [], "dependencies": [], "source_hash": "2eb9f6a59233beb416395ad25d3a7e0211b824fc5c6c801ebc9a5bb3f62a2373", "environment_hash": "2026-05-26T07:04:40.496742+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 6933, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 37, "proof_chars": 37, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rfl_add", "equation_text": "rfl add", "normalized_equation": "add_rfl", "operators": [], "variables": ["rfl", "add"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n + 0 = n := by rfl", "proof_script": "theorem t (n : Nat) : n + 0 = n := by rfl", "imports": [], "dependencies": [], "source_hash": "22c02658d595ec0476ff1995168b381605e930801de2ebeba2b55b832a7e090a", "environment_hash": "2026-05-26T07:04:43.551803+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2658, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 41, "proof_chars": 41, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rfl_succ", "equation_text": "rfl succ", "normalized_equation": "rfl_succ", "operators": [], "variables": ["rfl", "succ"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n.succ = n.succ := by rfl", "proof_script": "theorem t (n : Nat) : n.succ = n.succ := by rfl", "imports": [], "dependencies": [], "source_hash": "ddd5d29d3dd1e40329ac7be84711110606576b827c3a84e6b6509be99042e1ca", "environment_hash": "2026-05-26T07:04:47.023868+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 3179, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 47, "proof_chars": 47, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "simp_add_zero", "equation_text": "simp add zero", "normalized_equation": "add_simp_zero", "operators": [], "variables": ["add", "zero", "simp"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n + 0 = n := by simp", "proof_script": "theorem t (n : Nat) : n + 0 = n := by simp", "imports": [], "dependencies": [], "source_hash": "efb25179cb114978eda7f987a9388e2949cb17627a5512edde87cd9d3366f244", "environment_hash": "2026-05-26T07:04:50.184553+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2491, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 42, "proof_chars": 42, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "simp_mul_one", "equation_text": "simp mul one", "normalized_equation": "mul_one_simp", "operators": [], "variables": ["mul", "one", "simp"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n * 1 = n := by simp", "proof_script": "theorem t (n : Nat) : n * 1 = n := by simp", "imports": [], "dependencies": [], "source_hash": "c0089d5d19cb00aa15510683a51ec87b58def6c5233d2a002ac6e946eec38be8", "environment_hash": "2026-05-26T07:04:53.674048+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 3048, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 42, "proof_chars": 42, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "simp_add_comm", "equation_text": "simp add comm", "normalized_equation": "add_comm_simp", "operators": [], "variables": ["add", "comm", "simp"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : a + b = b + a := by simp [add_comm]", "proof_script": "theorem t (a b : Nat) : a + b = b + a := by simp [add_comm]", "imports": [], "dependencies": [], "source_hash": "6eea1a572785dabf171f1fa04a26e8e643911bda3c289c1c2b7589e082748f7e", "environment_hash": "2026-05-26T07:04:56.590911+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2539, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 59, "proof_chars": 59, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "simp_add_assoc", "equation_text": "simp add assoc", "normalized_equation": "add_assoc_simp", "operators": [], "variables": ["assoc", "add", "simp"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b c : Nat) : (a + b) + c = a + (b + c) := by simp [add_assoc]", "proof_script": "theorem t (a b c : Nat) : (a + b) + c = a + (b + c) := by simp [add_assoc]", "imports": [], "dependencies": [], "source_hash": "bba6095c94ebaf9b4ada297727ed1a8f1e1a7657daf44738a5b56d238ae6dd0e", "environment_hash": "2026-05-26T07:04:59.147580+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2196, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 74, "proof_chars": 74, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "simp_mul_comm", "equation_text": "simp mul comm", "normalized_equation": "comm_mul_simp", "operators": [], "variables": ["mul", "comm", "simp"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : a * b = b * a := by simp [mul_comm]", "proof_script": "theorem t (a b : Nat) : a * b = b * a := by simp [mul_comm]", "imports": [], "dependencies": [], "source_hash": "c9db3bace941af4cf587ccc65acda72b3e82d2411f3ee3f450530410208c9569", "environment_hash": "2026-05-26T07:05:01.619450+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2124, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 59, "proof_chars": 59, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "omega_add", "equation_text": "omega add", "normalized_equation": "add_omega", "operators": [], "variables": ["add", "omega"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b c : Nat) : a + b + c = a + c + b := by omega", "proof_script": "theorem t (a b c : Nat) : a + b + c = a + c + b := by omega", "imports": [], "dependencies": [], "source_hash": "e5e03b1835a771571f0bb3ca99b4f38bd2779162fcbfc5a0510ce3457c2b8a1a", "environment_hash": "2026-05-26T07:05:03.946229+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2042, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 59, "proof_chars": 59, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "omega_mul", "equation_text": "omega mul", "normalized_equation": "mul_omega", "operators": [], "variables": ["mul", "omega"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : (a + b) * 2 = a*2 + b*2 := by omega", "proof_script": "theorem t (a b : Nat) : (a + b) * 2 = a*2 + b*2 := by omega", "imports": [], "dependencies": [], "source_hash": "a7737e85b1ccbd4a0b85ba6836c81e02669877ed433134e699a580e39df97625", "environment_hash": "2026-05-26T07:05:06.043353+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 1801, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 59, "proof_chars": 59, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "omega_ineq", "equation_text": "omega ineq", "normalized_equation": "ineq_omega", "operators": [], "variables": ["omega", "ineq"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) (h : a \u2264 b) : a + 1 \u2264 b + 1 := by omega", "proof_script": "theorem t (a b : Nat) (h : a \u2264 b) : a + 1 \u2264 b + 1 := by omega", "imports": [], "dependencies": [], "source_hash": "166370fcdff586c946fd291776c046865ddf3c55a338a7e5cf4c74d006ed06e3", "environment_hash": "2026-05-26T07:05:09.977301+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 3650, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 61, "proof_chars": 61, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "omega_mod", "equation_text": "omega mod", "normalized_equation": "mod_omega", "operators": [], "variables": ["omega", "mod"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a : Nat) : a % 2 < 2 := by omega", "proof_script": "theorem t (a : Nat) : a % 2 < 2 := by omega", "imports": [], "dependencies": [], "source_hash": "002bb6698e3e20497d0351dff4865cba42aa3a2c4a8841eb1d58824a7e0bb89f", "environment_hash": "2026-05-26T07:05:12.765953+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2491, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 43, "proof_chars": 43, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "omega_double", "equation_text": "omega double", "normalized_equation": "double_omega", "operators": [], "variables": ["omega", "double"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n + n = 2 * n := by omega", "proof_script": "theorem t (n : Nat) : n + n = 2 * n := by omega", "imports": [], "dependencies": [], "source_hash": "e919b215f798e5896c82730431d647b20c9bf009072d693602c176795bb08872", "environment_hash": "2026-05-26T07:05:16.072745+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2989, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 47, "proof_chars": 47, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "ring_sq", "equation_text": "ring sq", "normalized_equation": "ring_sq", "operators": [], "variables": ["ring", "sq"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (x y : Nat) : (x + y)^2 = x^2 + 2*x*y + y^2 := by nlinarith", "proof_script": "theorem t (x y : Nat) : (x + y)^2 = x^2 + 2*x*y + y^2 := by nlinarith", "imports": [], "dependencies": [], "source_hash": "3ac022380b181532654d377184b8ee39b42d3801205a690f1ee3785c62207f3c", "environment_hash": "2026-05-26T07:05:18.544426+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2129, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 69, "proof_chars": 69, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "ring_cube", "equation_text": "ring cube", "normalized_equation": "cube_ring", "operators": [], "variables": ["ring", "cube"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (x : Nat) : (x+1)^3 = x^3 + 3*x^2 + 3*x + 1 := by nlinarith", "proof_script": "theorem t (x : Nat) : (x+1)^3 = x^3 + 3*x^2 + 3*x + 1 := by nlinarith", "imports": [], "dependencies": [], "source_hash": "a889eba9fbad22397e4c371dc84fcf6fac29460cf05fe9f3564bb23936a5b747", "environment_hash": "2026-05-26T07:05:20.812533+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 1981, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 69, "proof_chars": 69, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "ring_expand", "equation_text": "ring expand", "normalized_equation": "expand_ring", "operators": [], "variables": ["expand", "ring"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : (a + b) * (a - b) = a^2 - b^2 := by omega", "proof_script": "theorem t (a b : Nat) : (a + b) * (a - b) = a^2 - b^2 := by omega", "imports": [], "dependencies": [], "source_hash": "50d7d00d3728a11c12e1456bafbacf8b4693e2e08bbee213103e9dbd5941a927", "environment_hash": "2026-05-26T07:05:23.770462+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2625, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 65, "proof_chars": 65, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "induct_add_zero", "equation_text": "induct add zero", "normalized_equation": "add_induct_zero", "operators": [], "variables": ["add", "zero", "induct"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : n + 0 = n := by induction n with k IH; rfl; simp [add_succ, IH]", "proof_script": "theorem t (n : Nat) : n + 0 = n := by induction n with k IH; rfl; simp [add_succ, IH]", "imports": [], "dependencies": [], "source_hash": "f9b7198b67b168ec39bb1530c3e85bb771ebe58030620cf76445942750c045e6", "environment_hash": "2026-05-26T07:05:27.078876+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2911, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 85, "proof_chars": 85, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "induct_add_succ", "equation_text": "induct add succ", "normalized_equation": "add_induct_succ", "operators": [], "variables": ["add", "succ", "induct"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (n m : Nat) : n + m.succ = (n + m).succ := by induction n with k IH; rfl; simp [add_succ, IH]", "proof_script": "theorem t (n m : Nat) : n + m.succ = (n + m).succ := by induction n with k IH; rfl; simp [add_succ, IH]", "imports": [], "dependencies": [], "source_hash": "e69e8b26359660beaac38538e3367fc00a89c5ce0761cda17ae2c81b41b0214a", "environment_hash": "2026-05-26T07:05:30.338345+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2713, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 103, "proof_chars": 103, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "induct_mul", "equation_text": "induct mul", "normalized_equation": "induct_mul", "operators": [], "variables": ["mul", "induct"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n m : Nat) : n * m = m * n := by induction n with k IH; simp; simp [mul_add, IH, add_comm, add_left_comm, add_assoc]", "proof_script": "theorem t (n m : Nat) : n * m = m * n := by induction n with k IH; simp; simp [mul_add, IH, add_comm, add_left_comm, add_assoc]", "imports": [], "dependencies": [], "source_hash": "6a8b09e11b16cfb98d2acdcb10340f966da6a10c6e40cebcbdacefaf44f7b4e0", "environment_hash": "2026-05-26T07:05:32.767739+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2068, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 127, "proof_chars": 127, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rw_add_comm", "equation_text": "rw add comm", "normalized_equation": "add_comm_rw", "operators": [], "variables": ["add", "rw", "comm"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : a + b = b + a := by rw [add_comm a b]", "proof_script": "theorem t (a b : Nat) : a + b = b + a := by rw [add_comm a b]", "imports": [], "dependencies": [], "source_hash": "50959668e0de82e8ee3b31f6440d9ebe50481e754bfc54c8ec584ddcf89162df", "environment_hash": "2026-05-26T07:05:35.189413+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2119, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 61, "proof_chars": 61, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rw_mul_comm", "equation_text": "rw mul comm", "normalized_equation": "comm_mul_rw", "operators": [], "variables": ["mul", "rw", "comm"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : a * b = b * a := by rw [mul_comm]", "proof_script": "theorem t (a b : Nat) : a * b = b * a := by rw [mul_comm]", "imports": [], "dependencies": [], "source_hash": "8dd01b69a6bffa2a232f04205a992f14ba3f79f83a05372e5ea6f4fd59f0b455", "environment_hash": "2026-05-26T07:05:37.878995+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2384, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 57, "proof_chars": 57, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "rw_add_assoc", "equation_text": "rw add assoc", "normalized_equation": "add_assoc_rw", "operators": [], "variables": ["assoc", "add", "rw"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (a b c : Nat) : a + b + c = c + b + a := by rw [add_comm a b, add_comm (a+b) c, add_comm b a]; rfl", "proof_script": "theorem t (a b c : Nat) : a + b + c = c + b + a := by rw [add_comm a b, add_comm (a+b) c, add_comm b a]; rfl", "imports": [], "dependencies": [], "source_hash": "555692a15d74dca0d81ded8b21d2a8a1bb24409e6d4db7366a716b91eb66a73d", "environment_hash": "2026-05-26T07:05:40.267007+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 1938, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 108, "proof_chars": 108, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "with_import_list", "equation_text": "with import list", "normalized_equation": "import_list_with", "operators": [], "variables": ["list", "import", "with"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "import Mathlib.Data.List.Basic\ntheorem t (l : List Nat) : l.reverse.reverse = l := by simp", "proof_script": "theorem t (l : List Nat) : l.reverse.reverse = l := by simp", "imports": ["Mathlib.Data.List.Basic"], "dependencies": ["Mathlib.Data.List.Basic"], "source_hash": "5d583ea6-4968-4b95-9a0a-90db64b7e375", "environment_hash": "2026-05-26T07:06:44.339154+00:00", "status": "timeout", "kernel_checked": false, "returncode": -1, "elapsed_ms": 60000, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 90, "proof_chars": 59, "dependency_count": 1, "import_count": 1, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "with_import_nat", "equation_text": "with import nat", "normalized_equation": "import_nat_with", "operators": [], "variables": ["import", "with", "nat"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "import Mathlib.Data.Nat.Basic\ntheorem t (a b : Nat) : a.gcd b = b.gcd a := Nat.gcd_comm a b", "proof_script": "theorem t (a b : Nat) : a.gcd b = b.gcd a := Nat.gcd_comm a b", "imports": ["Mathlib.Data.Nat.Basic"], "dependencies": ["Mathlib.Data.Nat.Basic"], "source_hash": "028e78b689bcf7872cf3a639298b25238c6e3d2e766df395a0761118745e223b", "environment_hash": "2026-05-26T07:06:57.612502+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 16798, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 91, "proof_chars": 61, "dependency_count": 1, "import_count": 1, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "with_import_int", "equation_text": "with import int", "normalized_equation": "import_int_with", "operators": [], "variables": ["import", "with", "int"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "import Mathlib.Data.Int.Basic\ntheorem t (a b : \u2124) : a + b = b + a := by omega", "proof_script": "theorem t (a b : \u2124) : a + b = b + a := by omega", "imports": ["Mathlib.Data.Int.Basic"], "dependencies": ["Mathlib.Data.Int.Basic"], "source_hash": "eaaabd69e5af6b5e64e1f77dec878e82bbac6bab80a976b1271d3f8ecdebc07e", "environment_hash": "2026-05-26T07:07:05.835735+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 7893, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 77, "proof_chars": 47, "dependency_count": 1, "import_count": 1, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "with_import_set", "equation_text": "with import set", "normalized_equation": "import_set_with", "operators": [], "variables": ["import", "with", "set"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "import Mathlib.Data.Set.Basic\ntheorem t (s : Set Nat) : s \u222a s = s := Set.union_self s", "proof_script": "theorem t (s : Set Nat) : s \u222a s = s := Set.union_self s", "imports": ["Mathlib.Data.Set.Basic"], "dependencies": ["Mathlib.Data.Set.Basic"], "source_hash": "135e40eb-3f0d-494b-bfa1-390d3b216e4e", "environment_hash": "2026-05-26T07:08:09.972964+00:00", "status": "timeout", "kernel_checked": false, "returncode": -1, "elapsed_ms": 60000, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 85, "proof_chars": 55, "dependency_count": 1, "import_count": 1, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "algebra_id", "equation_text": "algebra id", "normalized_equation": "algebra_id", "operators": [], "variables": ["algebra", "id"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (x : Nat) : x * 1 = x := by simp", "proof_script": "theorem t (x : Nat) : x * 1 = x := by simp", "imports": [], "dependencies": [], "source_hash": "649dffcb03e5fc917b53e5c72aaabb454b1d3f554030bb205b7db3d8bec72cbd", "environment_hash": "2026-05-26T07:08:13.461439+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 7056, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 42, "proof_chars": 42, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "algebra_distrib", "equation_text": "algebra distrib", "normalized_equation": "algebra_distrib", "operators": [], "variables": ["algebra", "distrib"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b c : Nat) : a * (b + c) = a * b + a * c := by omega", "proof_script": "theorem t (a b c : Nat) : a * (b + c) = a * b + a * c := by omega", "imports": [], "dependencies": [], "source_hash": "a9ae5c52840e562ace840a72fa7ae8b73a4584e51ba6dbc5d569b745de3f82b3", "environment_hash": "2026-05-26T07:08:16.640999+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2823, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 65, "proof_chars": 65, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "algebra_sq_diff", "equation_text": "algebra sq diff", "normalized_equation": "algebra_diff_sq", "operators": [], "variables": ["algebra", "sq", "diff"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (x y : Nat) : x^2 - y^2 = (x - y) * (x + y) := by omega", "proof_script": "theorem t (x y : Nat) : x^2 - y^2 = (x - y) * (x + y) := by omega", "imports": [], "dependencies": [], "source_hash": "d421b2a324a40e0708fa5bda0ab0ff8635ed3dfc391039008b2998b8d2aaa7a3", "environment_hash": "2026-05-26T07:08:19.425076+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2497, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 65, "proof_chars": 65, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "logic_and", "equation_text": "logic and", "normalized_equation": "and_logic", "operators": [], "variables": ["logic", "and"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (A B : Prop) : A \u2227 B \u2192 A := by intro h; exact h.1", "proof_script": "theorem t (A B : Prop) : A \u2227 B \u2192 A := by intro h; exact h.1", "imports": [], "dependencies": [], "source_hash": "1f3ccaf31a3bebda25e8d91a537fa431529bc85c2f77bc26b01c4b6d6ba5db2c", "environment_hash": "2026-05-26T07:08:22.317543+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2480, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 59, "proof_chars": 59, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "logic_or", "equation_text": "logic or", "normalized_equation": "logic_or", "operators": [], "variables": ["logic", "or"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (A B : Prop) : A \u2228 B \u2192 B \u2228 A := by intro h; cases h; right; exact h; left; exact h", "proof_script": "theorem t (A B : Prop) : A \u2228 B \u2192 B \u2228 A := by intro h; cases h; right; exact h; left; exact h", "imports": [], "dependencies": [], "source_hash": "a2174f6ba40eeff557ca78145ffcc3a367b3682bc7fc41d428b65ddc1739de31", "environment_hash": "2026-05-26T07:08:24.920977+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2313, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 92, "proof_chars": 92, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "logic_not_not", "equation_text": "logic not not", "normalized_equation": "logic_not_not", "operators": [], "variables": ["logic", "not"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 0.9183}, "domain": "unknown", "theorem_statement": "theorem t (P : Prop) : P \u2192 \u00ac\u00acP := by intro hp hnp; exact hnp hp", "proof_script": "theorem t (P : Prop) : P \u2192 \u00ac\u00acP := by intro hp hnp; exact hnp hp", "imports": [], "dependencies": [], "source_hash": "050d95459a1cf9d98b30f3527689dc2f1370651fb27c05ab0542de2941003427", "environment_hash": "2026-05-26T07:08:28.089960+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2869, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 63, "proof_chars": 63, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "logic_impl_trans", "equation_text": "logic impl trans", "normalized_equation": "impl_logic_trans", "operators": [], "variables": ["logic", "trans", "impl"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (A B C : Prop) : (A \u2192 B) \u2192 (B \u2192 C) \u2192 (A \u2192 C) := by intro h1 h2 ha; exact h2 (h1 ha)", "proof_script": "theorem t (A B C : Prop) : (A \u2192 B) \u2192 (B \u2192 C) \u2192 (A \u2192 C) := by intro h1 h2 ha; exact h2 (h1 ha)", "imports": [], "dependencies": [], "source_hash": "68857ebebe49bc03f579829e6ea9f1c338e683cc190f36cc6b78d5fb653a5a46", "environment_hash": "2026-05-26T07:08:30.581772+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2069, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 93, "proof_chars": 93, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "order_refl", "equation_text": "order refl", "normalized_equation": "order_refl", "operators": [], "variables": ["refl", "order"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a : Nat) : a \u2264 a := Nat.le_refl a", "proof_script": "theorem t (a : Nat) : a \u2264 a := Nat.le_refl a", "imports": [], "dependencies": [], "source_hash": "4451970253c55225249e60e79a2c463554d742f0d2f31ab503c742b14b857626", "environment_hash": "2026-05-26T07:08:33.035101+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2074, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 44, "proof_chars": 44, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "order_trans", "equation_text": "order trans", "normalized_equation": "order_trans", "operators": [], "variables": ["trans", "order"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b c : Nat) (h1 : a \u2264 b) (h2 : b \u2264 c) : a \u2264 c := Nat.le_trans h1 h2", "proof_script": "theorem t (a b c : Nat) (h1 : a \u2264 b) (h2 : b \u2264 c) : a \u2264 c := Nat.le_trans h1 h2", "imports": [], "dependencies": [], "source_hash": "eddfed86b40133580f4ee090cf5b3283eee4b49b7696fa9f0f047543455c5866", "environment_hash": "2026-05-26T07:08:35.378814+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 2054, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 79, "proof_chars": 79, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "order_antisymm", "equation_text": "order antisymm", "normalized_equation": "antisymm_order", "operators": [], "variables": ["antisymm", "order"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) (h1 : a \u2264 b) (h2 : b \u2264 a) : a = b := Nat.le_antisymm h1 h2", "proof_script": "theorem t (a b : Nat) (h1 : a \u2264 b) (h2 : b \u2264 a) : a = b := Nat.le_antisymm h1 h2", "imports": [], "dependencies": [], "source_hash": "fc360c68b6c6689532747e1dd5cea507ba19d27554af137ca52406638e8662aa", "environment_hash": "2026-05-26T07:08:37.473978+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 1697, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 80, "proof_chars": 80, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "expect_fail_type_mismatch", "equation_text": "expect fail type mismatch", "normalized_equation": "expect_fail_mismatch_type", "operators": [], "variables": ["fail", "mismatch", "expect", "type"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 7, "depth": 4, "branching_factor": 1, "symbol_entropy": 2.0}, "domain": "unknown", "theorem_statement": "theorem t : Nat \u2192 String := \u03bb n => n", "proof_script": "theorem t : Nat \u2192 String := \u03bb n => n", "imports": [], "dependencies": [], "source_hash": "d2b89c30b2bda98be6007f4f3b2c5be60fdce7f90389881cd90bc6717ccd50fd", "environment_hash": "2026-05-26T07:08:39.503463+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 1638, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 36, "proof_chars": 36, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 4}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "expect_fail_unsat", "equation_text": "expect fail unsat", "normalized_equation": "expect_fail_unsat", "operators": [], "variables": ["fail", "expect", "unsat"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t (x : Nat) : x < x := by omega", "proof_script": "theorem t (x : Nat) : x < x := by omega", "imports": [], "dependencies": [], "source_hash": "33046326f037bf6e04615b517b9e7103947ecb57a39ae8f15720b04f8f49d402", "environment_hash": "2026-05-26T07:08:42.308024+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2464, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 39, "proof_chars": 39, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "expect_fail_axiom", "equation_text": "expect fail axiom", "normalized_equation": "axiom_expect_fail", "operators": [], "variables": ["fail", "axiom", "expect"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 5, "depth": 3, "branching_factor": 1, "symbol_entropy": 1.585}, "domain": "unknown", "theorem_statement": "theorem t : 1 = 0 := by native_decide", "proof_script": "theorem t : 1 = 0 := by native_decide", "imports": [], "dependencies": [], "source_hash": "ce18b9609d303aa9916c645780867424c1180632a645dc5783815d6a7cda471d", "environment_hash": "2026-05-26T07:08:44.806237+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 2076, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 37, "proof_chars": 37, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 3}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "expect_fail_timeout_like", "equation_text": "expect fail timeout like", "normalized_equation": "expect_fail_like_timeout", "operators": [], "variables": ["fail", "timeout", "expect", "like"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 7, "depth": 4, "branching_factor": 1, "symbol_entropy": 2.0}, "domain": "unknown", "theorem_statement": "theorem t (a b : Nat) : a^10 + b^10 = (a+b)^10 := by nlinarith", "proof_script": "theorem t (a b : Nat) : a^10 + b^10 = (a+b)^10 := by nlinarith", "imports": [], "dependencies": [], "source_hash": "c53ad7593bd30250685a22d696f8df307ede2614051b09119c731874e72f32bb", "environment_hash": "2026-05-26T07:08:47.046562+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 1837, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 62, "proof_chars": 62, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 4}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "complex_fib", "equation_text": "complex fib", "normalized_equation": "complex_fib", "operators": [], "variables": ["fib", "complex"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "def fib : Nat \u2192 Nat | 0 => 0 | 1 => 1 | n+2 => fib (n+1) + fib n\ntheorem t (n : Nat) : fib (n+2) = fib (n+1) + fib n := by rfl", "proof_script": "theorem t (n : Nat) : fib (n+2) = fib (n+1) + fib n := by rfl", "imports": [], "dependencies": [], "source_hash": "2948b3fa1252d481d7e0c71e2a99f66c48b34e6b3756b74e08e19de1ae2acd74", "environment_hash": "2026-05-26T07:08:49.068247+00:00", "status": "verified_empty_output", "kernel_checked": true, "returncode": 0, "elapsed_ms": 1737, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 126, "proof_chars": 61, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} +{"receipt_version": "rrc-proof-receipt-v2", "theorem_name": "complex_sum", "equation_text": "complex sum", "normalized_equation": "complex_sum", "operators": [], "variables": ["complex", "sum"], "constants": [], "operator_counts": {"adjusted": 0, "overflow": 0, "gate": 0, "offload": 0, "mapping": 0, "projection": 0, "loss": 0}, "ast_metrics": {"node_count": 3, "depth": 2, "branching_factor": 1, "symbol_entropy": 1.0}, "domain": "unknown", "theorem_statement": "theorem t (n : Nat) : \u2211 k in Finset.range n, k = n*(n-1)/2 := by sorry", "proof_script": "theorem t (n : Nat) : \u2211 k in Finset.range n, k = n*(n-1)/2 := by sorry", "imports": [], "dependencies": [], "source_hash": "8dbeb0edbae0dce8f194707e612ebc4de2f3e8439a998bb53c4a2eabe35d1e07", "environment_hash": "2026-05-26T07:08:51.187621+00:00", "status": "failed", "kernel_checked": false, "returncode": 1, "elapsed_ms": 1779, "proof_metrics": {"tactic_count": 2, "dependency_count": 1, "rewrite_count": 2, "simp_count": 4}, "metrics": {"statement_chars": 70, "proof_chars": 70, "dependency_count": 1, "import_count": 0, "tactic_count": 2, "ast_depth_estimate": 2}} diff --git a/shared-data/pist_canary_report.json b/shared-data/pist_canary_report.json new file mode 100644 index 00000000..7c9393e5 --- /dev/null +++ b/shared-data/pist_canary_report.json @@ -0,0 +1,703 @@ +{ + "n": 42, + "verified": 0, + "failed": 42, + "statuses": { + "verified_empty_output": 20, + "failed": 20, + "timeout": 2 + }, + "shape_distribution": { + "LogogramProjection": 41, + "CadForceProbeReceipt": 1 + }, + "unique_matrix_hashes": 42, + "unique_canonical_hashes": 42, + "unique_spectral_gaps": 42, + "spectral_gap_stats": { + "mean": 0.4638, + "min": 0.0955, + "max": 0.799, + "unique": 42 + }, + "rank_stats": { + "mean": 7.0, + "min": 4, + "max": 8, + "unique": 5 + }, + "results": [ + { + "name": "rfl_one", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 6933, + "wall_s": 7.46, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.7989642225649622, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "e972255be8553c2f", + "canonical_hash": "15606911ec0fae46" + }, + { + "name": "rfl_add", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2658, + "wall_s": 2.98, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.21697971970381058, + "rank_estimate": 8, + "laplacian_zero_count": 2, + "matrix_hash": "c5a3f1a7e4d55eb2", + "canonical_hash": "4d20339383eac392" + }, + { + "name": "rfl_succ", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 3179, + "wall_s": 3.54, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.24102358850715017, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "89facaf2f55a81c3", + "canonical_hash": "5bf8f402d288ac2a" + }, + { + "name": "simp_add_zero", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2491, + "wall_s": 3.16, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4476263686375421, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "9af30dd4d9acf703", + "canonical_hash": "dd67be6dfb8f0656" + }, + { + "name": "simp_mul_one", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 3048, + "wall_s": 3.44, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.45606180509465283, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "1d8562f6a0809240", + "canonical_hash": "f54897bb87ad893c" + }, + { + "name": "simp_add_comm", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2539, + "wall_s": 2.93, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4892160061620842, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "0c845b9f93164cd7", + "canonical_hash": "d3602b2addf1c966" + }, + { + "name": "simp_add_assoc", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2196, + "wall_s": 2.57, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.6116005124315291, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "2a571dc55d2d4705", + "canonical_hash": "d1704884b4696966" + }, + { + "name": "simp_mul_comm", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2124, + "wall_s": 2.41, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5077856092842012, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "49e206ad56bf6e66", + "canonical_hash": "d129acb91aca7e32" + }, + { + "name": "omega_add", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2042, + "wall_s": 2.33, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.6669957997734307, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "a4bdf366496aaeaa", + "canonical_hash": "c849ee66a0d0222b" + }, + { + "name": "omega_mul", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 1801, + "wall_s": 2.1, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.2949106822091147, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "9458f294272e7718", + "canonical_hash": "44ccec5c7500e01b" + }, + { + "name": "omega_ineq", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 3650, + "wall_s": 3.94, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.46361308277039853, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "0b105bd1a9bf44c0", + "canonical_hash": "6dd1841c6c40c7ff" + }, + { + "name": "omega_mod", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2491, + "wall_s": 2.79, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.453401625662083, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "19fc159d2f6ffb7e", + "canonical_hash": "b6b79202bae79cf4" + }, + { + "name": "omega_double", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2989, + "wall_s": 3.35, + "proxy_shape": "LogogramProjection", + "exact_shape": "CadForceProbeReceipt", + "zmp": 8, + "spectral_gap": 0.2500000000000002, + "rank_estimate": 4, + "laplacian_zero_count": 3, + "matrix_hash": "95a65ca154e5b36f", + "canonical_hash": "fc2841229e2d4798" + }, + { + "name": "ring_sq", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2129, + "wall_s": 2.42, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5791888552040121, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "9b238c3955946a74", + "canonical_hash": "1e6039284c0ffcb1" + }, + { + "name": "ring_cube", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 1981, + "wall_s": 2.26, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.0954915028125265, + "rank_estimate": 6, + "laplacian_zero_count": 1, + "matrix_hash": "06106e22c8f38385", + "canonical_hash": "c45c6a10ae4f4866" + }, + { + "name": "ring_expand", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2625, + "wall_s": 3.07, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4582409031818631, + "rank_estimate": 6, + "laplacian_zero_count": 3, + "matrix_hash": "67a0358548753e92", + "canonical_hash": "ef820d130c6f70d1" + }, + { + "name": "induct_add_zero", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2911, + "wall_s": 3.2, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.6200850464851544, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "e115e9fc7f456738", + "canonical_hash": "4b72e4615fb340a4" + }, + { + "name": "induct_add_succ", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2713, + "wall_s": 3.27, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4827579484434103, + "rank_estimate": 6, + "laplacian_zero_count": 1, + "matrix_hash": "336b7a79eb78369f", + "canonical_hash": "2df162f21af7b508" + }, + { + "name": "induct_mul", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2068, + "wall_s": 2.42, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.7642549759732272, + "rank_estimate": 6, + "laplacian_zero_count": 1, + "matrix_hash": "440715f056b3cbe5", + "canonical_hash": "6560b01c5127eade" + }, + { + "name": "rw_add_comm", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2119, + "wall_s": 2.42, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4845558951823607, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "c066f22b24f4892d", + "canonical_hash": "48392c6cc57070e0" + }, + { + "name": "rw_mul_comm", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2384, + "wall_s": 2.75, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.3722382750921264, + "rank_estimate": 6, + "laplacian_zero_count": 1, + "matrix_hash": "470b7550864e341b", + "canonical_hash": "26029a558bc27343" + }, + { + "name": "rw_add_assoc", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 1938, + "wall_s": 2.32, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5050147876303135, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "ab4877c42ae57039", + "canonical_hash": "7312850438c413f8" + }, + { + "name": "with_import_list", + "status": "timeout", + "ok": false, + "returncode": -1, + "elapsed_ms": 60000, + "wall_s": 60.0, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.41327312243014713, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "5b927f14265813ff", + "canonical_hash": "4a58f46135d9d8ab" + }, + { + "name": "with_import_nat", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 16798, + "wall_s": 17.29, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5140272979215483, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "0687a04940d0865e", + "canonical_hash": "bf757458b34ac958" + }, + { + "name": "with_import_int", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 7893, + "wall_s": 8.28, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.6745494714753261, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "1ab6b158de5b5c80", + "canonical_hash": "4fb7b38b09d247ba" + }, + { + "name": "with_import_set", + "status": "timeout", + "ok": false, + "returncode": -1, + "elapsed_ms": 60000, + "wall_s": 60.0, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.3870982940915625, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "9ffcc7f88f7a16ba", + "canonical_hash": "0ae57aadd4c042ed" + }, + { + "name": "algebra_id", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 7056, + "wall_s": 7.51, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.3813455199145743, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "a9e658aed67be75c", + "canonical_hash": "e2a8458d9364e041" + }, + { + "name": "algebra_distrib", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2823, + "wall_s": 3.17, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.2280837638408919, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "264ab38889f15535", + "canonical_hash": "47fd7989e14eddd6" + }, + { + "name": "algebra_sq_diff", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2497, + "wall_s": 2.83, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.2568260701927592, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "ed0ad05343300cf2", + "canonical_hash": "42103cde29fc1573" + }, + { + "name": "logic_and", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2480, + "wall_s": 2.84, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.31174490092936696, + "rank_estimate": 8, + "laplacian_zero_count": 2, + "matrix_hash": "ed2cff9b1f092f63", + "canonical_hash": "7a4a1e363ed7550e" + }, + { + "name": "logic_or", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2313, + "wall_s": 2.61, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4046292057003976, + "rank_estimate": 5, + "laplacian_zero_count": 3, + "matrix_hash": "650ad6926258fd72", + "canonical_hash": "4b3c4c4579d47091" + }, + { + "name": "logic_not_not", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2869, + "wall_s": 3.28, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5653913733843512, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "964984ef71bf8251", + "canonical_hash": "b6b65f1c8a76bf34" + }, + { + "name": "logic_impl_trans", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2069, + "wall_s": 2.46, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.3086539686847869, + "rank_estimate": 6, + "laplacian_zero_count": 3, + "matrix_hash": "dadcc20635993263", + "canonical_hash": "51f19a61923e8fe8" + }, + { + "name": "order_refl", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2074, + "wall_s": 2.37, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.7090819818514208, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "88297640e051c8fc", + "canonical_hash": "7f9feb2e0260ddda" + }, + { + "name": "order_trans", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 2054, + "wall_s": 2.36, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.3338234407935299, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "a5babfde689147f5", + "canonical_hash": "35bcccd450148146" + }, + { + "name": "order_antisymm", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 1697, + "wall_s": 2.09, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.386535339989764, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "3d4342dd660ae096", + "canonical_hash": "f9e503429176eea0" + }, + { + "name": "expect_fail_type_mismatch", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 1638, + "wall_s": 2.01, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.7173625914728612, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "249723db36d51a4e", + "canonical_hash": "d23f4b7f76a40ffc" + }, + { + "name": "expect_fail_unsat", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2464, + "wall_s": 2.8, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.38658207358333463, + "rank_estimate": 6, + "laplacian_zero_count": 2, + "matrix_hash": "1e1de314ac94ef6c", + "canonical_hash": "5407c7234993fe12" + }, + { + "name": "expect_fail_axiom", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 2076, + "wall_s": 2.5, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.4476740725182331, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "fc1dbab616542252", + "canonical_hash": "15e7305a7c08b019" + }, + { + "name": "expect_fail_timeout_like", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 1837, + "wall_s": 2.24, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.49083905778708004, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "cfccc120357016d7", + "canonical_hash": "075395d5ef3cb547" + }, + { + "name": "complex_fib", + "status": "verified_empty_output", + "ok": true, + "returncode": 0, + "elapsed_ms": 1737, + "wall_s": 2.04, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.5191665463113263, + "rank_estimate": 7, + "laplacian_zero_count": 1, + "matrix_hash": "1855ddc075548ff8", + "canonical_hash": "aedf113a861ee6ce" + }, + { + "name": "complex_sum", + "status": "failed", + "ok": false, + "returncode": 1, + "elapsed_ms": 1779, + "wall_s": 2.09, + "proxy_shape": "LogogramProjection", + "exact_shape": "LogogramProjection", + "zmp": 8, + "spectral_gap": 0.7837231554643304, + "rank_estimate": 8, + "laplacian_zero_count": 1, + "matrix_hash": "98e2aedb40570b4d", + "canonical_hash": "06885d17a161dd31" + } + ] +} \ No newline at end of file diff --git a/shared-data/pist_canary_results.jsonl b/shared-data/pist_canary_results.jsonl new file mode 100644 index 00000000..daa5ad62 --- /dev/null +++ b/shared-data/pist_canary_results.jsonl @@ -0,0 +1,42 @@ +{"name": "rfl_one", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 6933, "wall_s": 7.46, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.7989642225649622, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "e972255be8553c2f", "canonical_hash": "15606911ec0fae46"} +{"name": "rfl_add", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2658, "wall_s": 2.98, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.21697971970381058, "rank_estimate": 8, "laplacian_zero_count": 2, "matrix_hash": "c5a3f1a7e4d55eb2", "canonical_hash": "4d20339383eac392"} +{"name": "rfl_succ", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 3179, "wall_s": 3.54, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.24102358850715017, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "89facaf2f55a81c3", "canonical_hash": "5bf8f402d288ac2a"} +{"name": "simp_add_zero", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2491, "wall_s": 3.16, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4476263686375421, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "9af30dd4d9acf703", "canonical_hash": "dd67be6dfb8f0656"} +{"name": "simp_mul_one", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 3048, "wall_s": 3.44, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.45606180509465283, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "1d8562f6a0809240", "canonical_hash": "f54897bb87ad893c"} +{"name": "simp_add_comm", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2539, "wall_s": 2.93, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4892160061620842, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "0c845b9f93164cd7", "canonical_hash": "d3602b2addf1c966"} +{"name": "simp_add_assoc", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2196, "wall_s": 2.57, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.6116005124315291, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "2a571dc55d2d4705", "canonical_hash": "d1704884b4696966"} +{"name": "simp_mul_comm", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2124, "wall_s": 2.41, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5077856092842012, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "49e206ad56bf6e66", "canonical_hash": "d129acb91aca7e32"} +{"name": "omega_add", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2042, "wall_s": 2.33, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.6669957997734307, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "a4bdf366496aaeaa", "canonical_hash": "c849ee66a0d0222b"} +{"name": "omega_mul", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 1801, "wall_s": 2.1, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.2949106822091147, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "9458f294272e7718", "canonical_hash": "44ccec5c7500e01b"} +{"name": "omega_ineq", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 3650, "wall_s": 3.94, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.46361308277039853, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "0b105bd1a9bf44c0", "canonical_hash": "6dd1841c6c40c7ff"} +{"name": "omega_mod", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2491, "wall_s": 2.79, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.453401625662083, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "19fc159d2f6ffb7e", "canonical_hash": "b6b79202bae79cf4"} +{"name": "omega_double", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2989, "wall_s": 3.35, "proxy_shape": "LogogramProjection", "exact_shape": "CadForceProbeReceipt", "zmp": 8, "spectral_gap": 0.2500000000000002, "rank_estimate": 4, "laplacian_zero_count": 3, "matrix_hash": "95a65ca154e5b36f", "canonical_hash": "fc2841229e2d4798"} +{"name": "ring_sq", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2129, "wall_s": 2.42, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5791888552040121, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "9b238c3955946a74", "canonical_hash": "1e6039284c0ffcb1"} +{"name": "ring_cube", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 1981, "wall_s": 2.26, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.0954915028125265, "rank_estimate": 6, "laplacian_zero_count": 1, "matrix_hash": "06106e22c8f38385", "canonical_hash": "c45c6a10ae4f4866"} +{"name": "ring_expand", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2625, "wall_s": 3.07, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4582409031818631, "rank_estimate": 6, "laplacian_zero_count": 3, "matrix_hash": "67a0358548753e92", "canonical_hash": "ef820d130c6f70d1"} +{"name": "induct_add_zero", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2911, "wall_s": 3.2, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.6200850464851544, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "e115e9fc7f456738", "canonical_hash": "4b72e4615fb340a4"} +{"name": "induct_add_succ", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2713, "wall_s": 3.27, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4827579484434103, "rank_estimate": 6, "laplacian_zero_count": 1, "matrix_hash": "336b7a79eb78369f", "canonical_hash": "2df162f21af7b508"} +{"name": "induct_mul", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2068, "wall_s": 2.42, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.7642549759732272, "rank_estimate": 6, "laplacian_zero_count": 1, "matrix_hash": "440715f056b3cbe5", "canonical_hash": "6560b01c5127eade"} +{"name": "rw_add_comm", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2119, "wall_s": 2.42, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4845558951823607, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "c066f22b24f4892d", "canonical_hash": "48392c6cc57070e0"} +{"name": "rw_mul_comm", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2384, "wall_s": 2.75, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.3722382750921264, "rank_estimate": 6, "laplacian_zero_count": 1, "matrix_hash": "470b7550864e341b", "canonical_hash": "26029a558bc27343"} +{"name": "rw_add_assoc", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 1938, "wall_s": 2.32, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5050147876303135, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "ab4877c42ae57039", "canonical_hash": "7312850438c413f8"} +{"name": "with_import_list", "status": "timeout", "ok": false, "returncode": -1, "elapsed_ms": 60000, "wall_s": 60.0, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.41327312243014713, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "5b927f14265813ff", "canonical_hash": "4a58f46135d9d8ab"} +{"name": "with_import_nat", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 16798, "wall_s": 17.29, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5140272979215483, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "0687a04940d0865e", "canonical_hash": "bf757458b34ac958"} +{"name": "with_import_int", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 7893, "wall_s": 8.28, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.6745494714753261, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "1ab6b158de5b5c80", "canonical_hash": "4fb7b38b09d247ba"} +{"name": "with_import_set", "status": "timeout", "ok": false, "returncode": -1, "elapsed_ms": 60000, "wall_s": 60.0, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.3870982940915625, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "9ffcc7f88f7a16ba", "canonical_hash": "0ae57aadd4c042ed"} +{"name": "algebra_id", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 7056, "wall_s": 7.51, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.3813455199145743, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "a9e658aed67be75c", "canonical_hash": "e2a8458d9364e041"} +{"name": "algebra_distrib", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2823, "wall_s": 3.17, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.2280837638408919, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "264ab38889f15535", "canonical_hash": "47fd7989e14eddd6"} +{"name": "algebra_sq_diff", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2497, "wall_s": 2.83, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.2568260701927592, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "ed0ad05343300cf2", "canonical_hash": "42103cde29fc1573"} +{"name": "logic_and", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2480, "wall_s": 2.84, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.31174490092936696, "rank_estimate": 8, "laplacian_zero_count": 2, "matrix_hash": "ed2cff9b1f092f63", "canonical_hash": "7a4a1e363ed7550e"} +{"name": "logic_or", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2313, "wall_s": 2.61, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4046292057003976, "rank_estimate": 5, "laplacian_zero_count": 3, "matrix_hash": "650ad6926258fd72", "canonical_hash": "4b3c4c4579d47091"} +{"name": "logic_not_not", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2869, "wall_s": 3.28, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5653913733843512, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "964984ef71bf8251", "canonical_hash": "b6b65f1c8a76bf34"} +{"name": "logic_impl_trans", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2069, "wall_s": 2.46, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.3086539686847869, "rank_estimate": 6, "laplacian_zero_count": 3, "matrix_hash": "dadcc20635993263", "canonical_hash": "51f19a61923e8fe8"} +{"name": "order_refl", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2074, "wall_s": 2.37, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.7090819818514208, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "88297640e051c8fc", "canonical_hash": "7f9feb2e0260ddda"} +{"name": "order_trans", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 2054, "wall_s": 2.36, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.3338234407935299, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "a5babfde689147f5", "canonical_hash": "35bcccd450148146"} +{"name": "order_antisymm", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 1697, "wall_s": 2.09, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.386535339989764, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "3d4342dd660ae096", "canonical_hash": "f9e503429176eea0"} +{"name": "expect_fail_type_mismatch", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 1638, "wall_s": 2.01, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.7173625914728612, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "249723db36d51a4e", "canonical_hash": "d23f4b7f76a40ffc"} +{"name": "expect_fail_unsat", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2464, "wall_s": 2.8, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.38658207358333463, "rank_estimate": 6, "laplacian_zero_count": 2, "matrix_hash": "1e1de314ac94ef6c", "canonical_hash": "5407c7234993fe12"} +{"name": "expect_fail_axiom", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 2076, "wall_s": 2.5, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.4476740725182331, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "fc1dbab616542252", "canonical_hash": "15e7305a7c08b019"} +{"name": "expect_fail_timeout_like", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 1837, "wall_s": 2.24, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.49083905778708004, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "cfccc120357016d7", "canonical_hash": "075395d5ef3cb547"} +{"name": "complex_fib", "status": "verified_empty_output", "ok": true, "returncode": 0, "elapsed_ms": 1737, "wall_s": 2.04, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.5191665463113263, "rank_estimate": 7, "laplacian_zero_count": 1, "matrix_hash": "1855ddc075548ff8", "canonical_hash": "aedf113a861ee6ce"} +{"name": "complex_sum", "status": "failed", "ok": false, "returncode": 1, "elapsed_ms": 1779, "wall_s": 2.09, "proxy_shape": "LogogramProjection", "exact_shape": "LogogramProjection", "zmp": 8, "spectral_gap": 0.7837231554643304, "rank_estimate": 8, "laplacian_zero_count": 1, "matrix_hash": "98e2aedb40570b4d", "canonical_hash": "06885d17a161dd31"}