IndisputableMonolith.URCGenerators.Numeric
URCGenerators.Numeric supplies string formatting utilities that render rationals to fixed decimals and produce canonical string values for phi powers and alpha inverse. These feed the Audit scaffolding by supplying deterministic numeric text for unitless invariants. The module is a pure collection of Mathlib-based definitions with no theorems.
claimFunctions include ratToDecimal rendering rational $q = n/m$ to a $d$-decimal string, pow10, padLeftZeros, phiPowValueStr, and alphaInvValueStr.
background
The module lives in the urcgenerators domain and imports only Mathlib. It defines string utilities whose main object is ratToDecimal, which converts a rational to a fixed-decimal representation. Sibling definitions handle padding, powers of ten, and formatted strings for the constants phi and alpha inverse that appear in Recognition Science invariants.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
Supplies the numeric string generators required by the Audit scaffolding (M1) that emits deterministic JSON summaries of already-proven unitless invariants; the Audit placeholder will later incorporate scale-declared running quantities.
scope and limits
- Does not contain theorems or proofs.
- Does not import core Recognition Science modules.
- Does not derive physical constants or mass ladders.
- Provides only string formatting helpers.