printConsistency
The printConsistency definition outputs a formatted section verifying that c_min equals the inverse product of K_net, C_proj and C_eng for both cone and eight-tick constant sets, together with their numerical values 1/2 and 49/162. Researchers running the CPM audit CLI to confirm constant agreement in Recognition Science would invoke this routine. The implementation is a direct sequence of IO.println statements that hard-code the four verified claims.
claimDefinition that prints the consistency section stating $c_ {min} = (K_{net} · C_{proj} · C_{eng})^{-1}$ for cone and eight-tick models, with numerical evaluations $c_{min}=1/2$ and $c_{min}=49/162$.
background
The CPM audit module supplies a command-line interface that prints verified constants, consistency checks and probability bounds. Upstream, c_min is the inverse product of the net kernel, projection bound and energy constant; C_proj is fixed at 2. The cone_cmin_consistent theorem states that cmin of the cone constants equals that product inverse by reflexivity. The eight_tick_cmin_consistent theorem does the same for the eight-tick constants. Separate numerical theorems confirm the concrete fractions 1/2 and 49/162 after simplification with the known equalities for each constant set.
proof idea
The definition executes four IO.println calls that output the section header followed by the four consistency statements. It directly references the upstream results cone_cmin_consistent, eight_tick_cmin_consistent, cone_cmin_numerical and eight_tick_cmin_numerical by printing their verified claims verbatim.
why it matters in Recognition Science
This definition is invoked by the main entry point of the CPM audit CLI, which also prints the header, constants, probability bounds and examples. It supports verification of constants inside the Coercive Projection Model, aligning with Recognition Science's eight-tick octave (period 2^3) and the derivation of c=1. The routine closes the audit loop for coincidental numerical agreement without introducing new hypotheses.
scope and limits
- Does not prove any consistency theorem; only prints statements already established upstream.
- Does not compute or update constant values; output strings are hardcoded.
- Does not handle probability bounds or example output; those reside in sibling definitions.
- Does not accept parameters or perform dynamic checks; fixed CLI formatting only.
Lean usage
printConsistencyformal statement (Lean)
65def printConsistency : IO Unit := do
proof body
Definition body.
66 IO.println "┌─────────────────────────────────────────────────────────────┐"
67 IO.println "│ Consistency Checks │"
68 IO.println "└─────────────────────────────────────────────────────────────┘"
69 IO.println ""
70 IO.println " ✓ cone_cmin_consistent: c_min = (K_net·C_proj·C_eng)⁻¹"
71 IO.println " ✓ eight_tick_cmin_consistent: c_min = (K_net·C_proj·C_eng)⁻¹"
72 IO.println " ✓ cone_cmin_numerical: c_min = 1/2"
73 IO.println " ✓ eight_tick_cmin_numerical: c_min = 49/162"
74 IO.println ""
75
76/-- Print probability bounds section. -/