formatConstant
plain-language theorem explainer
The formatConstant definition produces a display string for a CPM constant, indicating whether its value is exact or approximate and citing its source. Developers running the audit CLI would invoke it to build the report output. The implementation is a direct string interpolation that selects the appropriate label based on the exact flag.
Claim. The function formatConstant(name, source, exact) returns the string `` • {name} (exact or approximate) Source: {source}'' where the parenthetical label is chosen according to the boolean exact.
background
The CPM.AuditMain module supplies a command-line interface for auditing CPM constants, invoked via lake exe cpm_audit. It prints a summary of verified constants, consistency checks, and probability bounds. The present definition supplies the per-constant formatting step used inside that report generation.
proof idea
Direct definition that conditionally selects the label string and performs string interpolation; no lemmas or tactics are applied.
why it matters
It supplies the output formatting layer for the CPM audit CLI, which displays verified constants and consistency results derived from the Recognition Science constant predictions. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.