printConstants
plain-language theorem explainer
This definition produces a console report of verified CPM constants, covering net factors for cone and eight-tick projections, coercivity minima, and RS-derived quantities such as the golden ratio. Researchers verifying constants in the Recognition Science model would cite the output for baseline inspection. The code executes a direct sequence of print commands that hardcode the values and their sources without further computation.
Claim. Define an IO action that prints the CPM core constants: $K_{net}$ (cone) = 1 from intrinsic cone projection; $K_{net}$ (eight-tick) = $(9/7)^2 = 81/49$ from covering with parameter 1/8; $C_{proj} = 2$ from Hermitian rank-one bound at second derivative of J at 1; $C_{eng} = 1$ from energy normalization. It continues with coercivity minima $c_{min}$ (cone) = 1/2 and (eight-tick) = 49/162, plus RS-derived values for the ILG exponent $(1 - 1/φ)/2$ from self-similarity and the golden ratio φ = (1 + √5)/2 as fixed point of x² = x + 1.
background
The module supplies a command-line interface for auditing CPM constants and prints summaries of verified values, consistency checks, and probability bounds. Constants are collected in the structure Constants, which bundles Knet (nonnegative), Cproj, Ceng, and Cdisp. The tick is the fundamental RS time quantum, defined as 1 in native units, and the eight-tick octave supplies the basic evolution period. Upstream results place physical quantities on discrete φ-tiers, with nuclear density scaling as φ to the nuclear rung times Planck density.
proof idea
The body is a do-block that issues a fixed sequence of IO.println calls. It opens with a boxed header, then emits the CPM Core Constants section listing Knet, Cproj, and Ceng with sources. It follows with the Coercivity Constants section for the two cmin values, then the RS-Derived Constants section for the ILG exponent and φ. No lemmas or tactics are applied; the routine is pure output.
why it matters
This definition is called by the main entry point of the CPM audit CLI, which also runs the header, consistency, probability, and examples sections. It surfaces constants tied to the eight-tick octave (period 2³) and the golden ratio as the self-similar fixed point from the forcing chain. The listed ILG exponent connects to self-similarity constraints within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.