printHeader
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute or verify any constant values.
- Does not perform consistency or probability checks.
- Does not accept or process command-line arguments.
- Does not produce the full audit output on its own.
Lean usage
def main : IO Unit := do printHeader; printConstants; printConsistency; printProbability; printExamplesformal statement (Lean)
23def printHeader : IO Unit := do
proof body
Definition body.
24 IO.println "╔══════════════════════════════════════════════════════════════╗"
25 IO.println "║ CPM Constants Audit Report ║"
26 IO.println "║ Recognition Physics Institute ║"
27 IO.println "╚══════════════════════════════════════════════════════════════╝"
28 IO.println ""
29
30/-- Print verified constants section. -/