pith. machine review for the scientific record. sign in
def definition def or abbrev high

main

show as:
view Lean formalization →

The main definition supplies the executable entry point for the URC audit CLI by delegating directly to runAudit, which emits the JSON report of unitless invariants. Auditors and Recognition Science developers cite it to invoke the deterministic summary from the command line. The implementation is a one-line alias with no additional logic.

claimThe primary entry point is the IO action that executes the audit report generator, printing the deterministic JSON summary of proven unitless invariants.

background

The module implements audit scaffolding for milestone M1: it emits a deterministic JSON summary of a minimal set of already-proven, unitless invariants. This surface serves as a placeholder to be extended later with numeric values and scale-declared running quantities. Upstream results include the CPM audit main, which prints a header followed by constants, consistency checks, probability statements and examples, plus the virtues export that outputs the formatted export payload and the sibling runAudit that directly prints the audit JSON report.

proof idea

This is a one-line wrapper that applies runAudit.

why it matters in Recognition Science

This definition supplies the top-level executable for the M1 audit placeholder in the URCAdapters module. It is referenced by downstream results including Jcost calibration, argon electron-affinity zero, SAT completeness lemmas, and several continuum-limit fluid theorems. It fills the audit scaffolding step described in the module documentation and supports verification of framework invariants such as the recognition composition law and phi-ladder structure. It touches the open extension to numeric and scale-declared quantities in later milestones.

scope and limits

Lean usage

import IndisputableMonolith.URCAdapters.Audit #eval main

formal statement (Lean)

 129def main : IO Unit := runAudit

proof body

Definition body.

 130
 131end URCAdapters
 132end IndisputableMonolith
 133
 134def main : IO Unit := IndisputableMonolith.URCAdapters.runAudit

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.