pith. sign in
module module high

IndisputableMonolith.CPM.ConstantsAudit

show as:
view Lean formalization →

This module supplies data structures and consistency checks for verified constants in the Coercive Projection Method, drawing on the Law of Existence and RS time quantum. Researchers auditing CPM constants against Recognition Science derivations would cite it for cone and eight-tick model checks. It organizes lists of constants, numerical bounds, and example certificates as a definition module with no proofs.

claimThe module defines a structure recording a constant value together with its derivation path, plus lists of verified constants, consistency statements for minimum values in cone and eight-tick models, numerical checks, coincidence bounds, and example certificates.

background

The module operates in the CPM domain of Recognition Science. It imports the Law of Existence module, which formalizes the generic A/B/C structure: Projection-Defect inequality, Coercivity factorization where energy gap controls defect, and Aggregation principle where local tests imply membership. The Constants module supplies the fundamental RS time quantum τ₀ = 1 tick. Sibling definitions introduce the structure for recording verified constants with derivation, lists of such constants, consistency statements, numerical checks, coincidence bounds, and example certificates.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the data structures and checks consumed by the AuditMain module, which provides the command-line interface for auditing CPM constants. It supports verification of constants against the Law of Existence in the CPM framework, contributing to the overall audit of RS-derived constants.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)