main
plain-language theorem explainer
The main definition assembles the command-line audit report for CPM constants by sequencing header, constants verification, consistency checks, probability bounds, example witnesses, and summary output. Researchers running lake exe cpm_audit invoke this entry point to inspect Recognition Science constant calibrations. The implementation is a direct do-block that calls the individual print routines in fixed order before emitting the completion string.
Claim. The primary IO action for the constants audit executes in sequence the header print, verified constants print, consistency checks print, probability bounds print, example witness print, summary print, and a final completion message.
background
This module supplies the command-line interface for auditing CPM constants. The module documentation states that the audit prints a summary of verified CPM constants, consistency checks, and probability bounds for coincidental agreement. It depends on the complete predicate from Complexity.SAT.Backprop, which asserts that a BPState has all variables assigned, along with sibling print routines that output fixed sections on cone_cmin_consistent and related checks.
proof idea
The definition builds the IO Unit by a do-block that sequences calls to printHeader, printConstants, printConsistency, printProbability, printExamples, printSummary, and IO.println with the audit completion string. It is a direct composition of the sibling print definitions.
why it matters
This entry point provides the executable interface for the CPM constants audit and is invoked by the main of Exports.Virtues. It supports inspection of constants calibrated against the Recognition Science framework, including those tied to the phi-ladder and RCL surface. It closes the audit loop for downstream results such as Jcost_is_calibrated and various continuum-limit theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.