pith. the verified trust layer for science. sign in
module module high

IndisputableMonolith.URCGenerators.Numeric

show as:
view Lean formalization →

URCGenerators.Numeric supplies string rendering utilities for rationals, phi-powered values, and the inverse fine-structure constant in Recognition Science units. Researchers auditing unitless invariants cite these helpers for deterministic decimal output in reports. The module defines conversion routines such as ratToDecimal for fixed-precision rendering of q = n/m together with padding and power-string generators. It contains only definitions and no theorems.

claimThe principal object renders a rational $q = n/m$ to a fixed $d$-decimal string via ratToDecimal$(q,d)$. Companion generators produce string forms of phi-power values and of $alpha^{-1}$ in the interval (137.030, 137.039).

background

The module sits inside the URCGenerators domain of Recognition Science and supplies numeric formatting tools that operate on the phi-ladder and on the alpha band. It introduces ratToDecimal for converting a rational to a fixed-decimal string, together with pow10, padLeftZeros, phiPowValueStr, and alphaInvValueStr. These utilities rest on the same phi and alpha conventions used throughout the framework (phi as self-similar fixed point, alpha inverse inside the narrow band).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Audit scaffolding (M1) in URCAdapters.Audit, which emits a deterministic JSON summary of already-proven unitless invariants. It supplies the numeric string values required for that placeholder surface and will be extended when scale-declared running quantities are added.

scope and limits

used by (1)

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

declarations in this module (5)