Cards, completely

A card is the heart of Lemma. Everything Lemma knows lives in cards. So if you understand cards, you understand what Lemma can actually check. We’ll build this up from nothing.

Words used on this page

• Card — one small file describing one piece of science (one formula and the facts about it). Like an index card in a recipe box, but for a scientific principle.
• JSON — a plain-text way to write data as labels and values, e.g. "name": "Ideal gas law". Cards are written in JSON.
• Schema — a template that says which labels a card must have and what type each value should be. Like a paper form with required boxes: fill it in wrong and it’s rejected.
• Units / dimensions — what a number is measured in (metres, seconds, kilograms…). Explained in full below.

What a card looks like

A card is just a text file with labelled facts. Here’s a real one, trimmed down, so you can see the shape before we explain it:

{
  "kind": "principle",
  "id": "ideal-gas-law",
  "version": "1.0.0",
  "name": "Ideal gas law",
  "formulaTeX": "P V = n R T",
  "conventions": ["T in kelvin (never °C)", "R = 8.31446 J/(mol K)"],
  "expectedLimits": ["as T -> 0, P -> 0 at fixed volume"],
  "references": ["any introductory thermodynamics text"]
}

Read it like a fact sheet: what kind of card it is, a short id (its nickname), a name, the formula, some notes about the symbols, how it should behave in extreme cases, and where it comes from. That’s a card.

Why JSON, and not Markdown?

A fair question — especially since this docs site is written in Markdown. The rule of thumb: cards are data read by programs, so they’re JSON; Markdown is prose read by people.

• A card is read by machines, not humans. The checker, the MCP server, and the Python library all need to pull exact values out of a card — like { "M": 1, "L": 2, "T": -2 }. JSON stores that as real structured data that every programming language reads the same way. You can’t reliably dig a dimension out of a paragraph of prose.
• JSON can be checked automatically; Markdown can’t. The template (card.v0.1.json) is enforced by a standard JSON validator — that’s what guarantees the required fields, correct types, and valid ids, and what powers the “Lemma refuses broken cards” promise.
• AIs propose cards as JSON. When a model suggests a new formula, it hands over a JSON object the engine reads directly — not an essay.
• Markdown is still here — as the output. Tools like ops_get take a card’s JSON and render it as readable Markdown. The JSON is the source of truth; the Markdown is the nice view generated from it.

The one downside: JSON is fiddlier to type by hand (especially LaTeX, with its \\ escaping). We accept that because cards are read far more often than they’re hand-written — and the readable view is generated for you.

One template, four kinds of card

Every card must follow the same template (the schema) so that programs can read them reliably. A label called kind says which of four types it is:

flowchart TD
  S[the template<br/>one schema] --> P[principle<br/>a known law<br/>33 cards]
  S --> O[ops<br/>a reusable script template<br/>3 cards]
  S --> H[hypothesis<br/>a proposed, unproven idea<br/>2 cards]
  S --> U[unidentified<br/>a placeholder]
  classDef s fill:#1e3a5f,stroke:#4a90d9,color:#fff;
  class S s;

• principle — an established scientific law (the workhorse).
• ops — a reusable template for a routine task, like a script to run a job on a supercomputer.
• hypothesis — a proposed idea that hasn’t been verified yet (often something an AI just suggested).
• unidentified — a placeholder the system returns when it has nothing matching, instead of guessing.

Two different labels — don’t mix them up

kind is the type of card (principle, ops, …). domain is the subject (physics-thermodynamics, chemistry-kinetics, …). Splitting them is what lets the same template hold a physics law and a biology law equally well.

Every card, whatever its kind, shares a few basics: kind, an id (lowercase-with-dashes, e.g. ideal-gas-law), a version (a number like 1.0.0), a name, and references.

The principle card, field by field

This is the main kind. Here’s what each label means, in plain words:

Label	Plain meaning
kind	always "principle" here
id	the card’s short nickname
version	which revision this is (e.g. 1.0.0)
name	the human-readable title
principles	the assumptions it rests on
formulaTeX	the formula, written in LaTeX (a standard way to type maths)
conventions	what the symbols mean, the units, and gotchas
expectedLimits	how it should behave in extreme cases (e.g. “as temperature → 0…”)
references	where it comes from (citations)
domain	(optional) the subject area
validationEnvelopes	(optional) sensible numeric ranges the values should fall in

The conventions and expectedLimits aren’t just comments — they’re the things the checker actually tests against a piece of work.

Units, from scratch (you’ll need this everywhere)

Every physical quantity is measured in units. Speed is length per time (metres per second). Energy is mass times length-squared per time-squared.

The golden rule: you can only equate two things with the same units. “3 metres = 3 seconds” is meaningless — it’s an automatic mistake, no calculation needed. Catching exactly this kind of mistake is one of Lemma’s superpowers.

To do that by computer, Lemma writes units as a short list of numbers: how many of each base unit you have. There are seven base units:

Symbol	L	T	M	E	Q	Theta	N
meaning	length	time	mass	energy	charge	temperature	amount

A number next to a symbol is its power (how many times it’s multiplied); anything not listed is zero. So:

• speed = length ÷ time = { "L": 1, "T": -1 } (“one length, one over time”)
• energy = mass × length² ÷ time² = { "M": 1, "L": 2, "T": -2 }

The one rule to remember

The power goes in the value, never in the label. Length-squared is { "L": 2 } — not { "L^2": 1 }. This trips people (and AIs) up constantly.

The hypothesis card (a proposed idea)

A hypothesis card is an idea that hasn’t been verified yet — so it must pass the checker before anyone trusts it. It’s almost like a principle card, but it says “proposed” everywhere and adds a section describing what to check:

• proposal — a one-sentence statement of the idea;
• origin — who suggested it (llm = an AI, human, or a maths program);
• derivedFrom — which existing card it builds on;
• checks — the things the engine should verify (units, references, limits…).

The units check can include the actual formula so the engine can work the units out itself rather than trust what the author wrote:

"dimensional": {
  "lhsLabel": "force",  "lhsDims": { "M": 1, "L": 1, "T": -2 },
  "rhsLabel": "-m g - b v", "rhsDims": { "M": 1, "L": 1, "T": -2 },
  "expr": "-m*g - b*v",
  "symbols": { "m": {"M":1}, "g": {"L":1,"T":-2}, "b": {"M":1,"T":-1}, "v": {"L":1,"T":-1} }
}

Here expr is the formula in plain typing, and symbols says the units of each letter. Given those, the engine multiplies and adds up the units itself. (The engine page shows this in action.)

The remaining two kinds — ops (script templates) and unidentified (placeholder) — are listed field-by-field in the full schema reference.

Make your own card and check it

1. Write a text file following the field tables above.
2. Validate it — i.e. check it fills the template correctly. One command does this:

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

(ajv is a tool that checks JSON against a schema. The --spec=draft2020 part just tells it which version of the schema rules to use — leave it out and it uses the wrong one and complains.) A good card prints valid; a bad one prints exactly what’s wrong and stops.

flowchart LR
  W[write your card] --> V{does it fit<br/>the template?}
  V -->|yes| C[(added to the library)]
  V -->|no, here's why| W
  C --> E[the checker can now use it]

Trust levels (bronze / silver / gold)

Not every card is equally trusted. Community cards earn a level as they’re reviewed — think of it like product reviews:

flowchart LR
  B[bronze<br/>submitted, fills the template] --> S[silver<br/>checked for correctness] --> G[gold<br/>fully vetted and widely cited]

Today the level is tracked during review; a future schema version will record it on the card itself. See Authoring a card for how to contribute one.

Mistakes people make

• Putting the power in the label. {"L^2": 1} is wrong; write {"L": 2}.
• Using °C. Temperatures should be in kelvin unless you say otherwise.
• Vague limits. “behaves nicely” checks nothing; “as T → 0, k → 0” is a real, testable statement.
• Forgetting --spec=draft2020. The validator then uses the wrong rules and rejects perfectly good cards.
• Referring to a card that doesn’t exist. Any id you mention must really be in the library, or the check flags it.

Next

• The engine, completely — how a card becomes a verdict.
• The schema reference — every field of every kind.