fix: match predictions to manifold by object_id

Use object_id from invariant_receipt as the lookup key instead of
equation_id from equation_record. This aligns the predictions JSON
with the manifold findMatrix calls. Build passes 3307 jobs.
This commit is contained in:
allaun 2026-06-30 04:32:55 -05:00
parent 862992ec98
commit 4d0afdf90a
3 changed files with 15 additions and 12 deletions

View file

@ -98,14 +98,14 @@ def lean_str_list(xs: list[str]) -> str:
def load_matrices(path: Path) -> dict[str, list[list[int]]]:
"""Load predictions JSON into equation_id → matrix lookup."""
"""Load predictions JSON into object_id → matrix lookup."""
if not path.exists():
return {}
data = json.loads(path.read_text())
return {
p.get("equation_id", ""): p.get("matrix_8x8", [])
p.get("object_id") or p.get("equation_id", ""): p.get("matrix_8x8", [])
for p in data.get("predictions", [])
if p.get("equation_id")
if p.get("object_id") or p.get("equation_id")
}

View file

@ -61,15 +61,15 @@ def main() -> int:
raw = preds.get("predictions", [])
print(f"Loaded {len(raw)} predictions from {args.predictions}", file=sys.stderr)
raw_sorted = sorted(raw, key=lambda p: p.get("equation_id", ""))
raw_sorted = sorted(raw, key=lambda p: p.get("object_id", p.get("equation_id", "")))
defs: list[str] = []
find_cases: list[str] = []
for p in raw_sorted:
eid = p.get("equation_id", "")
eid = p.get("object_id") or p.get("equation_id", "")
mat = p.get("matrix_8x8", [])
if not eid or len(mat) != 8:
print(f"WARNING: skipping malformed entry {eid}", file=sys.stderr)
print(f"WARNING: skipping malformed entry {p.get('equation_id', '?')}", file=sys.stderr)
continue
name = lean_matrix_def_name(eid)
defs.append(f"def {name} : Array (Array Int) :=\n {lean_matrix_rows(mat)}")

View file

@ -41,13 +41,14 @@ def canonical_json_matrix(matrix: list[list[int]]) -> str:
return json.dumps(matrix, separators=(",", ":"))
def build_record(text: str, equation_id: str, name: str) -> dict:
def build_record(text: str, equation_id: str, object_id: str, name: str) -> dict:
tokens = tokenize(text)
vocab = sorted(set(tokens))
matrix = build_matrix(tokens)
matrix_json = canonical_json_matrix(matrix)
return {
"equation_id": equation_id,
"object_id": object_id,
"name": name,
"equation": text,
"schema": "rrc_pist_predictions_250_v1",
@ -77,21 +78,23 @@ def main():
print(f"Loaded {len(equations)} source equations", file=sys.stderr)
# Dedup by equation_id: deterministic representative selection per AGENTS.md
# representative = min(records, key = equation_record.equation_id)
# Dedup by object_id (invariant receipt) which matches the manifold's lookup key.
merged: dict[str, dict] = OrderedDict()
for eq in equations:
rec = eq.get("equation_record", eq)
eid = rec["equation_id"]
ir = eq.get("invariant_receipt", {})
eid = ir.get("object_id", rec["equation_id"]) # use object_id for lookup match
name = rec.get("name", eid)
text = rec.get("equation", "")
if eid not in merged:
merged[eid] = build_record(text, eid, name)
oid = ir.get("object_id", rec["equation_id"])
merged[eid] = build_record(text, rec["equation_id"], oid, name)
merged[eid]["source_records"] = []
merged[eid]["source_records"].append({
"equation_record_id": eid,
"equation_record_id": rec["equation_id"],
"object_id": ir.get("object_id", rec["equation_id"]),
"name": name,
})