padLeftZeros
plain-language theorem explainer
padLeftZeros prepends leading zeros to a string until it meets a target length, enabling fixed-width formatting for numeric audit outputs. It is referenced by decimal rendering routines inside the URCAdapters module. The body computes the zero deficit from string length and target, then builds the prefix via a tail-recursive accumulator that prepends characters.
Claim. For string $s$ and natural number $n$, padLeftZeros$(s,n)$ returns the concatenation of $k$ zeros followed by $s$, where $k = max(0, n - |s|)$.
background
The Audit module supplies M1 scaffolding that emits deterministic JSON summaries of already-proven unitless invariants from the Recognition Science framework. Its helper definitions ensure consistent string output for later numeric and scale-declared quantities. The padLeftZeros definition mirrors an identical implementation in URCGenerators.Numeric and sits alongside geometry deficit functions that compute $2π - Σθ$ at hinges, though the string version uses only local length arithmetic.
proof idea
The definition first binds a local deficit to zero when $s.length ≥ len$, otherwise to the positive difference. It then invokes a recursive mkZeros that matches on the remaining count: base case returns the accumulator, successor case prepends one zero and recurses.
why it matters
The definition is called by ratToDecimal to produce fixed-decimal strings inside audit JSON reports. It therefore supports the M1 placeholder surface that will later incorporate running quantities and constants such as $α^{-1}$ inside (137.030, 137.039). The utility closes a formatting gap between generators and adapters while the framework remains at the scaffolding stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.