Representation-independent numerical automation

numerics rewrites executable numerical expressions through proved semantic rules registered by their concrete families, then discharges routine arithmetic and side conditions. Closed bit-level evaluation is attempted only after semantic simplification. numerics! explicitly requests that concrete phase even for goals with local variables.

The tactic never chooses a runtime backend and does not unfold optimized kernels on symbolic goals. Numerical families keep direct monomorphic executable functions; this module only consumes their proof theorems.

def FloatLib.Numerics.numericsReduce : Lean.ParserDescr

Normalize a concrete numerical goal and discharge closed arithmetic and bit-vector facts.

def FloatLib.Numerics.numerics : Lean.ParserDescr

Expose registered numerical semantics and solve routine arithmetic, range, and closed encoding goals without unfolding executable kernels on symbolic expressions.

def FloatLib.Numerics.numericsBang : Lean.ParserDescr

Force concrete carrier reduction after the ordinary semantic phase.

def FloatLib.Numerics.numericsRefine : Lean.ParserDescr

Construct a proof-indexed numerical view from a runtime code.

The expected type determines the numerical system and semantic value. The proof component is erased, so the resulting runtime data is exactly code.