printHeader
plain-language theorem explainer
The printHeader definition outputs the boxed title block for the CPM constants audit report. It is invoked inside the main entry point of the audit CLI to begin display of verified constants and checks. Implementation is a direct do-block of five IO.println calls that emit the ASCII header and a blank line.
Claim. The header-printing action is defined as an IO Unit computation that emits the report title block: a top border, the lines 'CPM Constants Audit Report' and 'Recognition Physics Institute', a bottom border, and a blank line.
background
The module supplies a command-line interface for auditing CPM constants, invoked via lake exe cpm_audit. It prints summaries of verified constants, consistency checks, and probability bounds for coincidental agreement. The upstream Constants structure from LawOfExistence bundles the core values Knet, Cproj, Ceng, Cdisp together with the non-negativity hypothesis 0 ≤ Knet.
proof idea
One-line wrapper implemented as a do-block. It applies IO.println five times in sequence to the fixed header strings, then prints an empty line.
why it matters
The definition is called first by the main entry point of the CPM audit CLI, which then sequences printConstants, printConsistency, printProbability and printExamples. It supports command-line verification of constants derived from the Law of Existence within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.