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

AuditSummary

show as:
view Lean formalization →

AuditSummary aggregates verification metrics for constants derived from Recognition Science invariants in the CPM framework. Researchers auditing phi-ladder derivations and gauge structures would cite this record when reviewing machine-checked consistency reports. The structure is instantiated directly by generateAuditSummary, which pulls counts from verifiedConstants, sets consistencyChecks to 2, and assigns the coincidence bound from cpmCoincidenceBound.

claimA record with five fields: natural number of verified constants, natural number of consistency checks passed, natural number of examples exercised, real-valued coincidence probability bound, and string status indicator.

background

The CPM Constants Audit module supplies machine-checkable verification that constants satisfy properties required by Recognition Science invariants. It includes consistency checks between constant sets and probability bounds for coincidental agreement, with export for audit reports via lake exe cpm_constants_audit. Upstream, RS Native Units fixes base units with c = 1, ħ = φ^{-5}, and the phi-ladder phiRung n = φ^n. NucleosynthesisTiers places nuclear densities on discrete φ-tiers as ρ_nuc ~ φ^{n_nuclear} × ρ_Planck. LedgerFactorization calibrates J on (ℝ₊, ×), while SpectralEmergence forces SU(3) × SU(2) × U(1) gauge content together with exactly three generations and 24 chiral fermions.

proof idea

Structure definition with no proof body. It is populated by the downstream generateAuditSummary, which directly assigns numConstants to verifiedConstants.length, consistencyChecks to 2 for the cone and eight-tick checks, numExamples to exampleCertificates.length, coincidenceProb to cpmCoincidenceBound.probability, and status to the literal string VERIFIED.

why it matters in Recognition Science

This record is the output type of generateAuditSummary and therefore the carrier for the final audit report in the CPM module. It closes the verification loop for constants whose derivations rest on the eight-tick octave (T7), D = 3 spatial dimensions (T8), and the Recognition Composition Law. The structure supports export of results that include the alpha-band coincidence bound and the J-cost calibration, touching the open numerical question of how tightly the observed constants sit inside the predicted interval (137.030, 137.039).

scope and limits

formal statement (Lean)

 169structure AuditSummary where
 170  /-- Total number of verified constants -/
 171  numConstants : ℕ
 172  /-- Number of consistency checks passed -/
 173  consistencyChecks : ℕ
 174  /-- Number of examples exercised in this audit -/
 175  numExamples : ℕ
 176  /-- Coincidence probability bound -/
 177  coincidenceProb : ℝ
 178  /-- Overall status -/
 179  status : String
 180
 181/-- Generate the audit summary. -/

used by (1)

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.