eight_tick_cmin_value
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish that the eight-tick model satisfies every CPM axiom.
- Does not compute cmin for any model other than eightTickModel.
- Does not derive the value 49/162 from first principles; it only evaluates the given constants.
- Does not address positivity or other properties of cmin beyond the equality.
formal statement (Lean)
160lemma eight_tick_cmin_value : cmin eightTickModel.C = 49 / 162 := by
proof body
Term-mode proof.
161 simp only [cmin, eightTickModel]
162 norm_num
163
164/-- Verify positivity of eight-tick constants. -/