pith. sign in
module module moderate

IndisputableMonolith.CPM.AuditMain

show as:
view Lean formalization →

CPM.AuditMain supplies the main executable and display utilities for auditing constants verified from Recognition Science invariants. It imports the verification logic and defines print helpers for constants, consistency checks, probabilities, examples, and summaries. The module is entirely definitional with no theorems.

claimThe module formats verified constants such as $\hbar = \phi^{-5}$, $G = \phi^5 / \pi$, and $\alpha^{-1} \in (137.030, 137.039)$ that satisfy the Recognition Composition Law and phi-ladder relations.

background

The imported ConstantsAudit module supplies machine-checkable verification of CPM constants and their derivations from Recognition Science invariants. AuditMain extends this with display functions. In the framework, constants arise from the forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

proof idea

This is a definition module, no proofs. It consists of helper definitions for formatting and printing that consume the verified constants from the imported module and culminate in a main entry point.

why it matters in Recognition Science

The module supports practical auditing of constants derived from the single functional equation, feeding the overall CPM verification process. It connects to the T5-T8 chain and the alpha band without introducing new derivations.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)