printConstants
printConstants emits a console block listing the verified CPM constants including K_net of 1 for the cone projection and 81/49 for the eight-tick case, C_proj of 2, C_eng of 1, the two coercivity minima, and the RS-derived alpha exponent together with phi. A researcher auditing the Recognition Science constants would invoke the definition inside the CPM CLI to inspect the assigned values and their listed sources. The body consists of a fixed sequence of IO.println statements that render the pre-set text and numbers without runtime calculation.
claimThe definition that prints the CPM constants bundle: $K_ {net}^{cone}=1$, $K_{net}^{eight-tick}=81/49$, $C_{proj}=2$, $C_{eng}=1$, $c_{min}^{cone}=1/2$, $c_{min}^{eight-tick}=49/162$, $alpha=(1-1/phi)/2$, $phi=(1+sqrt{5})/2$, each accompanied by its source note.
background
The CPM.AuditMain module supplies a command-line interface that prints a summary of verified constants, consistency checks, and probability bounds. The printed values are drawn from the Constants structure that packages Knet, Cproj, Ceng and related factors with a non-negativity hypothesis. Upstream results include the definition of tick as the fundamental RS time quantum equal to 1, the structure of nuclear densities in discrete phi-tiers, and the ledger factorization that calibrates the J-cost functional.
proof idea
The definition is realized by a direct sequence of IO.println calls that output a header box, the CPM core constants with sources, the coercivity constants, and the RS-derived constants section. No lemmas are applied and no tactics are used; the body simply emits the hardcoded text and numerical assignments.
why it matters in Recognition Science
The definition is called by the main entry point of the CPM audit CLI to produce the constants display section. It materializes the abstract Constants bundle into concrete printed values that align with the eight-tick octave and the self-similarity constraint on the alpha exponent. The output supports direct inspection of consistency with the phi-ladder and J-uniqueness step of the forcing chain.
scope and limits
- Does not derive any constant value from the forcing axioms at runtime.
- Does not compare the printed numbers against external experimental data.
- Does not accept command-line arguments or user input.
- Does not produce output in any format other than plain console text.
Lean usage
def audit : IO Unit := do printConstantsformal statement (Lean)
31def printConstants : IO Unit := do
proof body
Definition body.
32 IO.println "┌─────────────────────────────────────────────────────────────┐"
33 IO.println "│ Verified Constants │"
34 IO.println "└─────────────────────────────────────────────────────────────┘"
35 IO.println ""
36 IO.println " CPM Core Constants:"
37 IO.println " • K_net (cone) = 1"
38 IO.println " Source: Intrinsic cone projection"
39 IO.println ""
40 IO.println " • K_net (eight-tick) = (9/7)² = 81/49"
41 IO.println " Source: ε=1/8 covering, refined analysis"
42 IO.println ""
43 IO.println " • C_proj = 2"
44 IO.println " Source: Hermitian rank-one bound, J''(1)=1"
45 IO.println ""
46 IO.println " • C_eng = 1"
47 IO.println " Source: Standard energy normalization"
48 IO.println ""
49 IO.println " Coercivity Constants:"
50 IO.println " • c_min (cone) = 1/2"
51 IO.println " Source: 1/(K_net·C_proj·C_eng) = 1/(1·2·1)"
52 IO.println ""
53 IO.println " • c_min (eight-tick) = 49/162"
54 IO.println " Source: 1/(K_net·C_proj·C_eng) = 1/((81/49)·2·1)"
55 IO.println ""
56 IO.println " RS-Derived Constants:"
57 IO.println " • α (ILG exponent) = (1 - 1/φ)/2"
58 IO.println " Source: Self-similarity constraint"
59 IO.println ""
60 IO.println " • φ (golden ratio) = (1 + √5)/2"
61 IO.println " Source: Fixed point of x² = x + 1"
62 IO.println ""
63
64/-- Print consistency checks section. -/