pow10
plain-language theorem explainer
The pow10 definition supplies a natural-number power of ten for scaling in decimal string conversions. It is cited by decimal rendering functions in the audit and numeric generator modules. The definition is a direct one-line alias to the built-in Nat.pow operation on 10.
Claim. Define the function that maps a natural number $d$ to $10^d$.
background
The Audit module provides scaffolding for emitting deterministic JSON summaries of unitless invariants from the Recognition framework. This includes helper functions for formatting numeric values into strings for reports. Upstream, the Core.pow lemma establishes closure under exponentiation within the phi-subfield, while the Numeric module duplicates the same power-of-ten helper. The local setting is placeholder surface for M1 audit reports that will later incorporate scale-declared quantities.
proof idea
One-line wrapper that applies the standard Nat.pow function to base 10 and the input exponent.
why it matters
This helper supports the ratToDecimal function used in generating audit JSON reports. It contributes to the deterministic output required by the URCAdapters.Audit module for summarizing proven invariants. In the broader framework it enables consistent decimal representation of quantities derived from the phi-ladder and J-cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.