IndisputableMonolith.URCGenerators.Numeric
URCGenerators.Numeric supplies decimal string renderers for rationals and Recognition Science constants. Audit routines cite these helpers to produce deterministic output of unitless invariants. The module defines several formatting functions and imports only Mathlib.
claimThe primary operation renders a rational number $q = n/m$ to a string with exactly $d$ decimal places.
background
The module provides utilities for numeric string generation within the URCGenerators domain of the Recognition Science framework. Key definitions include conversion of rationals to fixed-decimal strings along with string generators for powers of phi and the inverse fine structure constant. These operate on top of Mathlib and support the emission of scale-declared quantities in audit outputs.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It feeds the Audit scaffolding (M1) in URCAdapters.Audit, which emits a deterministic JSON summary of already-proven unitless invariants. The module enables extension to include numeric values and scale-declared running quantities as described in the downstream doc-comment.
scope and limits
- Does not contain any theorems or proofs.
- Does not import Recognition Science core modules.
- Does not perform symbolic manipulation beyond string formatting.