VerifiedConstant
VerifiedConstant packages a constant's name, real-valued magnitude, derivation provenance, and exactness flag into a single record for CPM constant audits. Physicists verifying Recognition Science derivations would cite this structure when assembling lists of machine-checked constants such as K_net. The declaration is a plain structure definition with four fields and no attached proof obligations.
claimA verified constant is a record $(n, v, s, e)$ where $n$ is a string identifier, $v$ is a real number, $s$ is a string describing the derivation source, and $e$ is a boolean flag indicating whether the value is exact.
background
The CPM Constants Audit module supplies machine-checkable records for constants derived from Recognition Science invariants, including consistency checks and probability bounds for coincidental agreement. VerifiedConstant serves as the basic record type for storing each constant's metadata in this audit infrastructure. Upstream structures such as PhiForcingDerived.of supply the J-cost framework while NucleosynthesisTiers.of provides nuclear density tiers on the phi-ladder; the module also imports LawOfExistence and Constants to ground the derivations.
proof idea
This is a structure definition. It introduces the record type with four fields (name, value, source, exact) and contains no proof body, tactics, or lemma applications.
why it matters in Recognition Science
This structure is used by verifiedConstants to list specific CPM constants such as K_net from cone projection and eight-tick mechanisms. It supports the audit_passes theorem which confirms the audit summary status. In the Recognition Science framework it contributes to verification of constants like alpha inverse in the 137 band and G = phi^5 / pi by providing a uniform format for provenance tracking.
scope and limits
- Does not derive the numerical values of any constants.
- Does not perform consistency checks between constants.
- Does not generate audit reports or JSON outputs.
- Does not reference specific forcing chain steps T0-T8.
formal statement (Lean)
34structure VerifiedConstant where
35 /-- Name of the constant -/
36 name : String
37 /-- Numerical value -/
38 value : ℝ
39 /-- Source of derivation -/
40 source : String
41 /-- Whether the value is exact (vs. approximate) -/
42 exact : Bool
43
44/-- All verified CPM constants. -/