How to read a claim

A claim is a heading followed by a tag. The tag's first line is the tier, which says how the claim is known, and may give in parentheses the range or population it was checked over. The next line names the program that checks it (Verifier), or says the proof is written in the block, or both ("proof; program.py"), or for another author's result cites it (Source). A tag may carry several tiers, split by semicolons, each naming the part of the claim it covers, in parentheses or after "for", and a part inside a tier's parentheses may carry a tier of its own; a tier that names no part covers the rest. In "theorem; observation (the birthdays for m ≤ 200)" a formula is proved and its values are listed from a computation. Listings show the first two tiers outside parentheses. A heading that names a tier is a claim of that tier, or another author's result kept under its own name. The parameter a tier speaks of is whatever the claim varies: a modulus, a depth, a discriminant, a bound.

Property

It follows from the definitions, by an argument the block writes out.

Observation

Computed or noticed, not proved, at one or a few values of the parameter.

Pattern

Observed across many values of the parameter, with no proof. The tag states the population it was read over.

Rule

Proved algebraically, or verified exhaustively across a stated range, which the tag gives in parentheses whenever the rule rests on a check: a rule verified up to a bound says nothing past it. A proved rule stops short of a theorem where its proof leans on computation at specific values or its scope is narrower than its object's.

Criterion

A necessary and sufficient condition, proved.

Theorem

A complete proof holding for every value in scope, with no computation at specific values standing in for an argument.

Known

Another author's established result, cited by its source and kept under its own name.

A note on small cases

A number read off a small case is printed as a small case. Where a program is the verifier, it is served verbatim, and its page carries an anchor at each top-level function, where a citation lands, lists every claim it checks and names what a run of it needs: the other programs and the outside packages.