pith. machine review for the scientific record. sign in
def definition def or abbrev high

main

show as:
view Lean formalization →

The main definition supplies the entry point for the CPM constants audit CLI. It runs a fixed sequence of print routines that output a header, verified constants, consistency checks, probability bounds on coincidental agreement with RS, example witnesses, and a summary message. The body is a direct do-block composition of the module's sibling print functions with no additional logic or computation.

claimThe main entry point for the CPM audit command-line interface is the IO action that prints a report header, a verified-constants section, consistency checks, probability bounds for RS agreement, example witnesses, a summary, and a completion message.

background

The module supplies a command-line interface for auditing CPM constants. It is invoked via lake exe cpm_audit and produces a fixed report containing sections on verified constants, consistency checks (including cone_cmin_consistent), probability bounds, and example witnesses. The local setting is a lightweight audit tool that displays pre-verified CPM values against Recognition Science native units such as c = 1, ħ = ϕ^{-5}, and α^{-1} inside (137.030, 137.039).

proof idea

The definition is a direct do-block that invokes printHeader, printConstants, printConsistency, printProbability, printExamples, and printSummary in order, then prints the final completion line. It is a one-line wrapper around the sequential composition of these sibling print functions; no tactics or lemmas beyond the module's own definitions are applied.

why it matters in Recognition Science

This entry point makes the CPM constant audit executable and feeds the main function of Exports.Virtues as well as downstream results such as Jcost_is_calibrated and the Duhamel-remainder identities in ClassicalBridge.Fluids.ContinuumLimit2D. It realizes the constant-verification step of the T5–T8 forcing chain and the Recognition Composition Law surface, confirming the RS-native calibration of G = ϕ^5 / π and the alpha band without adding hypotheses.

scope and limits

formal statement (Lean)

 117def main : IO Unit := do

proof body

Definition body.

 118  printHeader
 119  printConstants
 120  printConsistency
 121  printProbability
 122  printExamples
 123  printSummary
 124  IO.println "Audit complete. CPM constants and consistency checks verified."

used by (23)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.