verifiedConstants
verifiedConstants enumerates nine machine-verified CPM constants drawn from Recognition Science invariants, including the net projection factors K_net for cone and eight-tick cases, C_proj equal to 2, the two c_min values, alphaLock, and phi. A researcher auditing the CPM module cites this list to anchor the numerical inputs for consistency checks and coincidence bounds. The definition is a direct list literal of VerifiedConstant records, each carrying its value, derivation source, and exact flag.
claimThe list contains $K_{net}$ (cone) = 1 from intrinsic cone projection, $K_{net}$ (eight-tick) = $(9/7)^2$ from the $1/8$ covering, $C_{proj}$ = 2 from the Hermitian rank-one bound with $J''(1)=1$, $C_{eng}=1$, $C_{disp}=1$, $c_{min}$ (cone) = $1/2$, $c_{min}$ (eight-tick) = $49/162$, the locked fine-structure constant $alpha = (1-1/phi)/2$, and the golden ratio $phi$ as the fixed point of $x^2=x+1$.
background
The VerifiedConstant structure records a name, real value, derivation source string, and exactness boolean for each constant. The module supplies machine-checkable verification of CPM constants derived from Recognition Science invariants, with consistency checks between cone and eight-tick sets plus probability bounds for coincidental agreement. Upstream, alphaLock is the canonical locked fine-structure constant defined by $(1-1/phi)/2$, tick is the fundamental RS time quantum equal to 1, and phi enters as the self-similar fixed point from the forcing chain.
proof idea
The definition is a direct enumeration of nine VerifiedConstant records. Each entry pulls its numerical value from upstream constants such as alphaLock and phi or computes it algebraically from the listed K_net and C factors, with the source field documenting the origin.
why it matters in Recognition Science
This definition supplies the constant list consumed by generateAuditSummary and audit_passes, which establish that the audit status is VERIFIED with positive counts of constants and checks. It anchors the CPM constants to the Recognition Science framework, incorporating the eight-tick octave and phi-ladder relations from the upstream forcing chain T5-T8. The module addresses open questions around numerical coincidence in physical constants by providing explicit provenance for each entry.
scope and limits
- Does not derive the constants from the J-cost functional equation.
- Does not include numerical approximations or error estimates.
- Does not verify consistency with external experimental data.
- Does not cover constants outside the listed CPM set.
Lean usage
theorem auditUsesConstants : verifiedConstants.length > 0 := by simp [generateAuditSummary, verifiedConstants]formal statement (Lean)
45noncomputable def verifiedConstants : List VerifiedConstant := [
proof body
Definition body.
46 { name := "K_net (cone)",
47 value := 1,
48 source := "Intrinsic cone projection",
49 exact := true },
50 { name := "K_net (eight-tick)",
51 value := (9/7)^2,
52 source := "ε=1/8 covering, refined analysis",
53 exact := true },
54 { name := "C_proj",
55 value := 2,
56 source := "Hermitian rank-one bound, J''(1)=1",
57 exact := true },
58 { name := "C_eng",
59 value := 1,
60 source := "Standard energy normalization",
61 exact := true },
62 { name := "C_disp",
63 value := 1,
64 source := "Dispersion bound",
65 exact := true },
66 { name := "c_min (cone)",
67 value := 1/2,
68 source := "1/(K_net·C_proj·C_eng) = 1/(1·2·1)",
69 exact := true },
70 { name := "c_min (eight-tick)",
71 value := 49/162,
72 source := "1/(K_net·C_proj·C_eng) = 1/((81/49)·2·1)",
73 exact := true },
74 { name := "α (ILG exponent)",
75 value := alphaLock,
76 source := "(1 - 1/φ)/2 from self-similarity",
77 exact := true },
78 { name := "φ (golden ratio)",
79 value := phi,
80 source := "Fixed point of x² = x + 1",
81 exact := true }
82]
83
84/-! ## Consistency Verification -/
85
86/-- Verify that c_min is correctly computed from other constants. -/