pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Certificates.UnitsKGate

show as:
view Lean formalization →

The UnitsKGate module supplies floating-point helpers and a certificate for the dimensionless K ratio used in unit conversions. Researchers verifying numerical stability of Recognition Science constants would cite it when checking approximate equalities in KDisplay-derived computations. The module consists entirely of definitions for absolute difference, approximate equality, ratio computation, and UnitsKGateCert.

claimThe module defines $floatAbs(x) := |x|$, $approxEq(a,b,ε)$, $computeRatios$, and the certificate $UnitsKGateCert$.

background

This module sits in the Certificates domain and imports KDisplay, whose doc-comment states it supplies the dimensionless bridge ratio K and display equalities. It introduces helper definitions for floating-point handling to support certification of units. The local setting assumes the Recognition Science framework where K acts as a numerical bridge between unit systems.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the LNALCerts module, whose doc-comment states it bundles VM preservation and token δ-unit bound. It supplies the certificate infrastructure required for invariants in URCGenerators.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)