ratToDecimal
plain-language theorem explainer
This definition supplies a pure function converting a rational n/m into a fixed d-decimal string, including sign handling and zero-denominator NaN. It is invoked by phiPowValueStr and alphaInvValueStr to emit deterministic constant strings for the URC pipeline. The body scales the absolute numerator by 10^d, splits integer and fractional parts, pads the latter, and concatenates the result.
Claim. The function ratToDecimal(n ∈ ℤ, m ∈ ℕ, d ∈ ℕ) returns the decimal string for the rational q = n/m with exactly d digits after the decimal point (or the string NaN if m = 0), prefixed by a minus sign when n < 0.
background
The module provides minimal numeric helpers for rational formatting in pure, computable form. It depends on the local pow10 d (which returns 10^d) and padLeftZeros (which prepends zeros to reach a target length). A parallel implementation exists in URCAdapters.Audit, indicating the helper is duplicated for independent numeric generators.
proof idea
The definition first extracts the sign and absolute value of n. It scales the absolute value by pow10 d, computes the integer part as scaled / scale and the fractional part as scaled % scale, converts the fractional part to a string, pads it to length d via padLeftZeros, and assembles the final string (sign + integer + optional decimal point + padded fraction). The m = 0 case short-circuits to NaN.
why it matters
The definition enables deterministic string emission of Recognition Science constants, directly feeding alphaInvValueStr (which approximates α^{-1} ≈ 4π·11 − (w8·ln φ + δ_κ) inside the interval (137.030, 137.039)) and phiPowValueStr. It supports the computable-constant layer required by the URC generators and closes a numeric-formatting gap in the pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.