Document formats

An ESM document can be written as a Markdown (.md) or Typst (.typ) source file as well as .esm JSON. This chapter specifies those source formats: the notation tables, the LaTeX and Typst math grammars, the value codecs (JSON, the strict YAML subset, Typst dictionaries) and the unit spellings. It is not a description of a Lean model; it is the Lean model, formal/ in the EarthSciAST repository, rendered page by page.

The Esm.Document modules, with Esm.Units.Canonical and Esm.Units.Typeset for the unit spellings, are the authority for these formats: esm-spec.md only points here, and a change to the notation is a change to the modules first. The other Esm.Units modules are included as the supporting model of units and dimensional analysis, which esm-spec.md §4.8 still defines. Every proof is checked by Lean in EarthSciAST’s CI (the formal workflow; formal/README.md explains how to build it locally).

Generated from the Lean source at commit 184aa13d35e5 , without running Lean. Module comments are the prose; each documented declaration shows its statement, its doc comment and a link to its source. 74 modules, 265 documented theorems. Every theorem marked proved has no sorry or admit in its proof, and no file of the Lean package contains either or declares an axiom.

Esm.Document

• Document notation: the Phase 0 tables, as data (Esm.Document.Notation): The signed-off notation for ESM source documents (.md with LaTeX math, .typ with Typst math).
• The canonical number spelling (CONFORMANCE §5.5.3.1) (Esm.Document.Number)
• Lexical pieces shared by the YAML and Typst codecs (Esm.Document.Strings)
• JSON values of an ESM document, in canonical form (Esm.Document.Json): The value type the document codecs (Esm.Document.Yaml, Esm.Document.TypstDict) print and read.
• The strict YAML subset codec (Esm.Document.Yaml): The YAML spelling of a Json value, used for esm:<path> blocks and front matter in Markdown documents.
• The Typst value codec (Esm.Document.TypstDict): A Json value prints as a Typst code-mode value.

Esm.Document.Math

• Math tokens, shared by the two surfaces (Esm.Document.Math.Token): One token type serves LaTeX math and Typst math.
• Pieces the LaTeX and Typst spellings share (Esm.Document.Math.Surface): The two surfaces (Esm.Document.Math.Latex, Esm.Document.Math.Typst) differ in their keyword spellings and lexers, but read numbers alike: a number in its JSON spelling, or a scientific literal mantissa × 10^exponent, where only the spelling of × 10^ and of the exponent’s brackets differs.
• LaTeX math: spelling and lexing of tokens (Esm.Document.Math.Latex): render spells a token list as LaTeX math.
• Typst math: spelling and lexing of tokens (Esm.Document.Math.Typst): render spells a token list as Typst math.
• Expressions as JSON values, and the symbol table (Esm.Document.Math.Expr): The math grammars are stated over the JSON value at an expression position (spec §4.1), not over Esm.Ast, which drops fields.
• How the printer prints each expression (Esm.Document.Math.View): view sorts every well-formed expression into the notation the printer gives it and states the printer’s output for it, so the round-trip proof never unfolds the printer itself.
• The printer: expressions to tokens (Esm.Document.Math.Print): pa c L e prints the expression e for a position that needs precedence level at least L, adding grouping parentheses when e’s own level is lower.
• The parser: tokens to expressions (Esm.Document.Math.Parse): Recursive descent with one function per precedence level (Esm.Document.Math.Print lists the levels), each taking fuel.
• Accepted variants and refused spellings (Esm.Document.Math.Variants): Each accepted variant spelling is a normalization step with one lemma: the variant reads to the same token or the same value as the canonical spelling.
• Hand-written input (Esm.Document.Math.HandWritten): The round-trip theorems cover what the printer writes; these checks cover spellings a person writes and the printer never does: binary minus without spaces, scientific literals spaced any way, \, between names, the italic-d derivative against declared names, field keys with LaTeX-special characters, and JSON strings.
• The LaTeX math round trip, at the string level (Esm.Document.Math.RoundTripLatex)
• The Typst math round trip, at the string level (Esm.Document.Math.RoundTripTypst)
• The token-level round trip (Esm.Document.Math.Main)
• Round trip, case by case: constant arrays (Esm.Document.Math.Arrays): A column for rank 1 and a matrix of at least two columns, LaTeX bmatrix, Typst vec(…) / mat(…), with units after them as for a scalar.
• Round trip of the atoms: numbers and names (Esm.Document.Math.Atoms)
• Round trip, case by case: atoms, prefix operators, functions (Esm.Document.Math.Cases1)
• Round trip, case by case (Esm.Document.Math.Cases2)
• Round trip, case by case: literals, prefix and infix operators (Esm.Document.Math.Cases3)
• Round trip, case by case: the and, or and * chains (Esm.Document.Math.Cases4)
• Round trip, case by case: fractions, powers, cases, initial conditions, indices, calls (Esm.Document.Math.Cases5)
• Round trip, case by case: calls, min/max, initial conditions, indices (Esm.Document.Math.Cases6)
• Round trip, case by case: indices, fractions, powers, cases (Esm.Document.Math.Cases7)
• Round trip, case by case: fractions, powers, cases (Esm.Document.Math.Cases8)
• Round trip, case by case: ifelse as cases (Esm.Document.Math.Cases9)
• Round trip, case by case: derivatives and quantities (Esm.Document.Math.Derivs)
• Round trip, case by case: the escape form (Esm.Document.Math.Escape): Every node has it.
• Round trip, case by case: reductions (faq), rows (Esm.Document.Math.Faq)
• The token-level round trip, by induction over the expression (Esm.Document.Math.Induct)
• Which operator a printer kind stands for (Esm.Document.Math.Kinds)
• Parsing at a level, what may follow, and moving between levels (Esm.Document.Math.Levels): pLvl L parses at precedence level L (1 = an or chain … 9 = postfix, 10 = a primary).
• The LaTeX lexer lemma (Esm.Document.Math.LexLatex): Every list of LaTeX tokens (tokOK) reads back from its rendering.
• The Typst lexer lemma (Esm.Document.Math.LexTypst): Every list of Typst tokens (tokOK) in which each call parenthesis follows a token after which ( is a call parenthesis (CallOK) reads back from its rendering.
• The loops of the level parsers: stopping and running through a chain (Esm.Document.Math.Loops)
• Names read back (Esm.Document.Math.Names): pName_nameToks: the tokens of a name read back to the name, whatever symbol table printed them, before anything that does not continue a name (NameStop: not the scope dot, not an upright name subscript).
• Round trip, case by case: open operators (Esm.Document.Math.OpenOp)
• The token-level round trip: generic pieces (Esm.Document.Math.RoundTrip): PL c e: the printed tokens of e for any level read back to e at that level, before anything that does not continue it, with enough fuel (need).
• Round trip, case by case: expression templates (Esm.Document.Math.Templates): Positional arguments read back through the parameter list of the symbol table, and the parser sorts the bindings; named arguments read back in the printed (sorted) order.
• The LaTeX printer writes only LaTeX tokens (Esm.Document.Math.TokLatex): Every token of a printed well-formed expression is a LaTeX token (tokOK), so the LaTeX lexer lemma applies to the printer’s output.
• The Typst printer writes only Typst tokens, in lexable order (Esm.Document.Math.TokTypst): Every token of a printed well-formed expression is a Typst token (tokOK), every call parenthesis follows a name-like token, and no unit block follows a unit block (Adj), so the Typst lexer lemma applies to the printer’s output.

Esm.Document.Source

• Lines of text (Esm.Document.Source.Lines): Containers are line-oriented: a fenced block ends at the first line that starts with its closing fence.
• Objects in canonical form: sorting entries, and splitting an object between surfaces (Esm.Document.Source.Keys): A canonical ESM document has the keys of every object in strictly increasing order (the sorted-key canonical serialization).
• The document skeleton (Esm.Document.Source.Skeleton): The document layer maps an ESM document (a JSON object in canonical form) to a skeleton: the front matter, the description, the path blocks, and one section per model or reaction system with its description, its declarations, its equations and its own path blocks.
• The document layer round trip (Esm.Document.Source.SkeletonRT): ofDoc_toDoc: a canonical document is rebuilt exactly from its skeleton, for every choice of container predicates Caps.
• The skeleton as a sequence of constructs (Esm.Document.Source.Items): A container spells a skeleton as a sequence of constructs: description blocks, path blocks, component directives, declarations, equations (model, initialization and constraint) and reactions.
• What the skeleton of a canonical document satisfies (Esm.Document.Source.Facts): toDoc_ok: the skeleton of a canonical document only holds what its container can spell (Caps), and only well-formed JSON values; the containers’ round trips assume exactly this.
• Text scanning shared by the containers (Esm.Document.Source.Text): Prefixes, lines, fenced bodies ended by a closing line, and the facts the containers’ round trips use about them.
• Line heads of the YAML spelling (Esm.Document.Source.YamlLines): Facts about which characters start a line of Yaml.encode v, used to show a YAML block can sit inside a Markdown code fence (yaml_heads_tick) or between front-matter --- delimiters (yaml_heads_dash), and that it ends at the start of a line (yaml_ends).
• Reaction sides, shared by the containers (Esm.Document.Source.Reaction): A reaction prints as one line in the chemistry notation of its container (mhchem \ce{…} in Markdown, typsium #ce[…] in Typst), the rate over the arrow (Notation.reactionLatex).
• An equation as math (Esm.Document.Source.Equation): An equation lhs = rhs is printed as the math of the expression ==(lhs, rhs): the = is the comparison’s sign at the loosest comparison level.
• Multi-line equations (accepted input variants) (Esm.Document.Source.MultiLine): The printer writes one equation per display.
• The Markdown container (Esm.Document.Source.Markdown): An ESM document in Markdown is CommonMark with $…$ / $$…$$ math (LaTeX), fenced blocks, YAML front matter and directives.
• Markdown documents: printing, parsing, and the round trip (Esm.Document.Source.MarkdownDoc): printMd spells a canonical ESM document as Markdown, parseMd reads it back, and parseMd_printMd is the round trip.
• The Typst container (Esm.Document.Source.Typst): An ESM document in Typst is markup plus the functions of an esm Typst package.
• Typst documents: printing, parsing, and the round trip (Esm.Document.Source.TypstDoc): printTyp spells a canonical ESM document as Typst, parseTyp reads it back, and parseTyp_printTyp is the round trip, composed exactly as for Markdown (Esm.Document.Source.MarkdownDoc) with the Typst math theorem parseTypst_printTypst.

Esm.Units

• Units: dimensions and exact scales (esm-spec §4.8.1) (Esm.Units.Core): A dimension is a vector of rational exponents over exactly the eight axes m kg s mol K A cd rad (§4.8.1 “The eight canonical dimension axes”).
• The unit registry table (esm-spec §4.8.1) (Esm.Units.Registry): The flat table, exactly as written in §4.8.1: a symbol is in it, spelled exactly, or it does not resolve.
• The unit-string grammar (esm-spec §4.8.2) (Esm.Units.Grammar): A unit string is resolved in four steps, each a function here.
• Whole unit strings, end to end (esm-spec §4.8.2) (Esm.Units.Strings): Facts about resolve on specific strings the spec names, and about the scaling-factor diagnostic text.
• The canonical unit spelling (Esm.Units.Canonical): The canonical form of a document rewrites every units string to ONE spelling built from its parsed unit (esm-spec §4.8.2), so m*h/(mi*s), m h/(mi s) and m·h/(mi·s) canonicalize alike.
• Typeset unit spellings: LaTeX and Typst, with no unit package (Esm.Units.Typeset): A const with units prints in a document as the number, a thin space, then the canonical unit (Esm.Document.Notation).
• Closed examples of the canonical unit spelling (Esm.Units.CanonicalExamples): Tests, not properties: the theorems quantifying over all inputs are in Esm.Units.Canonical and Esm.Units.Typeset.
• Esm.Units.Examples (Esm.Units.Examples)
• Executable read-outs of a resolved unit (Esm.Units.Exec): Rendering for the esm-lean units adapter: the exponent map of a scale in normal form, the exact scale as the p/q*pi^k string the unit-registry golden uses, and a floating-point conversion factor (for the golden’s 1e-12 check only; no verdict reads it, §4.8.1).
• Factor lists: the flattened form of a parsed unit (Esm.Units.Factors): The canonical unit spelling (Esm.Units.Canonical) is computed from a parsed unit tree (UExpr, esm-spec §4.8.2) by flattening it to a list of factors (symbol, rational exponent) and normalizing that list.
• Laws of the unit-string grammar (esm-spec §4.8.2) (Esm.Units.GrammarLaws)
• The identities §4.8.1 states, checked against the table (Esm.Units.Identities): Every entry of table is built from the scale the spec states for it, so each identity below is a genuine check that the stated scales are consistent with the stated relations, exactly (rational arithmetic on exponent maps).
• Algebra of units (esm-spec §4.8.1 “Scales are EXACT”) (Esm.Units.Laws): Units under multiplication form an abelian group up to agreement (equal dimension and equal exact scale), rational powers obey the exponent laws, and the real value of a scale is a positive homomorphism that agreement respects.
• Exact scales of rational numbers (Esm.Units.Rat): Scale.ofRat q is the prime factorization of a positive rational q in the formal-product representation: every prime of the numerator with exponent 1 and every prime of the denominator with exponent -1.