Problem packet rules

Purpose

A problem packet is the reviewed research graph attached to one canonical TheoremDB problem. Checked-in fixtures supply the initial release and outage fallback. The live packet head supplies current statement pages, the research directory, search projections, and agent-readable research context.

These rules govern packet creation, extension, correction, review handoff, and release checks. The bounded runtime context_packet returned by orient and check_plan is a different object. Agent retrieval governs its selection and budget.

Core invariants

Every new contribution satisfies all of these conditions.

One active packet serves one canonical target. Two fixture files with the same dataset.problem_ref compete for one static route, and the later file silently replaces the earlier file.
dataset.problem_ref uses a stable canonical slug or stable ID. Display numbers are local to one store and are forbidden here.
The target problem has passed the canonical problem intake and review workflow. A packet cannot create a private substitute for a missing target.
dataset.project is unique across the corpus. Object slugs are globally unique.
Published packet revisions are immutable. A record slug is the stable logical identity across reviewed editorial revisions. A correction that changes the mathematical identity of a claim creates a successor and an audited supersedes edge. Public R record numbers and S statement-family numbers are store-local accession projections. They never enter packet JSON, object hashes, relation endpoints, or presentation selectors. Slugs and content hashes remain durable aliases.
Every object is bound to the canonical target. Every relation endpoint is an object in the same JSON file. A packet with two or more local objects has a connected local graph when edge direction is ignored.
Status, evidence, scope, and resolution are separate facts. Each field says exactly what its validator and public label claim.
Sources, licenses, computations, and artifact descriptions support the exact record that cites them.
Every packet source projects into the problem’s References tab with its citation, locator, and relevance preserved.
Agent writers stay within public writer authority. Reviewers, resolution workflows, and formal verifiers assign controlled grades and relations.
A packet release follows research packet publication. It accounts for the checked-in fallback, immutable live revision, semantic diff, review history, and current head.

Legacy fixtures contain exceptions that predate this contract. They remain historical data and provide no waiver for new work.

Historical baseline

At this revision, the checked-in corpus has 444 fixtures, 1,677 objects, and 1,414 relations. A normal agent contribution leaves the exception counts below unchanged or reduces them. A controlled workflow or reviewed migration may change a count and updates this baseline in the same release.

Known structural exceptions:

fibonacci_research_v1.json has no dataset.problem_ref or dataset.agent;
graph_metric_subtour_gap_eight_research_v1.json, rainbow_divisor_count_run_1e12_research_v1.json, rainbow_squarefree_gap_1e12_research_v1.json, and weight_five_cyclic_inverse_127_research_v1.json each have more than one connected component.

Eight legacy scopes use kind: "bounded" without machine-readable bounds: one each in carmichael_collision_gap_10m, hamming_rips_twenty_beta_one, max_girth_sl2_101_generators, prime_indicator_recurrence_weight_600, and small_squarefree_summand_billion, plus three in sl2_101_unipotent_cayley_diameter. The validator fixes the exception to those exact fixture and object slug pairs. New writes require bounds.

Closed object vocabulary already present:

fixture-only types: note (1) and problem (9);
statuses outside the direct-writer table: artifact reproduced (12); attempt established (1), failed_as_complete_proof (3), incomplete (1), and open (1); claim claimed_unverified (1), established (240), open (17), partial (4), and reproduced (14);
evidence grades outside the current writer and controlled-grade sets: computed (1), documented (1), literature_audit (1), mathematical_argument (4), mathematical_identity (22), mixed (1), planned (1), primary_source (1), proposed (18), proved (2), supported (4), and verified (1);
relations outside CONTROLLED_RELATIONS: bounds (4), contextualizes (20), corroborates (8), cross_checks (2), extends (1), implies (1), independently_reproduces (1), independently_verifies (1), produces (2), proposes_continuation_for (1), qualifies (1), refines (4), reproduces (16), and targets (1);
packet source URLs awaiting structured citations: 24;
external object sources awaiting structured citations: 415;
external object sources with composite semicolon locators: 307.
active legacy research records without a packet-specific relevance annotation: 262.

Eight immutable structured rows in two published packets predate the current row contract. Their complete packet-wide mirrors supply the public citations without changing the content-addressed research objects. The validator names those two lists exactly, checks every mirrored identity, and rejects any new exception. All other structured rows have no field exemption. Historical free-form sources remain visible while they are converted into reviewed rows, and the validator rejects growth in each queue.

These names record the historical audit. New or edited objects use the current contracts below.

Before writing

Read the complete canonical problem and every object already attached to it. Then:

resolve the target by slug or stable ID;
inspect its statement, typed exposition, acceptance conditions, resolution state, structured references, documented reference search, and source advisories;
call orient, then use check_plan for any proposed experiment or proof route;
inspect current claims, attempts, artifacts, formalizations, and supersession edges;
search TheoremDB for duplicate targets and overlapping records;
perform a dated source check for the exact parameter, normalization, and nearby formulations;
decide whether the work creates a new packet, adds to a published packet, corrects a record, or submits a resolution.

A blocking statement-integrity advisory pauses proof and resolution work. Source audit and correction work follow the advisory workflow.

File and dataset contract

Location and name

Store a fixture at:

api/app/data/<descriptive_snake_case_name>_research_v1.json

The suffix names the fixture format. Choose a name tied to the canonical problem. Keep one active file for that target.

Do not create a second active fixture to work around packet growth. If one file approaches build, review, or import limits, stop and design a versioned projection or shard format with deterministic assembly and atomic import before splitting it.

Top-level shape

Use this shape:

{
  "dataset": {
    "project": "canonical-target-research",
    "version": "canonical-target-research-v1",
    "problem_ref": "canonical-target-slug",
    "source_url": null,
    "license": "CC0-1.0",
    "provenance": "Who assembled or reproduced the material, from which sources, and when",
    "contributors": [],
    "agent": "agent-name/version"
  },
  "presentation": {
    "version": "theoremdb-packet-presentation-v1",
    "resolution": "open",
    "status_record": "canonical-target-current-status",
    "recommended_next": "canonical-target-next-attempt",
    "featured_failure": "canonical-target-reusable-failure"
  },
  "objects": [],
  "relations": []
}

Choose the license that applies to the submitted dataset. CC0-1.0 in the example fits original factual data released on those terms. It grants no rights to copied source material.

An optional top-level figure may hold a supported pure-data figure configuration.

Reader presentation

presentation is the reviewed index into the packet for human-facing pages. It selects existing immutable records and contains no mathematical prose:

version is exactly theoremdb-packet-presentation-v1;
resolution is open while no complete answer is recorded, review_pending when a complete answer and argument await independent review, and resolved after that review accepts the answer to the whole stated problem;
status_record is the current claim selected for the Status tab of an open problem;
resolution_record is the direct answer claim selected for the Status tab while review is pending, or for the Resolution tab after the answer is accepted;
recommended_next is the actionable open attempt another worker should consider first;
featured_failure is the failed, blocked, timed-out, inconclusive, abandoned, incomplete, or failed-as-complete-proof attempt whose boundary is most reusable.

An open packet has exactly one status_record and omits resolution_record. A review_pending or resolved packet has exactly one resolution_record and omits status_record. A packet with an actionable open attempt has one recommended_next. A packet with a negative attempt has one featured_failure. Omit an optional work selector when the matching class is empty.

Legacy fixtures may contain more than one genuine problem object. The root presentation applies only to the canonical problem. Each additional public problem uses a top-level presentations entry keyed by its exact slug and satisfying the same selector contract. Its selected status or resolution record must have a directed relation path to that problem. When the entry is absent, the secondary problem inherits no packet status and remains open. New packets continue to use one canonical target.

The Status selector points to a current local claim bound to the canonical target. Its summary states the strongest recorded mathematical status and the exact unresolved remainder. A bare “open,” “unknown,” or “work remains” is insufficient. Dated search conclusions belong in the record body or a supporting Research object. A sourcing, convention, notation, or indexing audit cannot serve as status_record.

The Resolution selector points to a current local claim that directly answers the complete canonical statement. Its summary stands alone as the public answer. The first sentence gives the requested value, formula, classification, existence result, or counterexample with the problem’s parameters and conventions. Phrases such as “the problem is resolved,” “an exact answer was found,” or “see the proof” do not satisfy this requirement. The body gives a complete, self-contained account of the resolution in concise, readable mathematical prose. Resolution always contains that prose argument. Lean declarations, verifier results, and certificate status belong in Lean verification or supporting evidence. A record with metadata.proof_file may keep that complete proof in a checked repository Markdown file instead. The public renderer inlines every mathematical section of the file in Resolution. A link to the file does not substitute for that rendering. A computational resolution states the finite reduction, exhaustive step, and certificate check needed to establish the answer. Raw output, source detail, and secondary checks may remain in supporting records.

A proof file puts [@key] beside every named result or imported method it invokes and defines each key by stable URL in its references section, as required by the reference standard. The renderer resolves those keys against the selected record’s structured references, prints linked [n] markers at the point of use, and gives the Resolution proof a short source map. Unresolved proof citations stop the release.

Judge resolution against the complete problem statement and its acceptance conditions. A bounded check, one side of an interval, a useful reduction, or an answer to a nearby problem leaves the value open. A resolved presentation satisfies all of these binding invariants:

resolution_record names a local object with object_type: "claim";
the selected claim has status: "established";
its current canonical-target binding is the review-controlled resolves relation;
its scope covers the whole statement and every acceptance condition;
it has not been superseded;
its direct-answer summary satisfies the standalone requirement above.

The acceptance conditions themselves state what completes the displayed problem. They cannot refer to a hidden incumbent, claimed value, progress endpoint, or packet result. A request for an exact value or classification requires an exact answer or characterization with a proof or certificate. Better bounds, additional finite cases, and tighter numerical enclosures remain partial research unless the canonical statement expressly makes one of them the target.

Use review_pending only when the same scope and completeness conditions hold but the argument has not passed independent review. Its selected claim has status: "reported" or status: "supported", target_relation: "claims_resolution_of", and metadata.independent_review_status: "pending". The public Status tab labels it as a claimed answer, gives the complete argument, and carries the required Lean verification tag. A successful independent review changes the claim to established, changes the target relation to resolves, and changes the presentation to resolved.

The reviewed resolves binding records acceptance of the answer’s relation to the complete target. The evidence grade records how the claim was checked. These fields keep their separate meanings.

Every selector is a local object slug of the required type and state. A selector cannot assert resolution, strengthen evidence, or replace a typed relation. The renderer may use relations to attach supporting artifacts and checks to the selected record.

The public Status tab renders the active open selector’s summary. For review_pending, it renders the claimed direct answer followed by its complete body or inlined metadata.proof_file, with the pending-review label visible. The public Resolution tab renders the accepted selector’s direct-answer summary followed by the same complete proof material. The renderer does not combine other records into either tab. Follow the content boundaries in problem display.

An attached open packet may be visible before its canonical problem passes publication review. In that case the Status tab labels the selected summary Packet-reported status and states that it has not passed editorial review. The canonical state remains unknown. The packet selector cannot qualify the problem, add it to the reviewed directory, or produce a Resolution tab.

Every resolved packet also produces a Lean verification label. The label is Lean-verified only when a current formalization object names a pinned Lean world, carries the controlled formally_verified evidence grade, and has a proof or formalization relation to the canonical problem or resolution_record. All other resolved packets produce not Lean-verified. Packet authors do not write this label by hand.

The paused Survey projection has no presentation selector or authored research object in the packet. Its retained model is governed by the inactive research survey standard. A proposed synthesis that adds an inference or comparison enters the packet as a new object and passes review before any future public display.

The References projection is also derived at render time. It takes the union of the canonical problem’s structured references, dataset.references, dataset.source_url, every object’s source_url and any external source_locator attached to an identifiable work, structured references nested in object metadata, and sources attached to reviewed status evidence. Stable DOI and URL identities collapse to one bibliography row. Distinct locators and relevance notes remain attached to that row. Internal paths and replay notes stay with their records. The packet stores no presentation selector or authored bibliography object for this projection.

Presentation selectors are excluded from research-object content hashes and from the live object store. A reviewed selector change updates the static packet reading without editing or superseding the selected object. Release review still checks that the selector describes the live and checked-in graphs honestly.

presentation.headline_record is a compatibility alias for the active state-specific selector. A legacy packet may use it until migration. When headline_record and status_record or resolution_record appear together, they name the same record. New packets and edited presentations use the state-specific selector. metadata.featured_result is an older compatibility selector. When it appears, it names the same active record.

Dataset fields

project: a stable kebab-case research-project identifier, unique across every packet and live project.
version: the packet identity carried into stored object metadata. Set it at creation and freeze it.
problem_ref: the canonical problem slug or stable ID. Confirm exact resolution before review.
source_url: the common source when one source anchors the packet. Use null when each object has its own source or the packet contains original work.
references: structured citations for packet-wide sources, following the reference and source-use standard.
license: the rights basis for the packet’s authored data and prose.
provenance: a dated account of assembly, searches, reproductions, and source revisions.
contributors: people or organizations credited by the source.
record_contributors: an importer-only historical fallback for object attribution. Use it only in a reviewed append-only migration that must preserve previously stored credit receipts. contributors remains the public packet byline, and an object’s own contributors field takes precedence.
record_version, record_provenance, and record_operator: importer-only defaults for replaying exact historical records inside a reviewed append-only union.
record_routing_targets: the exact local problem slugs accepted for a named historical routing migration. The reconciler limits this exception to records carrying the frozen historical version and provenance, and requires a matching home-target binding.
agent: the producing agent and version, when an agent produced the packet.

The seeder expands project, source_url, license, object contributors, and agent, then injects the record version and provenance into stored metadata. An object’s explicit metadata can name a newer envelope when it is a successor in a reviewed append-only union. The seeder chooses contributors in this order: the object’s field, dataset.record_contributors, then dataset.contributors. Project, source, license, and metadata affect the content hash. Contributors and agent affect attribution. Treat the envelope as immutable after first import. A proposed envelope change requires a reviewed migration plan.

The seeder copies dataset.contributors to any object without its own contributors field. Put names in the dataset list only when they apply to every object. Otherwise give each object its exact source contributors, using an empty list for original agent work. The public writer accepts a nonempty contributor list only with sourced evidence and a source URL or locator.

When dataset.source_url is present, it uses an absolute HTTP or HTTPS URL and identifies a source relevant to the target or the packet as a whole. It always enters the References projection. Give the supporting object a fuller citation and exact locator when the dataset URL alone cannot identify the cited result.

Later additions record their own search date, execution date, source revision, and reproduction details in the object body and metadata.

Do not use problem_number, a numeric problem_ref, or the legacy dataset.figure field.

Canonical target and problem objects

A new packet attaches research to an existing qualified problem through dataset.problem_ref. Confirm that the reference exists in the canonical problem corpus.

Fixture records with object_type: "problem" are legacy migration data. New packets and additions omit them. A genuine subproblem first passes problem review and the display standard, enters through the canonical problem intake workflow, and receives its own packet through dataset.problem_ref.

canonical_alias exists for migrations of older data. New packets do not use it.

Object contract

Identity and size

Every object records one reusable unit of work.

Use a globally unique kebab-case slug. Include enough of the target and purpose to avoid collision.
Do not author record_number, record_ref, statement_number, or statement_ref. The serving store assigns them after import and backfills them for earlier records.
Supply object_type, title, summary, body, status, evidence_grade, and source_locator.
Supply relevance for every new or edited packet record. In one or two sentences, state how the record advances, constrains, tests, or redirects work on this packet’s canonical problem.
Write a summary that stands alone in a compact retrieval packet.
Use the body for the exact argument, method, result, limit, or replay detail.
Split unrelated assertions and experiments into separate objects.
Keep metadata structured and small. Put mathematical meaning in the summary, body, and scope.

routing_target is an importer-only field for a successor in a reviewed legacy packet that contains several problem objects. It names one non-aliased problem object in the same fixture. The field does not enter the research-object content hash. The stored immutable routing target and its home binding must agree.

Standing alone means that a summary identifies the record and its contribution during retrieval. A summary is not a substitute for the canonical mathematical statement. Public renderers use the reviewed editorial statement for every statement-labeled panel and never place summary or title in that slot.

source_locator identifies the exact theorem, page, section, table row, declaration, artifact, file, or execution record that supports the object. source_url, when present, uses an absolute HTTP or HTTPS URL. Externally sourced work supplies enough bibliographic detail in these fields or structured metadata for a reader to identify the author, title, publication, and relevant location. Original work still names its internal proof, artifact, or dated execution record.

New fixture objects stay within the strict HTTP object schema even when the trusted seeder would accept more:

Field	Limit
`project`	120 characters
`slug`	160 characters
`title`	240 characters
`summary`	4,000 characters
`relevance`	1,000 characters
`body`	50,000 characters
`source_url`, `source_locator`	4,000 characters each
`license`	200 characters
`world`	1,000 characters
`formal_statement`	100,000 characters
`metadata`	100,000 encoded JSON characters
`artifact`	250,000 encoded JSON characters
`contributors`	100 entries, 500 characters per entry
`agent`	120 characters

Content fields enter the object hash. Editing published content creates a different object identity and conflicts with the old slug. Use the correction workflow below.

Public packet proposals encode each new or changed integer outside JavaScript’s exact range as a decimal string. A proposal may carry an existing arbitrary-precision integer unchanged at the same packet path. Package-owned release tooling may submit reviewed exact integer tokens through its trusted preflight path. This boundary prevents a browser JSON runtime from silently rounding a mathematical value before publication.

relevance is a packet annotation tied to dataset.problem_ref. It stays outside the research-object content hash and stored object row, so the same immutable record can carry a different explanation when another packet cites it. A packet revision may improve this annotation without superseding the mathematical record. Historical packets may omit it until their next editorial pass.

Supported types

New agent contributions use:

claim: one exact mathematical assertion;
attempt: one proposed, active, completed, failed, or blocked line of work;
artifact: a reusable program, dataset, certificate, proof trace, or execution recipe;
formalization: a statement or proof in a pinned formal environment.

problem is reserved for reviewed problem intake. note is a legacy fixture type and is closed to new contributions.

Claims

A claim states its quantifiers, parameter conventions, equivalence relation, and boundary. Its scope matches the assertion. An exact finite value needs exact arithmetic, a certificate, or a source that establishes that value.

Record a conjectural observation with a working claim status. Route a result that meets the problem’s acceptance conditions through the resolution submission and independent review workflow. A raw claim never changes the canonical problem’s resolution state.

Attempts and negative results

An attempt records:

the exact action or method;
the input family, parameter range, assumptions, and environment;
the budget or stopping rule;
the observed outcome;
the blocker or failure boundary;
any reusable residue and the condition that would justify another run.

failed, blocked, timed_out, and inconclusive describe different outcomes. Choose the literal one. A literature audit that finds no answer is a dated search report. It supplies no proof that an answer is absent.

Artifacts

Keep an artifact object as a compact replay descriptor. Store substantial code and data in the repository, an immutable release, or approved object storage. A small certificate or short self-contained program may live inline.

Program-backed evidence includes the exact program source. A short program uses source_lines plus source_sha256. Larger programs use an immutable source URL or repository path together with the exact commit, release, or source digest. A command, compiled-binary digest, execution log, or prose description alone does not identify the program that produced the result. If the source is unavailable, record the report as sourced; it cannot receive executable, computational, or reproduced evidence on the strength of that run.

Record:

immutable source identity, such as a repository path plus commit, release URL, or digest;
language, runtime, tool versions, and dependencies;
entry point, exact command, and inputs;
expected output, certificate, or digest;
pseudorandom generator, version, and seed when randomness is used;
precision and error model for floating-point work;
time, memory, processor, and storage bounds;
network requirements and external services.

Use these canonical keys for new inline artifact metadata:

entrypoint: the file, module, or declaration that starts the replay;
command: the exact shell command or tool invocation;
runtime: the language runtime, proof assistant, solver, or toolchain environment;
runtime_seconds: measured wall-clock duration in seconds;
source_lines: short inline source represented as an ordered array of lines;
source_sha256: SHA-256 of the exact inline source bytes or referenced source file;
source_url: immutable release or repository URL when source is stored externally;
source_version: exact commit, immutable release, or equivalent revision for external source;
outputs: the expected structured results, certificates, or digests.

Treat a compiled-binary digest as the identity of that recorded build unless the build is known to be deterministic. Toolchains may embed UUIDs or timestamps. Cross-build reproducibility should anchor on the source digest, pinned toolchain and command, and stable output or certificate digest.

Legacy fixtures also use entry_point, wall_time_seconds, and code. Readers preserve those aliases. New and replacement records use the canonical keys above. Keep elapsed time out of runtime, whose value describes the execution environment.

Inspect an artifact before execution. Run untrusted work in an isolated environment with time and resource limits. Keep secrets out of commands, fixtures, logs, and outputs. Reject destructive paths and undeclared network access.

Randomized or floating-point evidence supports the stated probabilistic or numerical claim. It cannot establish an exact theorem without a separate certificate or proof.

Formalizations

Pin the prover, package set, world or commit, source module, declaration, and exact statement. Agent-authored formalizations use pending_verification with unverified_formalization. The formal verification worker records a passing check and assigns verifier-controlled evidence.

An approved formal target accepts several immutable proof submissions. A queue claim is an advisory coordination signal, so proof submission does not require an exclusive lease. Each distinct proof receives its own deposit, verifier verdict, and contributor receipts. An identical proof deposit is shared and credits each authenticated contributor who supplied it. When a signed worker accepts the exact approved statement hash, the verified record may enter the packet through the constrained append path in research packet publication. Statement changes and broader packet edits require the standard review path.

Status and evidence

Agent-authored drafts use values accepted at the public writer boundary in api/app/research_workflow.py. Check the live constants before every batch. Existing fixtures carry older spellings and steward-only values that are closed to new agent writes.

Current direct-writer statuses are:

Type	Allowed status
`claim`	`draft`, `proposed`, `observed`, `reported`, `conjectured`, `supported`
`attempt`	`planned`, `in_progress`, `partial`, `completed`, `failed`, `blocked`, `timed_out`, `inconclusive`, `abandoned`, `open_strategy`, `next_experiment`, `promising`
`artifact`	`draft`, `planned`, `available`, `reported`, `sourced`
`formalization`	`draft`, `pending_verification`

Use conjectured, observed, reported, or supported for a live claim as warranted. status: "open" is outside the direct-writer claim vocabulary and produces inconsistent static projections: the compact packet omits it while the research article treats it as a result. Use an allowed claim status.

Current agent-writable evidence grades are self_reported, sourced, executable, and computational. Formalization drafts use unverified_formalization.

self_reported records the contributor’s account without external support.
sourced requires a stable source URL or source locator.
executable requires a replayable artifact descriptor.
computational requires execution details or an artifact and states the exact computed region.
reproduced requires an independent replay through a controlled review path.
formally_verified comes from the pinned verification service.

Mathematical resolution state and evidence grade remain separate. A stronger-sounding label cannot substitute for review. Agents must never self-assign reviewer or verifier grades. When a controlled workflow emits another status or grade, copy its accepted record exactly. Typing that controlled value into a fixture cannot stand in for the workflow.

Scope

Use the structure enforced by api/app/claim_scope.py. Scope is mandatory for:

executable, computational, reproduced, and formally_verified evidence;
claims with supported, established, or reproduced status.

Give every claim, computation, and bounded attempt a scope whenever the covered region can be stated.

Allowed kinds:

universal: the assertion in this record covers every case named by its own quantifiers;
bounded: numeric parameter limits define the covered region;
family: family names a structural subclass;
conditional: conditions lists the record IDs or slugs on which the assertion depends.

Every scope has a plain statement of at most 400 characters. A bounded scope names its parameters under bounds with numeric min and/or max. Use equal minimum and maximum for a singleton, with at most eight parameters. A conditional scope lists at most 16 record IDs or slugs. Match the problem’s indexing, units, and normalization. Set exhaustive: true only when the computation or argument covers every case in the stated bounds.

A universal scope concerns the assertion in its own record. It does not announce resolution of the target problem.

Sources, prior work, and rights

The complete citation and reuse contract is the reference and source-use standard. Treat each packet as a short mathematical paper. Cite the source on the record that makes the sourced claim, and connect the citation to that claim in every public projection.

Prefer primary sources. Use a stable DOI, arXiv identifier and version, journal page, archival URL, or repository commit. A locator names the exact theorem, page, section, table row, declaration, file, or line range.

The packet’s source fields form part of the public bibliography. A packet author checks the rendered References union for every new or changed object. Relevant references found during the canonical problem’s documented search stay in the problem submission even when no packet object cites them yet.

Separate these records:

what a source reports;
what the contributor independently checked;
what a computation observed;
what remains open after a dated search.

State the search date, databases and sources checked, exact query or formulation, strongest nearby result, and unresolved remainder. Match shifted indexing and alternative normalizations before claiming novelty.

Use an independently written summary for ordinary source discussion. Quoted or adapted prose, copied proof text, code, data, figures, tables, and screenshots carry the source-use record required by the reference standard. Record source-code licenses beside executable artifacts. The packet license covers the packet author’s contribution and cannot expand the source owner’s grant.

Relations

Use the exact controlled vocabulary in research_workflow.CONTROLLED_RELATIONS. Read each edge aloud as <src> <relation> <dst> and confirm that the direction says the intended fact.

New packet graphs follow these rules:

every src and dst slug exists in the same fixture;
every object in a multi-object packet participates in a meaningful edge;
the graph is connected when direction is ignored;
each (src, relation, dst) triple is unique;
self-edges are forbidden;
relations describe mathematical or evidentiary dependence rather than page layout.

Use addresses as the default canonical target binding. target_relation: "claims_resolution_of" is reserved for a complete answer awaiting independent review. target_relation: "resolves" is reserved for a trusted import after exact-scope review. Direct writers cannot assign refutes, resolves, validates, or verifies.

Common literal edges include artifact evidences claim, attempt uses artifact, attempt produced artifact, attempt attempts claim, attempt addresses problem, and formalization formalizes claim. Choose the relation whose direction matches the stored vocabulary.

At most one legacy record in a packet may carry metadata.featured_result: true, and it matches the active presentation.status_record or presentation.resolution_record. Before migration, it matches the compatible presentation.headline_record.

Creating a packet

Complete the checks in “Before writing.”
Confirm that no current fixture uses the target problem_ref or proposed project.
Create the JSON fixture with the frozen dataset envelope.
Add small, independently meaningful objects and their local relations.
Confirm that every packet source appears in the rendered References union with its exact locator.
Add the fixture path to RESEARCH_FIXTURES in api/app/seed.py. The web app discovers files automatically; the development seeder uses this explicit list.
Run the packet checks and every artifact replay below.
Dry-run the fixture importer against an approved disposable or staging store where the canonical target resolves.
Submit the packet, sources, replay output, and import digest for review.

Production startup skips fixture seeding. An operator imports an approved new project with the digest-confirmed importer once the import safety requirements below are satisfied. A dry run is read-only and requires a schema-ready configured store.

Adding to a published packet

The development fixture seeder leaves a project untouched once that project contains an object. The operator importer accepts an exact completed replay as a no-op and rejects every other nonempty project graph. The publication-authority reconciler has one narrower path for a manifest-pinned append-only revision. It verifies every stored fixture identity, content address, attribution row, target binding, and relation that the reviewed union names. It then inserts the missing successors and supersedes relations in one transaction. A slug collision, changed primary target, or altered stored row aborts the transaction. Unrelated community records in the same project remain in place.

After first import, the live research object is canonical. A matching slug alone cannot establish identity because object IDs are content hashes.

For an agent-writable addition intended for both surfaces:

Read the live project and checked-in fixture, then reconcile any difference.
Prepare the final fixture object with the frozen dataset values that the seeder inherits: project, version metadata, provenance metadata, source URL, license, contributors, and agent.
Submit those exact content fields through POST /v1/research/objects, then add relations through POST /v1/research/relations.
Compare the returned live ID with research_object_id for the fully expanded fixture object in api/app/hashing.py.
Compare the expanded contributors and agent with the live attribution.
Append the object and relations to the JSON packet only after identity and attribution match.
Preserve the dataset envelope and every earlier object.
Verify the live graph and static packet separately.

The effective fixture agent is dataset.agent. For a legacy fixture where the field is absent, the seeder uses mixed-memory-fixture/v1; that absence remains part of the frozen envelope. The seeder assigns the effective agent to every object and assigns operator: "seed" to imported objects. A fixture mirror cannot preserve live account ownership or credit receipts. It also cannot preserve a later producer whose agent differs from the effective fixture agent. Keep the live receipts canonical. A packet with no declared agent, or work by another agent, requires a reviewed per-object attribution format before the addition enters the fixture. Never relabel that work with the packet’s earlier agent or legacy default.

record_result, resolution review, and formal verification generate their own workflow metadata. The current fixture seeder also injects dataset version and provenance metadata. A hand-copied JSON record can therefore receive a different content hash. Use the applicable controlled workflow, then require a reviewed export, synchronization, or migration path that proves ID parity before adding that record to the checked-in packet.

Do not claim that an addition is deployed until both intended surfaces contain the same content-addressed contribution. Record any temporary live/static difference in the release review. A differing ID identifies a separate object, so stop the packet addition and resolve the projection format.

The MCP record_research_object tool validates scope and includes the normalized value in the content hash and stored object. The public API projections and tools/research_bundle.py preserve it as well. Keep the scope-persistence and projection regression tests green when changing any write, retrieval, or bundle path.

Packet submission by an outside agent

A packet may arrive from the agent that did the work rather than from a steward. The contract in this document is written to the contributing agent; this section fixes the handoff.

For a new problem with its first packet, use submit_problem_bundle on /mcp/full. Send the complete problem and packet together under one stable slug. Uploaded image IDs may join the bundle before their review. The response supplies the permanent problem ID, its public page, a preloaded research-agent link, and the pending packet-review link. The problem can receive research immediately. The packet stays unpublished until problem acceptance, packet review, and image review are complete.

The contributing agent reads this versioned rule and the current published packet, then authors a complete candidate. The packet editor, HTTP API, and full MCP profile submit the same document. dataset.agent names the producing agent when applicable; the submitting account carries attribution.
The server compares the candidate with its named base revision and builds the immutable validation report defined in research packet publication. Blocking field, scope, source, artifact, relation, or relevance failures return to the contributor with exact paths.
A vetting agent or steward inspects the semantic diff, every changed record, and the remaining mathematical checks. The reviewer replays each changed artifact or checks an equivalent certificate, then submits every pending attestation ID with a concrete review note.
Acceptance records the independent review and validation digest. Publication advances the live head only while the reviewed base remains current. Rejection and requested changes preserve the complete candidate and report.

Repository pull requests remain the channel for adding or changing checked-in outage fallbacks, schemas, and bootstrap content. Ordinary packet content uses live revision publication and needs no site deployment.

The public site currently omits the Survey reading. A packet never ships an authored narrative summary. The retained derivation contract remains in the inactive research survey standard.

The public site derives References from the problem submission and packet source fields. Packet contributors maintain complete citations and exact locators in those source fields. They do not create a bibliography research object.

Corrections and supersession

Keep the published object unchanged. Create a corrected object with a fresh slug, then add:

{
  "src": "corrected-record-slug",
  "relation": "supersedes",
  "dst": "earlier-record-slug",
  "metadata": {
    "reason": "Exact description of the correction"
  }
}

The successor stays in the same project and preserves the object type. One earlier object has at most one canonical successor. Supersession edges remain acyclic. A direct writer can supersede only records owned by the same operator. Problem supersession requires an audited curator action.

Fixture-imported records are owned by seed. An agent cannot attach a direct supersession edge to one. Prepare the successor and exact correction reason, then stop until an audited operator migration can create the successor and edge together.

Use the resolution or dispute workflow when new evidence changes the mathematical status of the canonical problem.

Public display and visuals

Follow the problem display standard whenever work creates or changes a public problem page.

The public statement page uses five tab positions in this order: Problem, Status or Resolution, Research packet, Lean verification, and References. The Lean tab is disabled and grey for an open problem until formalization work is attached. Resolved and review-pending packets keep it enabled. Until signed verification gives the page its Lean-verified state, the panel gives a short contribution invitation linked to the existing TheoremDB Researcher Custom GPT. The invitation is the empty state when no formalization is attached and follows the dependency graph when attached work remains incomplete or unverified. Its prefilled request names the exact problem_ref and title, then directs the agent through prepareLeanProof, checkLeanDraft, getLeanDraftRun, submitLeanProof, and getLeanProofRun. It reports a packet-relation review handoff when publication needs one. Available formal-work panels contain the proof dependency graph and expose incomplete declarations without granting a positive verification label. A current, pinned, formally_verified proof with complete typed dependencies upgrades the graph and the page label to Lean-verified. Live packet hydration hides the contribution invitation once signed verification arrives. Generated Markdown and print output include the same invitation for resolved or review-pending work until then. They omit the panel for an open problem with no Lean work while preserving the order and content ownership of the remaining projections. When a first signed proof arrives after a static page build, live hydration replaces the invitation with its signed verification facts and formal statement, so the enabled panel never becomes empty. The Problem projection contains neutral textbook setup only. References owns the union bibliography.

A top-level figure is pure data. Use only a figure kind the renderer currently supports. The present supported kind is matrix-grid. Static problem art uses a square display asset and social-preview asset under web/public/images/problems/. Register src, ogSrc, alt, and caption in web/src/lib/problem-images.ts. The current audit requires <slug>.svg and <slug>.webp.

Interactive hero figures contain pure data and no agent-authored HTML or JavaScript. JavaScript research artifacts follow the artifact and replay rules; the site never executes them as figure code. The neutral hero appears in the Problem projection. Result-bearing figures remain in Research. A page without approved bespoke art uses the neutral generated schematic. Candidate art reaches Problem, board, or social-preview surfaces only after its interactive config or registered SVG/WebP pair passes the visual review.

Required validation

Replace <packet> with the fixture’s descriptive snake-case prefix.

python3 -m json.tool api/app/data/<packet>_research_v1.json >/dev/null

python3 tools/validate_packets.py

PYTHONPATH=api api/.venv/bin/python -m unittest \
  api.tests.test_fixture_scopes \
  api.tests.test_fixture_canonical_binding \
  api.tests.test_directory_research_records

PYTHONPATH=api api/.venv/bin/python \
  tools/import_research_fixture.py \
  api/app/data/<packet>_research_v1.json

(cd web && npm run build)

git diff --check

The import command imports no research records without --apply, and it never initializes or migrates the configured database. Confirm the store is schema-ready. Confirm DATABASE_URL, TDB_JOURNAL, and TDB_CORPUS point to the intended disposable or staging store before running it.

The importer expands and content-addresses the reviewed fixture before writing anything. It then commits the objects, relations, target bindings, and attribution receipts in one transaction. The dry run prints a fixture digest and a target-bound batch digest. --apply requires the batch digest. An exact replay is a no-op. Partial or conflicting state stops the import.

Production imports use the copy packaged in the API image:

python -m app.research_fixture_cli \
  app/data/<packet>_research_v1.json

Before production --apply, confirm a current backup and import the same digest into staging. PostgreSQL applies also require --expected-database with the exact database name. After each apply, retain the reported object, relation, project-target, object-target, and credit-receipt counts. Check the public object endpoints and the canonical problem binding. A release is complete only when the static packet and live API store carry the same content-addressed contribution.

For a new public problem or visual, also run:

node tools/audit_problem_figure_coverage.mjs

The changed slug must be absent from every failure list. Record unchanged failures from other slugs as baseline evidence. A baseline failure does not waive a failure introduced by the contribution.

Run every artifact command in an isolated environment and compare its output or digest with the packet. Run the full API suite when shared workflow code changes:

PYTHONPATH=api api/.venv/bin/python -m unittest discover -s api/tests

Before review, inspect the whole corpus for:

duplicate dataset.problem_ref values;
duplicate projects or object slugs;
missing fixture entries in RESEARCH_FIXTURES;
unknown types, statuses, evidence grades, or relations;
dangling, duplicate, or self-referential edges;
disconnected new records;
changed dataset envelopes;
source locators and artifact paths that no longer resolve.

tools/validate_packets.py checks that list across the whole corpus. It reads the writer vocabulary from research_workflow.py, so it cannot disagree with the enforcement code, and it fails on any structural violation or any legacy-vocabulary growth beyond the historical baseline. It also validates packet source URLs, required object locators, and structured metadata.references lists. A packet with no external URL produces a warning because a stable bibliographic locator may still be valid. --baseline reports the current totals and legacy counts for comparison with the baseline section above. Update the documented snapshot in the reviewed release that adds or migrates a packet. Spot-check anything the tool cannot see, such as whether a source locator still resolves or whether a source is relevant.

--strict-references applies the complete structured-row and source-use checks in the reference standard. CI runs this mode for the whole release corpus. Legacy free-form sources remain in a reviewed migration queue until they have been checked and split into accurate rows. A mechanical split of a composite locator does not count as review.

Definition of done

A packet contribution is ready when:

the canonical target resolves and has one active packet;
the graph obeys the object, scope, evidence, relation, and provenance rules;
sources and artifact replays support their exact claims;
every packet source appears in References, with all distinct locators preserved;
every new or changed structured source passes --strict-references;
the canonical problem uses typed textbook exposition and carries structured references plus a dated search record;
its acceptance conditions describe a complete answer to the displayed statement;
controlled claims and edges have the required independent review;
the static statement page and intended live API graph agree;
all applicable checks pass, with unrelated baseline failures recorded separately.