diff --git a/4-Infrastructure/shim/lean_trace_bridge_v2.py b/4-Infrastructure/shim/lean_trace_bridge_v2.py index fafacd7f..9e034f38 100644 --- a/4-Infrastructure/shim/lean_trace_bridge_v2.py +++ b/4-Infrastructure/shim/lean_trace_bridge_v2.py @@ -46,8 +46,19 @@ def instrument_theorem(code: str) -> tuple[str, list[str]]: if by_start < 0: return code, [] - # header is everything up to and including ':= by' or '= by' - header = code[:by_start].rstrip() + # header is everything up to ':= by' or '= by' + raw_header = code[:by_start].strip() + + # Strip import lines from the header (they'll be placed at the top) + header_parts = [] + header_imports = [] + for line in raw_header.split("\n"): + if line.strip().startswith("import "): + header_imports.append(line.strip()) + else: + header_parts.append(line.strip()) + header = "\n".join(header_parts) + if header.endswith(":=") or header.endswith("="): header += " by" elif ":" in code[:by_start]: @@ -85,7 +96,19 @@ def instrument_theorem(code: str) -> tuple[str, list[str]]: tags.append(atag) instrumented = "\n".join(lines) - full = TRACE_PREAMBLE + "\n" + instrumented + + # Extract existing imports from the original code and place them first + existing_imports = header_imports[:] # imports from the header + for line in code.split("\n"): + stripped = line.strip() + if stripped.startswith("import ") and stripped not in existing_imports: + existing_imports.append(stripped) + + if existing_imports: + full = "\n".join(existing_imports) + "\n" + TRACE_PREAMBLE + "\n" + instrumented + else: + full = TRACE_PREAMBLE + "\n" + instrumented + return full, tags diff --git a/shared-data/pist_trace_scaled_vectors.jsonl b/shared-data/pist_trace_scaled_vectors.jsonl new file mode 100644 index 00000000..54633366 --- /dev/null +++ b/shared-data/pist_trace_scaled_vectors.jsonl @@ -0,0 +1,57 @@ +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_one", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_add", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_succ", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "simp_add_zero", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "simp_mul_one", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_add_comm", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_add_assoc", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_mul_comm", "status": "failed"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_add", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_mul", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_ineq", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_mod", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_double", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_sq", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_cube", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_expand", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "induct_add_zero", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "induct_add_succ", "status": "failed"} +{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_mul", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_add_comm", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_mul_comm", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_add_assoc", "status": "failed"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "with_import_list", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "with_import_int", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "algebra_id", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "algebra_distrib", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "algebra_sq_diff", "status": "failed"} +{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_and", "status": "verified"} +{"matrix_size": 12, "rank": 11, "density": 0.076389, "trace": 0, "frobenius_norm": 3.316625, "adjacency_eigenvalue_max": 0.970942, "adjacency_eigenvalue_second": 2.730245, "spectral_gap": -1.759304, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_or", "status": "failed"} +{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_not_not", "status": "verified"} +{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_impl_trans", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_unsat", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_axiom", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_timeout_like", "status": "failed"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "complex_fib", "status": "verified"} +{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_eq", "status": "verified"} +{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_mixed", "status": "verified"} +{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_3step", "status": "verified"} +{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_then_omega", "status": "failed"} +{"matrix_size": 7, "rank": 6, "density": 0.122449, "trace": 0, "frobenius_norm": 2.44949, "adjacency_eigenvalue_max": 0.920991, "adjacency_eigenvalue_second": 2.673763, "spectral_gap": -1.752772, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "cases_or_swap", "status": "failed"} +{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "cases_and_elim", "status": "verified"} +{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "constructor_example", "status": "verified"} +{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "apply_chain", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_chain_ineq", "status": "verified"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_reorder_sum", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "omega_distrib", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "omega_chain_unsat", "status": "failed"} +{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_mul_zero", "status": "failed"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_factorial", "status": "verified"} +{"matrix_size": 8, "rank": 7, "density": 0.109375, "trace": 0, "frobenius_norm": 2.645751, "adjacency_eigenvalue_max": 0.939693, "adjacency_eigenvalue_second": 2.55146, "spectral_gap": -1.611768, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "intro_all", "status": "verified"} +{"matrix_size": 8, "rank": 7, "density": 0.109375, "trace": 0, "frobenius_norm": 2.645751, "adjacency_eigenvalue_max": 0.939693, "adjacency_eigenvalue_second": 2.55146, "spectral_gap": -1.611768, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "intro_apply", "status": "verified"} +{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "have_chain", "status": "verified"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "calc_chain", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_type_mismatch", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_missing_lemma", "status": "failed"} +{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_unsat", "status": "failed"} +{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "fail_bad_coercion", "status": "failed"}