A theorem the package is sold on, as lean2js read it out of the build: the signature Lean prints for it, and the docstring written above it.

A constant a shipped theorem's statement names. @[expand] writes a def out where it is called, so the package holds the number and not the name — and a reader of the claim would have no way to learn what refundWindowMs is. The value is carried here so that the signature the manifest publishes has no symbol in it the package cannot answer for.

What a package is emitted from. Only manifest is written by hand; lean2js reads the program and the public theorems out of the manifest's namespace.

docs pairs an export with the docstring written above the def it was read from. A consumer reads the .d.ts and the package's README and nothing else, so what the author wrote about a function has to reach both.

Kept alongside the lakefile's version; scripts/check-template.sh fails when the two drift.

The codes an export throws instead of returning a value JavaScript would have to guess at. The rest of Value.Err cannot be reached from a shipped program: the cost bound rules out outOfFuel, exhaustiveness rules out noMatchingAlternative, and the remaining three are about a program that does not compile.

The signature a consumer reads, in the types the .d.ts declares rather than the subset's own spellings: those are what index.d.ts says and the only ones a caller can act on.

artifacts is the SHA-256 of every other file the package ships, paired with its name. The manifest is what carries the theorems, so a reader who has the manifest and the files can ask whether the two belong together; without it a package that was edited after it was written reads exactly like one that was not. The manifest cannot name its own digest, which is why the file that carries the list is the one file not in it.

The package's own README, which is the page npm shows. A consumer of the package reads this and the .d.ts; neither Lean nor this repository is in front of them, so what the exports are, what they throw and what has been proved about them are all stated here.