Schema

The frontmatter contract for statements and problems, for humans and agents

Conjura has three content layers. Only the first two carry a schema; the third (facets) is generated, never authored.

Statement frontmatter

Field Type Notes
id string Four-digit zero-padded, matches the c/<id>/ directory name.
problem string Exactly one hub slug under p/.
title string Precise, fully-quantified.
short_title string For listing-table columns; falls back to title.
areas list of string Subset of the 19 fixed area slugs below. First entry is primary, display only – never a home directory.
model enum rom | prom | icm | ggm | qrom | standard | other
form enum separation | lower-bound | tight-bound | equivalence | impossibility | assumption | characterization
assumption_class enum unconditional | falsifiable | non-falsifiable
category enum research-open | research-solved | test | api | withdrawn. Solved special cases and sanity lemmas (research-solved, test) belong on the site – a disproof of an easy case is often the signal that a definition was formalized wrongly.
statement_sha string 64-char hex sha256 of the ## Statement tab content. Script-maintained by scripts/status_badge.py; never hand-edit.
revision integer Bumped automatically when statement_sha changes.
status map Six graded fields: statement_informal, statement_formal, statement_match, proof_informal, proof_review, proof_formal. Plus proof_direction (proves | refutes), optional, defaulting to proves: which way the work points. It is not a grade and never enters σ or π; refutes requires proof_informal != open. See the status legend.
status_badge string Generated. Never hand-edit.
status_summary string One required sentence, rendered next to the badge in listing tables.
status_updated date
relations list of map {kind, target, note?}. kind is one of generalizes, specializes, implies, implied-by, equivalent-to, strengthens (same claim, better quantitative bound), variant-of, refutes, refuted-by, superseded-by. target is a four-digit id. note is required on an equivalent-to edge whose proof grades disagree.
lean map mode (in-repo | external-lean4 | other-system | none), plus repo/commit/path/decl/toolchain as applicable. commit is required once status.statement_formal != open when mode: external-lean4.
sources list of map {cite, url}. Real citations only – never a specific author/venue/year citation that hasn’t been verified to exist; leave the list empty rather than invent one.
withdrawn_reason string Required when category: withdrawn. A withdrawn statement is never deleted and never 404s – its page stays up as a tombstone, together with a {kind: superseded-by, target: ...} relation pointing at whatever replaced it.

difficulty

Required, a mapping of three keys, and the only graded field on a statement that is not part of the badge.

difficulty:
  reach: new-idea        # routine | adaptation | new-idea | barrier
  by: ai                 # ai | human
  note: "one sentence saying what is missing, and checkable"

reach measures distance from known technique, not effort and not likelihood; the status legend says what each value means. by records who judged, on the same rule as status: a machine never writes human. note is required, because a grade with no stated reason cannot be argued with.

The 19 fixed area slugs

foundations, idealized-models, impossibility-results, symmetric-key, information-theoretic, side-channel, public-key, lattices, isogenies, quantum, zk, proof-systems, homomorphic-encryption, obfuscation, mpc, secret-sharing, universal-composability, privacy, consensus.

These are kept in sync between _quarto.yml’s sidebar and scripts/build_index.py’s AREA_SLUGS. Do not rename or merge them silently – see CONTRIBUTING.md.

Body sections, in order

  1. Badge markers (<!-- status:start -->...<!-- status:end -->), generated – the single combined ring+disc badge plus its one-line caption, at the very top of the page, before the tabset.
  2. A ::: {.panel-tabset} with ## Statement (the block statement_sha hashes), ## Proof, ## Formal Artifact.
  3. ## Open obligations – a markdown task list of the concrete outstanding items (unverified steps, unaudited files, unmatched formalizations, missing sanity lemmas). The open count feeds a listing column.

There is no rendered Status, Sessions, or Changelog section on the page. status_summary is still a required frontmatter field (it’s what shows next to the badge in listing tables), it’s just not restated in page prose – the badge’s own caption is the brief explanation shown on the page itself. The same single combined badge (ring and disc together) is used everywhere: in the frontmatter’s status_badge field, at the top of the page, and in every listing table. Session dumps still live in each leaf’s sessions/ folder for provenance (excluded from the site); revision history is tracked by revision/statement_sha and by the commit that changed them – see CONTRIBUTING.md for the same-id-vs-new-id rule and where a misformalization classification belongs.

See _templates/statement.qmd for a fully commented skeleton.

What the badge gate scans

scripts/status_badge.py scans c/ and papers/ by default, and CI runs it as --check c papers. A paper under papers/ carries the same badge contract as a statement – the same status: fields, the same hashed ## Statement tab, the same generated status_badge – so the same staleness gate applies to it.

Hubs under p/ are not scanned. A hub carries no badge of its own, only an aggregate view over its children, so it has no status: block for the script to grade. Pages without a status: block are skipped in any case; naming the two roots explicitly is about intent, so that putting a status: block on a hub is a deliberate schema change rather than something the script quietly starts generating a badge for.

Problem frontmatter

Just title and an optional subtitle. The body carries motivation, provenance/history, a parameter lattice (a table whose axes are the independent dimensions the family varies along, each cell linking to the occupying leaf, empty cells marked unstated as research prompts rather than left blank), and a listing of the hub’s own children. See _templates/problem.qmd.

Machine-readable index

scripts/build_index.py emits conjura.json at the site root: every statement, keyed by id, with its full frontmatter, parsed obligations, and resolved relations. This is generated (gitignored, rebuilt by CI before every render) – read it, never hand-edit it. It’s the interface external tooling (for example a proof-campaign harness) consumes as a work queue.

Identifier and revision rules

See CONTRIBUTING.md for the full editorial rule on when a change needs a new id versus a revision bump on the same one.