Repository navigation
feat(data): add negative-example and repair-trajectory child records #4
Description
Problem
MathCorpus currently has a minimal packet-level failure summary and almost no negative examples, while Proof Search generates organic failed attempts, diagnostics, rejected actions, interactive tactic failures, and successful repairs.
Scope
Add versioned child records for:
- organic failed attempts
- controlled proof mutations
- repair links from failed attempt to successful variant
- complete repair trajectories
- diagnostic categories and structured Lean diagnostics
- attempt-level token, cost, timing, model, prompt, context, and artifact hashes
Negative records must never be able to confer proof authority on the parent packet.
Acceptance criteria
- A failed attempt can retain candidate source by governed artifact reference.
- Diagnostics preserve category, message, source span, goals, local context, and unsolved goals when available.
- Organic and mutation-generated negatives are clearly distinguished.
- Repair chains are ordered, hash-linked, and terminate in either a verified proof or explicit failure.
- Training/export policy can independently allow metadata, proof text, diagnostics, and model identity.
- Fixtures cover parse failure, unknown declaration, type mismatch, unsolved goals, and a successful repair.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
b3bfa63, stacked onbcdb683/8c74201/7f1ac10— not yet pushed, see notes on #1-#3):packet.schema.jsongainsattempts[],negative_examples[],repair_trajectories[], additive to the existing packet-levelfailureobject, mirroring MCIP'sAttemptRecord/NegativeExample/RepairTrajectoryfrom feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1. Any packet — not just a standalonekind: negative_exampleone — can now carry its own attempt history.negative_example_record.proof_authorityis fixed to"none"at the schema level (a JSON Schemaconst), not just a convention.repair_trajectories[].steps[].step_hashis a real SHA-256 over{step_index, from_attempt_id, repair_action, diagnostic_category_addressed, to_ref}(tools/mathcorpus/hashing.repair_step_hash) — a step can't be silently reworded without changing its hash.policy.check_attempts_and_repairscatches dangling attempt/variant references, out-of-order steps, stale step hashes, and negative-example/attempt diagnostic-category disagreement (warning). New corpus-widepolicy.check_repair_trajectory_refscatches a dangling cross-packetterminal_reffor when the successful proof was filed as its own packet.negative_example_record.candidate_source_ref.$defs.diagnostic.negative_example_record.origin(organic|controlled_mutation).can_export_metadata/can_export_proof_text/can_export_diagnostics/can_export_model_identity, each its own boolean.packets/negative/number_theory/gcd_dvd_omega_no_gcd_theory.v1.jsonwas enriched with a realunsolved_goalsattempt and a real successful repair — itsterminal_refpoints at the actual companion packet (elementary.number_theory.gcd_dvd_left.v1) where that second proof-search step already lives, reconstructed from the packet's own pre-existing notes, not invented. The 3 diagnostic categories with no real corpus precedent (parse_failure,unknown_declaration,type_mismatch) are covered by a new, explicitly syntheticpackets/negative/_fixtures/diagnostic_categories_conformance.v1.json—kind: concept+training.eligibility: private_audit_onlyso it's excluded from every export lane, confirmed by grepping a full export run for its packet_id.Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(data): add negative-example and repair-trajectory child records (c…