Cards schema reference

The canonical wire format for Lemma cards is defined as a single JSON Schema document at schema/card.v0.1.json. This page summarises the shape of every variant; the schema file itself is the authority.

Identifier	Value
$id	https://openlemma.dev/schema/card.v0.1.json
Spec version	JSON Schema 2020-12
Discriminator	top-level kind field
Licence	MIT

A card is a oneOf over four variants — principle, ops, hypothesis, unidentified. Every variant is closed (additionalProperties: false); unknown fields fail validation.

---

PrincipleCard

The structural shape used for physics, chemistry, biology, climate, mathematics, engineering, and numerical methods. The discriminator is structural, not subject-area — the actual domain lives in the domain field.

Field	Type	Required	Notes
kind	const "principle"	yes	Variant discriminator
id	string, kebab-case	yes	Pattern ^[a-z][a-z0-9-]*$. Stable and never reused once published.
version	semver string	yes	MAJOR for breaking convention changes, MINOR for added limits, PATCH for typos / refs.
name	string	yes	Human-readable title.
domain	string	no	Subject area, e.g. "physics-condensed-matter", "chemistry-electrochemistry". Conventional values are listed in the schema.
principles	string array	yes	The underlying physical / mathematical principles in plain English.
formulaTeX	string	yes	Canonical equation in LaTeX. KaTeX-renderable.
conventions	string array	yes	Sign conventions, unit conventions, coordinate frames.
expectedLimits	string array	yes	Plain-English asymptotic / boundary expectations.
references	string array	yes	Canonical sources — textbooks, papers, official documentation.
validationEnvelopes	object	no	Numerical bounds asserted at runtime. Keys are domain-conventional (e.g. gEarth_m_per_s2); values are either [min, max] tuples or richer objects.
crossMethodTolerances	object	no	How far two independent methods may disagree on the same observable before the disagreement is a finding. See Cross-method agreement.
formula	MachineFormula	no	Machine-readable counterpart to formulaTeX — see MachineFormula.
seriesConditions	array	no	Conditions every reported sample must satisfy — see seriesConditions.
convergence	object	no	Qualifies how a claimed convergence order is measured — see convergence.
metadata	CardMetadata	no	Authorship and review tier. Stripped before the card reaches a model — see Card metadata.

MachineFormula

formulaTeX is written for a human reader and carries presentational markup; it is not something a program can evaluate. formula is the machine-readable counterpart. Both are kept, because they serve different readers.

Field	Type	Required	Notes
expr	string	yes	Plain-ASCII expression, e.g. "y0 + v0*t - (1/2)*g*t**2". Same grammar as the dimensional check’s expr, so the corpus has one expression language rather than two.
symbols	object	yes	Every free symbol in expr, mapped to its DimVec.
relation	string	yes	What the expression actually encodes, in plain English.

relation is required, and the reason is worth stating plainly: expr need not be a transcription of formulaTeX. A card may state the integrated form for a human and the differential form for a machine. free-fall-uniform-gravity does exactly that — its formulaTeX is the position form y(t), its expr is the net force -m*g. Both describe the same physics at different levels of integration. Without relation, a consumer would assume they are the same relation and compare two expressions that were never meant to match.

A card must declare formula before a hypothesis card’s limit claim can name it as the thing it reduces to.

seriesConditions

Conditions every reported sample of a quantity must satisfy.

"seriesConditions": [
  {
    "of": "g",
    "op": ">=",
    "value": 0,
    "basis": "a density of states counts levels per unit energy, so it is non-negative by definition"
  },
  {
    "of": "imChi0",
    "op": "<=",
    "value": 0,
    "where": { "of": "omega", "op": ">", "value": 0 },
    "basis": "passivity: a system cannot supply energy to the perturbation driving it"
  }
]

Field	Type	Required	Notes
of	string	yes	Which reported quantity this constrains.
op	< <= > >=	yes
value	number	yes
where	{of, op, value}	no	Restricts which samples the claim covers.
basis	string	no	Why the condition holds.

This is not a small validationEnvelopes. An envelope bounds a magnitude; these bound a sign or relation, which can be universal where a magnitude is not. That is why cards deliberately carrying no envelope can still carry these — density-of-states and joint-dos are both envelope refusals, because a DOS scales with cell volume and band count, yet neither can ever be negative.

where is load-bearing, not a convenience. Im chi_0(omega > 0) <= 0 says nothing about negative frequencies, where Im chi_0 is legitimately positive. Without the restriction the check would report a violation the card never asserted — turning correct physics into a failure.

Conditions are structured rather than written as expressions on purpose: an expression language would need a computer-algebra system to evaluate, which would make the check Python-only like symbolic verification. Every such claim in the corpus fits this shape without algebra.

convergence

Qualifies how a claimed order of accuracy is measured.

"convergence": {
  "maxPerLevelSpread": 0.4,
  "basis": "matches the ±0.2 acceptance width on this card's observedConvergenceOrder envelope"
}

Field	Type	Required	Notes
orderKey	string	no	Which validationEnvelopes key holds the expected order. Defaults to observedConvergenceOrder.
maxPerLevelSpread	number > 0	no	How far per-level orders may spread before the study stops supporting an estimate at all.
basis	string	no	Why this number.

maxPerLevelSpread exists because it decides verdicts — it separates “this refinement study is not a clean power law” (warn) from “the method converges at the wrong rate” (fail). It began as a constant inside the engine, which put a judgement in the engine that everywhere else in Lemma lives in the card with a recorded reason.

Omit it and a documented default applies — but the verdict then says so, naming the source of the number that decided the outcome (declared by <card>, supplied by the caller, or the engine default, not declared by this card). A fallback is fine; a silent fallback is not.

---

OpsCard

Parameterised templates for scripting and job-submission tasks (SLURM, Snakemake, Singularity recipes).

Field	Type	Required	Notes
kind	const "ops"	yes	Variant discriminator
id	string, kebab-case	yes	Same pattern as PrincipleCard.id
version	semver string	yes
name	string	yes
description	string	yes	One-paragraph plain-English summary.
parameters	array of OpsParameter	yes	Each entry: { key, label, defaultValue, required, note? }
validation	string array	yes	Validation rules in plain English.
references	string array	yes	Sources.
metadata	CardMetadata	no	Authorship and review tier. Stripped before the card reaches a model — see Card metadata.

OpsParameter

Field	Type	Required	Notes
key	string	yes	Identifier used by the template engine.
label	string	yes	Human-readable label.
defaultValue	string	yes	Default; empty string allowed.
required	boolean	yes	Whether the template requires this parameter at instantiation.
note	string	no	Free-form explanation, rendered alongside the label.

---

HypothesisCard

Proposed extensions to the corpus — generated by an LLM, by a human, or by symbolic regression. Explicitly not yet verified; the cross-check engine consumes the declared checks to decide whether the hypothesis can be promoted to a principle.

Field	Type	Required	Notes
kind	const "hypothesis"	yes
id	string, kebab-case	yes
version	semver string	yes
name	string	yes
proposal	string	yes	Plain-English statement of what the hypothesis claims.
proposedFormulaTeX	string	yes	The proposed equation in LaTeX.
derivedFrom	object	no	{ cardId: string, relationship: "extends" | "replaces" | "complements" }
checks	HypothesisChecksSpec	yes	The cross-checks the engine should run.
references	string array	yes
origin	enum	yes	"llm", "human", or "symbolic-regression".
rationale	string	no	Why this hypothesis was proposed.
metadata	CardMetadata	no	Authorship and review tier. Stripped before the card reaches a model — see Card metadata.

HypothesisChecksSpec

Field	Type	Notes
dimensional	object	lhsLabel/lhsDims/rhsLabel/rhsDims (canonical DimVecs). Optionally expr (a plain-ASCII RHS expression, e.g. "(1/2)*m*v**2") + symbols (map of symbol → DimVec): when both are present the engine derives the RHS dimensions from the formula and checks them against lhsDims, instead of trusting the declared rhsDims.
limits	array	Each entry: { name, regime, expectedReducesTo } in prose, plus an optional machine form — see Machine-readable claims. Without a machine form the claim is recorded and returns warn.
conservationLaws	array	Each entry: { law, statement }, plus an optional evolution block — see Machine-readable claims. law names the quantity and is free-form; conventional values are energy, momentum, charge, particle-number, total-spin, parity, mass, probability, lyapunov-function.
referenceCorpus	object	{ mustAgreeWith?: string[], mayContradict?: string[] }. The engine resolves every id against the live corpus.

DimVec

Canonical dimension vector. Each axis is an integer exponent on a primitive dimension. Omitted axes default to zero.

Axis	Meaning	Notes
L	length
T	time
M	mass
E	energy
Q	charge
Theta	temperature	Renders as Greek capital Θ in human output.
N	particle count

---

Machine-readable claims

A hypothesis card states its limit and conservation claims in prose, for a human. It may additionally state them in a form a program can evaluate. Prose alone is recorded and returns warn — the engine confirms the claim is well-formed and says so honestly, rather than implying it was tested.

Discharging these claims requires the symbolic adapter, which is opt-in and Python-only. The fields below are part of the schema regardless, so a card carrying them is valid and portable whether or not anything in the pipeline evaluates them.

Limit claims

limits[] originally held one field, regime, describing “the thing that happens in this limit”. In practice cards were using it for four different operations, which give different answers:

Field	Operation	Example
limit	{ symbol, to } — a genuine limiting process. to takes 0, oo, -oo, or a numeric literal.	b -> 0
substitute	map of symbol → expression — setting a variable	y = 0
solveFor	{ symbol } — a root: the value at which the expression vanishes	terminal velocity is the v where net force is zero
fixedPoint	{ system, solveFor, parameters?, conditions? } — a stationary point of a coupled system	the coexistence equilibrium of a predator-prey model

Exactly one may be declared. A claim carrying two is ambiguous rather than richer, and the engine says so instead of guessing.

The distinctions are not pedantry. A substitution and a limit disagree wherever the function is discontinuous at the point. A root is not a limit at all. And a fixed point of a two-equation system cannot be found from one equation — which is why fixedPoint declares its own system rather than assuming the card’s single formula is the whole story.

target says what the claim reduces to, in one of three forms:

Form	Meaning
{ cardId }	another corpus card, which must then declare a formula
{ expr }	an inline expression
{ point }	map of symbol → expression, for a fixedPoint — an equilibrium is a tuple, not a single value

conditions — which fixed point

A coupled system usually has several stationary points, and a predator-prey model is exactly as stationary at extinction as at coexistence. Verifying stationarity alone would therefore accept (0, 0) for a claim about coexistence. conditions is the list of inequalities that select the intended branch:

"conditions": ["y > 0", "gamma/delta < K"]

A condition that is demonstrably false refutes the claim. One that cannot be decided without sign assumptions on the parameters leaves the stationarity verdict standing and is reported as unverified — an undecidable side condition must not retract a result that was actually established.

parameters

Names the block introduces beyond the card’s own declared symbols. Declared rather than inferred, because several ordinary physics parameter names — gamma, beta, zeta, lambda, pi — collide with functions and constants in the algebra system. An unbound collision does not necessarily raise; pi*r**2 parses cleanly as 3.14159…, silently computing a different expression than the card declared. Nothing here is guessed.

Conservation claims

conservationLaws[].evolution describes how a declared quantity changes along the system’s dynamics:

Field	Type	Required	Notes
quantity	string	yes	The conserved or dissipated quantity, e.g. total mechanical energy.
system	array	yes	Each entry { of, expr } — the time derivative of a state variable.
rate	string	yes	The claimed time derivative of quantity. "0" means genuinely conserved.
parameters	string array	no	As above.

law is free-form, like domain. It was a closed list of six physics values until the corpus demonstrated the problem: lotka-volterra-with-logistic-prey is a population-dynamics card whose claim is about a Lyapunov function, and the enum left it no option but to declare law: "energy" — after which its own statement opened “No conserved energy-like quantity.” A vocabulary that forces a card to mislabel itself is not a constraint worth keeping. Use a conventional value where one fits; invent one where none does.

Note that the check compares against a declared rate rather than testing whether the derivative vanishes. That is deliberate: both cards in the public corpus that carry a conservation law assert a quantity is not conserved, at a specific rate — mechanical energy under linear drag (dE/dt = -b v²), and a Lyapunov function under logistic predation. A checker that only asked “does this vanish” would have covered neither.

---

Cross-method agreement

validationEnvelopes bounds what a single run may produce. crossMethodTolerances sits one relation higher: it bounds how far two independent methods may disagree with each other.

Keys match the output keys engines emit, exactly as validationEnvelopes does.

"crossMethodTolerances": {
  "latticeConstant_A": {
    "relative": 0.01,
    "gating": true,
    "basis": "the scale at which independent all-electron and pseudopotential codes are held to agree in the Delta-gauge reproducibility studies"
  },
  "bulkModulus_GPa": {
    "absolute": 25.0,
    "gating": false,
    "basis": "reported for information only — B_0 depends on curvature and is dominated by basis quality"
  }
}

Field	Type	Required	Notes
relative	number > 0	one of	Maximum fractional spread, about the mean.
absolute	number > 0	one of	Maximum spread in the observable’s own unit.
gating	boolean	no	Whether disagreement fails the verdict. Defaults to true; set false for observables you report but know to be method-sensitive.
basis	string	no	Why this number — the citation or reasoning behind it.

Exactly one of relative / absolute per observable. Declaring both would leave which one binds ambiguous.

For each key reported by at least two methods, the spread (max − min) is tested against the tolerance. A single method raises rather than passing: it cannot corroborate itself.

basis exists because a bare number is unreviewable. A tolerance with no recorded provenance cannot be argued with later — when a run fails it, nobody can say whether the bound or the engine was wrong. The same gap still exists on validationEnvelopes, which has nowhere structured to record it.

The comparator is available as a library function in both SDKs (runAgreementChecks / run_agreement_checks). It is deliberately not exposed as an MCP tool.

---

UnidentifiedCard

Sentinel returned by the IDENTIFY phase when no card honestly matches the request. Surfaced verbatim instead of fabricating a fallback.

Field	Value	Notes
kind	const "unidentified"
id	const "none"
version	const "0.0.0"
name	string
reason	string	Why nothing matched.

---

Card metadata

Every card variant may carry an optional metadata block recording who wrote the card and how far it has been reviewed. It is additive: cards without it remain valid.

Field	Type	Required	Notes
authors	array of Author	yes	At least one. Every card credits a human.
tier	enum	no	"bronze", "silver", or "gold" — the review level reached.
created	string	no	Date the card was first written.
updated	string	no	Date of the last substantive change.

Author

Field	Type	Required	Notes
name	string	yes
orcid	string	no	Preferred stable identifier for academic authors.
github	string	no
role	enum	no	"author", "curator", "reviewer", "translator", or "maintainer".

Why it is separated from the card body

cards_get removes metadata before returning a card. A model asking the substrate for a principle receives the physics and nothing about who wrote it. That is deliberate, and there are four reasons:

• Authority bias. A verification substrate should not encourage a model to weight a claim by the prestige of its author. The card is correct or it is not; who curated it is irrelevant to that judgement.
• Privacy. Author names, ORCIDs and affiliations would otherwise be sent to a third-party model provider on every single tool call.
• Token budget. Metadata is dead weight in a context window that is paying for physics.
• Training-data hygiene. Anything that reaches a model can end up in a future training corpus. Author identity is not a physical property and should not become a learned feature.

Metadata is for humans, attribution tooling, and the review process — read it from the card files or the Python SDK, not from the MCP tool surface.

"metadata": {
  "authors": [
    { "name": "Ada Lovelace", "orcid": "0000-0000-0000-0000", "role": "curator" }
  ],
  "tier": "silver"
}

---

Validating a card

npx ajv-cli@5 validate --spec=draft2020 \
  -s schema/card.v0.1.json \
  -d "cards/**/*.json"

or in Python:

from artano_lemma import validate_card_payload, parse_card

# Strict validation against the schema:
validate_card_payload(my_card_dict)

# Or validate + parse to a typed model in one call:
card = parse_card(my_card_dict)

See the Python SDK page for the typed models and the validator.