pith. sign in
module module high

IndisputableMonolith.CPM.AuditMain

show as:
view Lean formalization →

AuditMain delivers formatting and printing utilities for verified CPM constants drawn from Recognition Science invariants. Researchers auditing constant derivations would cite it to generate readable reports of machine-checked values. The module structures output through helper functions that draw directly from the imported ConstantsAudit without new derivations.

claimDisplay functions for constants satisfying $c=1$, $h = phi^{-5}$, $G = phi^5 / pi$ and the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

background

This module builds on the CPM.ConstantsAudit which supplies machine-checkable verification of CPM constants and their derivations from Recognition Science invariants. It introduces formatting routines to present these values in human-readable form. The theoretical setting is the formal audit of phi-derived constants in RS-native units, with the imported module handling the core property checks.

proof idea

This is a definition module, no proofs. It imports the verification layer from ConstantsAudit and defines local print helpers plus a main entry point that orchestrates formatted output of headers, constants, summaries, and examples.

why it matters in Recognition Science

This module supports the top-level executable audit in the CPM domain, feeding the overall verification of constants against the phi-ladder and T5-T8 forcing chain. It enables practical inspection of results tied to the Recognition Composition Law and alpha band without adding new theorems.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)