eight_tick_cmin_value
plain-language theorem explainer
The lemma computes the coercivity minimum for the eight-tick model as exactly 49/162. Model builders in Recognition Science who instantiate CPM with eight-tick constants cite this value to confirm the coercivity bound before applying existence theorems. The proof is a direct simplification that unfolds the cmin definition and the model's Knet, Cproj, Ceng fields, then normalizes the resulting rational.
Claim. For the eight-tick model whose constants satisfy $K_{net} = (9/7)^2$, $C_{proj} = 2$, $C_{eng} = 1$, the coercivity constant obeys $c_{min} = 1/(K_{net} C_{proj} C_{eng}) = 49/162$.
background
The module supplies concrete CPM models that satisfy the abstract LawOfExistence axioms. The eightTickModel is defined with Knet = (9/7)^2, Cproj = 2, Ceng = 1 (and Cdisp = 1). The function cmin extracts the coercivity lower bound as the reciprocal of the product Knet · Cproj · Ceng. Upstream, the tick constant supplies the fundamental time quantum whose eight-fold repetition defines the octave period used to calibrate these constants. The module documentation states that all examples include explicit verification that the core theorems apply.
proof idea
One-line wrapper that applies the definitions of cmin and eightTickModel, then invokes norm_num to evaluate the resulting rational arithmetic.
why it matters
This supplies the concrete numerical anchor for the eight-tick model inside the CPM framework, confirming that the coercivity bound matches the value derived from the eight-tick octave (T7) and the phi-ladder constants. It closes the verification loop for the model before downstream applications of the LawOfExistence theorem. No open scaffolding remains for this specific instantiation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.