Factor lists: the flattened form of a parsed unit

Lean module Esm.Units.Factors, formal/Esm/Units/Factors.lean at 184aa13d35e5
Imports Esm.Units.GrammarLaws, Mathlib.Data.String.Basic, Mathlib.Data.List.Sort, Mathlib.Algebra.BigOperators.Group.Finset.Basic

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:

UExpr.factors flattens: * concatenates, / negates the exponents of its right operand, ^q multiplies every exponent below it by q. The atom 1 and the symbol dimensionless contribute nothing: §4.8.1 lists "", "1" and "dimensionless" as the three spellings of ONE dimensionless entry, so dimensionless is a spelling of the atom 1, not a symbol to be kept.
norm sums the exponents of each symbol, drops the symbols whose sum is zero, and sorts by symbol (String’s order: codepoint order, so uppercase before lowercase).
norm2 splits the list into its numerator side (positive exponents) and its denominator side (the rest) and applies norm to each side separately, so a symbol on both sides stays on both: mol/mol is not cancelled (ruling of 2026-11-12). This is the canonical form; norm is its building block.

This is purely syntactic: no symbol is looked up, so km stays km and ppm stays ppm. Two factor lists denote the same product iff they have the same exponent function expOf ; norm picks the one sorted, zero-free list with a given exponent function (eq_of_expOf_eq ), and norm2 keeps that exponent function too (expOf_norm2).

abbrev Factor source

abbrev Factor

A unit factor: a symbol and its rational exponent.

def UExpr.factors source

def UExpr.factors : UExpr → List Factor

Flatten a parsed unit to its factor list.

def expOf source

def expOf (l : List Factor) (s : String) : ℚ

The total exponent of symbol s in a factor list.

def syms source

def syms (l : List Factor) : List String

The symbols of a factor list.

def norm source

def norm (l : List Factor) : List Factor

Sum exponents per symbol, drop zero sums, sort by symbol.

def Normal source

def Normal (l : List Factor) : Prop

A normalized factor list: strictly increasing symbols, no zero exponent.

The exponent function

`norm`

theorem expOf_of_mem_normal proved source

theorem expOf_of_mem_normal {l : List Factor} (hl : Normal l) {f : Factor} (hf : f ∈ l) :
    expOf l f.1 = f.2

In a normal list, a member’s exponent is its symbol’s total exponent.

theorem eq_of_expOf_eq proved source

theorem eq_of_expOf_eq {l l' : List Factor} (hl : Normal l) (hl' : Normal l')
    (h : expOf l = expOf l') : l = l'

A normal list is determined by its exponent function.

The two-sided normal form

The canonical spelling never cancels a symbol across the fraction bar: mol/mol stays mol/mol. A factor is on the numerator side when its net exponent (after / and negative exponents) is positive, and on the denominator side otherwise; each side is normalized on its own (norm2 ). A zero exponent (m^0) is dropped.

def numFactors source

def numFactors (l : List Factor) : List Factor

The factors with a positive exponent.

def denFactors source

def denFactors (l : List Factor) : List Factor

The factors with a nonpositive exponent.

def norm2 source

def norm2 (l : List Factor) : List Factor

Each side normalized on its own: numerator side, then denominator side.

def Normal2 source

def Normal2 (l : List Factor) : Prop

A two-sided normal list: its positive factors, then its negative ones, each side normal; no zero exponent.

theorem exp_of_mem_norm proved source

theorem exp_of_mem_norm (l : List Factor) {f : Factor} (hf : f ∈ norm l) : f.2 = expOf l f.1

In norm l, each member’s exponent is the total exponent of its symbol in l.

Weighted sums depend only on the exponent function

def wsum source

def wsum (v : String → M) (l : List Factor) : M

Σ q • v s over a factor list.

This module also proves 31 lemmas without doc comments; they are in the source.