module module high

`IndisputableMonolith.CPM.ConstantsAudit`

The CPM.ConstantsAudit module supplies structures and certificates for recording verified constants together with their derivation paths inside the Coercive Projection Method. It defines VerifiedConstant, lists example certificates, and supplies consistency predicates such as cone_cmin_consistent and eight_tick_cmin_consistent. Researchers auditing Recognition Science constants against the phi-ladder would cite these objects when running the AuditMain CLI. The module contains only definitions and example data with no embedded proofs.

claimThe module introduces the structure $VerifiedConstant$ that pairs a constant value with its derivation path, together with the predicate $cone_cmin_consistent$ and the list $exampleCertificates$ of concrete instances.

background

This module sits inside the CPM development and imports the generic Law of Existence, which decomposes into three parts: the projection-defect inequality, coercivity factorization in which energy gaps control defects, and the aggregation principle that lifts local tests to global membership. It also imports the Constants module whose sole content is the RS time quantum $τ_0 = 1$ tick. The sibling definitions therefore operate on top of these two imported foundations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the data structures consumed by AuditMain, the CLI that prints summaries of verified CPM constants and consistency checks. It therefore closes the verification loop for constants that appear in the phi-ladder and the eight-tick octave.

scope and limits

Does not derive any constants from the forcing chain.
Does not execute numerical searches beyond the listed examples.
Does not prove the Law of Existence statements.
Does not interface with external measurement data.

used by (1)

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

IndisputableMonolith.CPM.AuditMain module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.CPM.LawOfExistence module_import

declarations in this module (18)

structure VerifiedConstant L34
def verifiedConstants L45
theorem cone_cmin_consistent L87
theorem eight_tick_cmin_consistent L91
theorem cone_cmin_numerical L97
theorem eight_tick_cmin_numerical L101
structure CoincidenceBound L108
def cpmCoincidenceBound L122
theorem coincidence_negligible L132
structure ExampleCertificate L140
def exampleCertificates L151
theorem all_examples_cproj_two_statement L159
structure AuditSummary L169
def generateAuditSummary L182
theorem audit_passes L191
def constantsToJSON L213
def examplesToJSON L226
def generateJSONReport L231