eightTickModel_pos
plain-language theorem explainer
The lemma confirms strict positivity of the three constants K_net, C_proj and C_eng in the eight-tick CPM model. Researchers constructing discrete evolution models or applying coercivity bounds cite it to license the energy-gap inequality for this parameter choice. The proof reduces the claim by unfolding the model definition and evaluating the explicit arithmetic.
Claim. Let the eight-tick model be defined by the constants $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$. Then $K_{net}>0$, $C_{proj}>0$ and $C_{eng}>0$.
background
The CPM module supplies abstract Model bundles whose Constants record contains the fields Knet, Cproj and Ceng. The cmin definition is the reciprocal of their product, and the upstream coercivity theorem states that the energy gap is at least cmin times defect mass once that product is positive. The eight-tick model is one of the concrete instantiations listed in the module, chosen to align with the fundamental eight-tick period. Upstream doc-comment: “Model using the eight-tick aligned constants (K_net = (9/7)², C_proj = 2). This matches the constants derived in the LaTeX support document.”
proof idea
The proof is a one-line wrapper that applies simp only [eightTickModel] followed by norm_num to evaluate the three inequalities on the explicit numeric values.
why it matters
The result supplies the positivity hypothesis required by energyGap_ge_cmin_mul_defect, allowing the coercivity statement to be instantiated on the eight-tick model as shown in the immediate example. It thereby supports use of the eight-tick octave (period 2^3) inside CPM constructions, consistent with the T7 step of the forcing chain. The declaration closes the verification step for this particular model so that downstream coercivity applications become unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.