Pins the axioms every shipped theorem is allowed to rest on #

Pins down that the theorems the artifact is sold on do not depend on sorry: every public theorem of Lean2Js.Example, which lean2js lists in the manifest, plus the seven the guarantee itself rests on: typeSound, fragment_correct, fragment_traps_in, decl_correct, decl_refuses, decl_traps and decl_traps_at_cost.

lean2js refuses a claim whose proof reaches sorryAx, but only when it emits: lake build lets a proof plugged with sorry through with a warning. Pinning the axiom set makes the build fail the moment sorryAx gets mixed in.

The roundtrip is pinned here too, ahead of the manifest carrying it: it is the only thing standing between the trees the proofs are about and the text that ships. So is the small-step machine's agreement with eval. So is the descent Lean2Js.Denote makes from a theorem about an author's function to a claim about the generated module. The certificates the walk assembles are public theorems of Lean2Js.Example, so the sweep at the end of this file is what pins them: there is one per shipped declaration and naming them one by one would drift the moment a declaration is added.

Every public theorem of Lean2Js.Example ships as a claim, and the certificates are among them. The sweep reads the same axioms lean2js reads before it writes, so a proof plugged with sorry fails the build rather than only the emit.