mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(pist): canary batch — 42 real Lean theorems through full pipeline
- 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.
This commit is contained in:
Brandon Schneider
parent
bfce0f70bf
commit
e7525fb6f4
4 changed files with 1159 additions and 0 deletions
372
4-Infrastructure/shim/pist_canary_batch.py
Normal file
372
4-Infrastructure/shim/pist_canary_batch.py
Normal file
|
|
@ -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())
|
||||
42
shared-data/pist_canary_receipts.jsonl
Normal file
42
shared-data/pist_canary_receipts.jsonl
Normal file
|
|
@ -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}}
|
||||
703
shared-data/pist_canary_report.json
Normal file
703
shared-data/pist_canary_report.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
]
|
||||
}
|
||||
42
shared-data/pist_canary_results.jsonl
Normal file
42
shared-data/pist_canary_results.jsonl
Normal file
|
|
@ -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"}
|
||||
Loading…
Add table
Reference in a new issue