pow10
The pow10 definition supplies the integer power of ten required for scaling in rational-to-decimal string conversion. It is cited inside ratToDecimal implementations both in the generators and in the audit adapters. The definition is a direct one-line binding to Nat.pow.
claim$pow10(d) = 10^d$ for $d$ a natural number.
background
The declaration lives in the URCGenerators.Numeric module whose module documentation states it supplies minimal numeric helpers for rational formatting that remain pure and computable. It sits alongside sibling definitions such as ratToDecimal and phiPowValueStr that perform fixed-precision rendering of Recognition Science constants. The upstream dependency on the pow lemma from RecogSpec.Core records that exponentiation preserves the PhiClosed property, although the present definition itself only invokes the standard Nat.pow operation.
proof idea
The definition is a one-line wrapper that directly invokes Nat.pow with base 10 and the supplied exponent.
why it matters in Recognition Science
The definition feeds the ratToDecimal rendering used by both the Audit and Numeric modules when producing decimal strings for constants such as alpha inverse. It therefore supports the numeric layer that underlies the Recognition Science framework's handling of the alpha band and phi-ladder values. No open scaffolding questions are closed by this declaration.
scope and limits
- Does not accept negative exponents.
- Does not return floating-point results.
- Does not perform rounding or truncation beyond integer division.
formal statement (Lean)
10def pow10 (d : Nat) : Nat := Nat.pow 10 d
proof body
Definition body.
11