runAudit
plain-language theorem explainer
runAudit provides the executable entry point that emits a deterministic JSON summary of unitless invariants from the Recognition framework. Developers building CLI tools or test harnesses would cite it to surface audit data. The definition is a one-line IO wrapper that prints the string produced by audit_json_report.
Claim. $runAudit : IO Unit$ is the definition that executes the IO action printing the JSON string assembled by $audit_json_report$ from the lists of audit items and cosmology items.
background
The URCAdapters.Audit module implements audit scaffolding milestone M1: a deterministic JSON summary of already-proven, unitless invariants. This surface is a placeholder that will later incorporate numeric values and scale-declared running quantities. The upstream definition audit_json_report builds the JSON by interleaving AuditItem.toJson calls over auditItems and cosmologyItems into arrays keyed by 'items' and 'cosmology'.
proof idea
The definition is a one-line wrapper that applies IO.println directly to the audit_json_report string.
why it matters
This definition supplies the executable surface for audit scaffolding M1 and feeds the main entry point. It supports verification of core Recognition invariants such as J-uniqueness and the phi-ladder while remaining unitless. It touches the open extension to numeric and scale-dependent quantities in later milestones.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.