printHeader
plain-language theorem explainer
This definition supplies the header-printing routine for the CPM constants audit CLI. It is invoked by the main audit entry point to produce the formatted title block before other report sections. The body consists of sequential IO.println calls that render a boxed header with the report title and institute name.
Claim. Definition of the IO procedure that outputs the formatted header block for the CPM constants audit report, including the title and institute affiliation.
background
The CPM.AuditMain module supplies a command-line interface for auditing CPM constants, invoked via lake exe cpm_audit. Output consists of a summary of verified constants, consistency checks, and probability bounds for coincidental agreement. It depends on the Constants structure from LawOfExistence, an abstract bundle containing Knet, Cproj, Ceng, Cdisp with the property that Knet is nonnegative.
proof idea
One-line wrapper that executes five IO.println statements rendering the boxed header lines followed by a blank line.
why it matters
This routine is invoked by the main entry point of the audit CLI, which sequences it before printing constants, consistency, probability, and examples. It forms part of the tooling to verify constants in the CPM component of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.