padLeftZeros
plain-language theorem explainer
padLeftZeros prepends leading zeros to a string until it reaches a target length. It is invoked inside ratToDecimal for fixed-width decimal output in the URC generators and Audit adapters. The definition computes the required zero count from a direct length comparison and assembles the result with a tail-recursive accumulator.
Claim. For a string $s$ and natural number $n$, padLeftZeros$(s,n)$ returns the string formed by prepending exactly $k$ zeros to $s$, where $k = max(0, n - |s|)$.
background
The module supplies minimal numeric helpers for rational formatting that remain pure and computable. padLeftZeros supports fixed-width string representations required by ratToDecimal when rendering rationals to decimal strings.
proof idea
The definition first evaluates the zero count via a conditional length subtraction. It then applies the recursive mkZeros helper, which matches on the remaining count and either returns the accumulator or prepends a zero character and recurses.
why it matters
It underpins ratToDecimal in both the Numeric module and the Audit adapter, enabling consistent formatting of rational approximations such as phiPowValueStr and alphaInvValueStr. The helper sits in the numeric output layer of the URC generators and does not interact with the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.