eightTickModel_pos
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values of the constants.
- Does not establish positivity for models other than the eight-tick instantiation.
- Does not address continuous or higher-dimensional limits.
- Does not supply quantitative bounds stronger than strict positivity.
Lean usage
Model.energyGap_ge_cmin_mul_defect eightTickModel eightTickModel_pos ()formal statement (Lean)
165lemma eightTickModel_pos :
166 0 < eightTickModel.C.Knet ∧ 0 < eightTickModel.C.Cproj ∧ 0 < eightTickModel.C.Ceng := by
proof body
Tactic-mode proof.
167 simp only [eightTickModel]
168 norm_num
169
170/-- Verify coercivity applies to eight-tick model. -/
171example : eightTickModel.energyGap () ≥ cmin eightTickModel.C * eightTickModel.defectMass () :=
172 Model.energyGap_ge_cmin_mul_defect eightTickModel eightTickModel_pos ()
173
174/-! ## Demonstration: cpmsimp tactic -/
175
176/-- Demonstration that `cpmsimp` normalizes products correctly. -/
177example (a b c d : ℝ) : a * b * c * d = a * (b * c) * d := by cpmsimp
178
179example (a b c : ℝ) : a * b * c = b * a * c := by cpmsimp
180
181end Examples
182end CPM
183end IndisputableMonolith