Update to Mathbox

{
  "description": "Run one bounded, auditable mathematical research route: a proof attempt, reduction, counterexample search, source-dependent implication, or claim-supporting computation. Use when the user explicitly asks to attack a research question or invokes this skill. Do not use for a sustained multi-route investigation that continues after failed approaches, routine editing, explanation, or an unchanged verification rerun.",
  "included_files": [
    {
      "relative_path": "agents/openai.yaml",
      "size_in_bytes": 268
    },
    {
      "relative_path": "evals/evals.json",
      "size_in_bytes": 10086
    },
    {
      "relative_path": "evals/trigger-evals.json",
      "size_in_bytes": 1520
    },
    {
      "relative_path": "references/evidence-model.md",
      "size_in_bytes": 1876
    },
    {
      "relative_path": "references/project-context.md",
      "size_in_bytes": 864
    },
    {
      "relative_path": "references/route-card.md",
      "size_in_bytes": 2403
    },
    {
      "relative_path": "references/structural-moves.md",
      "size_in_bytes": 2543
    }
  ],
  "name": "research-attempt",
  "skill_md_contents": "---\nname: research-attempt\ndescription: >-\n  Run one bounded, auditable mathematical research route: a proof attempt, reduction, counterexample search, source-dependent implication, or claim-supporting computation. Use when the user explicitly asks to attack a research question or invokes this skill. Do not use for a sustained multi-route investigation that continues after failed approaches, routine editing, explanation, or an unchanged verification rerun.\n---\n\n# Bounded mathematical research attempt\n\nPursue one route far enough to obtain a durable result, a precise obstruction,\nor a well-identified next implication. This is a work-package boundary, not a\nreason to stop a broader user-authorized investigation. For sustained or\nmulti-route requests, use the available `research-program` workflow, or continue\nsuccessive attempts directly if it is unavailable. Do not turn the log into a\ntranscript.\n\n## Resolve project context\n\nDetermine the repository root first. Read the applicable `AGENTS.md`, the\ncurrent status summary when present, and only the files relevant to the target.\nSearch a large status, claims file, or history index for relevant sections\nrather than loading it wholesale. Resolve project roles from the paths\nnamed there. When not explicit, look for the standard alternatives in\n[project-context.md](references/project-context.md). Interpret every project\npath relative to the repository root, never relative to this installed\n`mathbox:research-attempt` plugin skill (or its standalone installation).\n\nIf the project uses `.mathbox/`, use the available `research-state` skill's\nbrief check and goal handoff, opening full details only for the relevant\ncontracts and evidence. Check freshness and the target's dependency closure\nbefore trusting a status label. Otherwise use the existing prose evidence records. A clean ledger\nis bookkeeping evidence, not mathematical verification.\n\n## Open the route\n\n1. Inspect the worktree and preserve unrelated changes.\n2. Normalize the target:\n   - exact statement or decision;\n   - quantified objects and source/target types;\n   - hypotheses, coefficient domain, grading, variance, signs, finiteness,\n     completion, equivariance, and range;\n   - current evidence status and dependencies.\n3. Search the research-history index for the target and nearby mechanisms,\n   then open only the nearest relevant records needed to find the first failed\n   or unproved implication.\n4. State a falsifiable success criterion, a failure/no-go criterion, and the\n   cheapest decisive example, source check, or computation.\n5. Choose one route within the current program. Match it against prior failed\n   mechanisms, not merely prior titles. Retrying a mechanism with an established\n   obstruction requires a new input, invariant, construction or hypothesis that\n   addresses its first failed step. An unresolved step is not an obstruction;\n   resuming an untried or deferred continuation needs a concrete next action,\n   not a new mathematical premise. When resuming a stalled step, state what\n   differs from the stalled attempt: a narrower sub-step, method, tool or\n   resource. Do not rerun it unchanged.\n\nUse the route card in [route-card.md](references/route-card.md) when a durable\nentry will be needed.\n\nFor an obstructed structural route, consult the relevant moves in\n[structural-moves.md](references/structural-moves.md). Turn a proposed analogy\ninto a specific comparison, obstruction or discriminating invariant.\n\n## Execute\n\n- Begin with the smallest typed case capable of changing the conclusion.\n- Verify that the chosen example, representative and every intermediate\n  construction belong to the claimed domain; a convenient surrogate needs an\n  explicit comparison theorem before it can decide the route.\n- Search actively for counterexamples, boundary cases, convention failures,\n  circularity, and missing hypotheses.\n- Check nullary/unary or minimum-parameter cases and absolute degrees whenever\n  a unit, augmentation, suspension or induction boundary is involved.\n- Do not repair a failed type, sign, variance, normalization, or completion\n  check by silently changing the statement or convention.\n- Route every load-bearing question about what an external mathematical source\n  proves through the available `literature-check` skill\n  (`mathbox:literature-check` in plugin installations). That workflow checks an\n  authorized project-local cache before fetching. If the skill is unavailable,\n  perform the exact-source check directly with available tools. If the source\n  cannot be verified, leave the input conditional; snippets and memory do not\n  discharge it.\n- For computation, separate the mathematical claim from the finite assertion\n  implemented. Record domain, bounds, seed, versions, inputs, runtime, and\n  non-claims; use the `mathbox:computation-audit` plugin skill when\n  appropriate.\n- Before calling a finite sweep exhaustive, compare the claimed population with\n  the actual iterator, filters and skipped cases. Sampling requires a proved\n  coverage reduction.\n- After any bounded success, pause before extending the arity, range, or case\n  ladder. Identify the minimal structural features used, separate uniform\n  features from case-specific coincidences, and formulate the candidate\n  uniform lemma or obstruction. Run another finite case only if it\n  discriminates between named alternatives or enters a genuinely new regime.\n- A timeout, failed search, or bounded computation is not a universal negative\n  result.\n- A change to a registered convention requires explicit owner approval unless\n  the project instructions already authorize that exact correction.\n\n## Classify the outcome\n\nUse one of:\n\n- proved as written;\n- proved after an explicit restriction;\n- conditional on a named unverified input;\n- computationally verified only in a stated range;\n- heuristic or conjectural;\n- refuted, with the smallest counterexample found;\n- ill-typed or incomplete;\n- inconclusive, with the first unresolved implication.\n\nState the strongest surviving result. Never upgrade evidence because the route\nwas long or persuasive.\n\nClassify this attempt separately from the route's disposition. If a construction\nis unresolved, say what you could not establish; do not infer that it is\nimpossible. Preserve other proposed continuations as untried, obstructed with\nevidence, or deferred with a reason and resumption condition. An inconclusive\nattempt or a resource limit alone does not close the route. Return unfinished\nwork to the program, or retain an executable handoff when only this bounded\nattempt was authorized. Closing an unresolved route needs an account of why no\nknown continuation remains executable within its stated scope.\n\n## Persist at a natural checkpoint\n\nExploration may remain scratch work. Create durable records when the route\nproduces reusable mathematics, a counterexample, a corrected dependency, a\nmaterial blocker, a convention decision, or a claim-supporting computation.\n\n- Put reusable proof or obstruction details in the project's durable proof\n  location.\n- Write one self-contained route record in the project-designated research\n  records directory, or `research/records/` when none is designated. Use the\n  format and filename rules in [route-card.md](references/route-card.md).\n- Append one compact linked entry to the project-designated route index. In a\n  small flat history this is normally `RESEARCH_LOG.md`; in a sustained\n  program it may be a program/phase index reached from the short top-level\n  history entry point. Do not add the same route to both levels or put route\n  details, commands, or dead ends in an index. If a hierarchical project has\n  no designated route index, resolve that location under its edit rules before\n  appending; do not turn the top-level program entry into a flat route log.\n- Update live status or claim obligations only when project state changed.\n- Treat live status as current state, not chronology. Keep its latest full\n  verification summary and link the route record or manifests for older runs.\n  Do not add another full checkpoint story. Replace a stacked dated narrative\n  with current facts and a link only when that narrative already has a durable\n  home (an indexed record, manifest, or closeout) and the project's edit policy\n  permits it. Otherwise leave it in place and report that compaction needs a\n  `research-program` closeout or `mathbox:research-init` migration.\n- In an executable ledger, record only changed contracts, evidence, reviews,\n  and route outcomes. A session alone needs no event. Use a prevalidated batch\n  for several necessary events while preserving their distinct types.\n- When persistence is authorized but this host cannot execute or write, use the\n  `research-state` deferred-handoff contract for the durable files, index entry,\n  and ledger proposals; report that local ingest has not yet recorded them.\n- Once indexed, keep the record and index entry immutable. Record a correction\n  in a new file with a `Corrects:` link and append it to the same designated\n  route index. Do not create a program closeout for each attempt.\n- If the index still contains legacy long-form entries, do not rewrite them as\n  a side effect of this attempt. Use the new format prospectively and report\n  that a `mathbox:research-init` migration remains pending.\n- Do not integrate into a manuscript unless that is separately requested.\n\nEvidence labels and promotion rules are summarized in\n[evidence-model.md](references/evidence-model.md).\n\n## Verify and report\n\nRun the narrowest relevant documented check, then broader checks only when their\nrisk trigger applies. Report:\n\n1. target and route;\n2. outcome and evidence label;\n3. decisive derivation, source, counterexample, or computation;\n4. durable files changed;\n5. commands run and exact scope;\n6. unresolved assumptions and the next mathematical question; when evidence is\n   bounded, include its uniform route or discriminating check.\n"
}