ratToDecimal
plain-language theorem explainer
The decimal renderer converts a rational given by integer numerator and natural denominator into a fixed-precision decimal string with d places. It is invoked by the numeric generators to produce strings for the inverse fine-structure constant and phi powers. The body uses integer scaling by ten to the d, integer division for parts, and zero-padding for the fractional string.
Claim. The map sending integers $n$ and natural numbers $m, d$ to the decimal string for the rational $n/m$ truncated to $d$ places after the decimal point (or the string NaN when $m = 0$).
background
The Audit module supplies scaffolding for deterministic JSON reports on unitless invariants from the Recognition framework. This definition belongs to the numeric formatting layer imported from URCGenerators.Numeric. It depends on the power-of-ten function, which raises 10 to a natural exponent, and the zero-padding function, which prepends zeros to a string to reach a target length. The cosmology scale function, returning phi to a natural power, is imported but not used in this definition. The local setting is the M1 milestone placeholder for audit surfaces that will later incorporate scale-declared running quantities.
proof idea
The definition extracts the sign from the numerator and its absolute value as a natural number. When the denominator is zero it returns NaN. Otherwise it multiplies the absolute numerator by ten to the d, divides by the denominator to obtain the scaled integer, splits that into integer and fractional parts via division and modulo, converts the fractional part to a string, pads it with leading zeros to length d, and concatenates sign, integer part, decimal point if needed, and padded fraction.
why it matters
This definition supplies the string formatting required by the alpha inverse and phi power string generators in the numeric module. Those generators feed the audit JSON report that summarizes proven invariants. It supports the deterministic output of RS constants such as alpha inverse near 137.036 and phi powers on the ladder, consistent with the eight-tick octave and phi-ladder mass formulas in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.