pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.URCAdapters.Audit

show as:
view Lean formalization →

This module supplies pure formatting and reporting utilities for URC audit outputs, including rational-to-decimal conversion, JSON escaping, and top-level audit report generation. It depends only on the numeric helpers in URCGenerators.Numeric and exposes sibling definitions such as ratToDecimal, auditItems, audit_json_report and runAudit. Working physicists or mathematicians auditing Recognition Science constants would invoke runAudit to obtain machine-readable verification reports. The module consists entirely of definitions with no theorems.

claimThe module defines ratToDecimal : ℚ → ℕ → String that renders q = n/m to a fixed d-decimal string, together with supporting functions pow10, padLeftZeros, escape, quote, boolToJson, alphaInvValue, auditItems, cosmologyItems, audit_json_report and runAudit.

background

The module imports Mathlib for basic types and IndisputableMonolith.URCGenerators.Numeric, whose doc-comment states it supplies 'Minimal numeric helpers for rational formatting (pure, computable)'. It introduces concrete definitions for AuditItem records, decimal padding, rational rendering (explicitly 'Render a rational q = n / m to a fixed d-decimal string'), JSON string escaping, and two top-level report generators: audit_json_report and runAudit. These sit inside the URCAdapters domain whose purpose is to produce machine-readable audit artifacts for Recognition Science constants.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module closes the numeric-to-report pipeline inside URCAdapters, feeding auditItems and cosmologyItems into audit_json_report and runAudit. These artifacts are the final consumable outputs used to verify constants such as alpha inverse value against the Recognition Science phi-ladder and alpha band. No downstream theorems are recorded, indicating the module terminates the adapter layer.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)