eightTickModel
plain-language theorem explainer
eightTickModel supplies a concrete Model instance over Unit with K_net = (9/7)^2, C_proj = 2, C_eng = 1, C_disp = 1 and the four functions constantly 1 or 4. Researchers testing coercivity or cmin positivity for eight-tick constants in the CPM setting would cite this example. The definition is assembled by direct record construction with norm_num and a short linarith block discharging the projection inequality.
Claim. The eight-tick model is the Model instance over the unit type whose Constants record has $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$ (all nonnegative) and whose defectMass, orthoMass, energyGap and tests functions are constantly 1, 1, 4 and 1 respectively, with the projection-defect inequality, energy-control and dispersion conditions verified by direct computation.
background
The Model structure from LawOfExistence packages a Constants record (Knet, Cproj, Ceng, Cdisp together with their nonnegativity proofs) and four functions on a parameter type β: defectMass, orthoMass, energyGap and tests. The CPM.Examples module supplies sample instantiations to validate that core theorems such as cmin_pos apply once the positivity hypotheses on the constants are met. Upstream, tick is the fundamental RS time quantum τ₀ = 1; the eight-tick period is the octave of eight such quanta.
proof idea
The definition populates each field of the Model record with explicit rational values. The four nonnegativity obligations inside Constants are discharged by norm_num. projection_defect uses norm_num to obtain the inequality 1 ≤ (9/7)^2 * 2 and then linarith. energy_control and dispersion are each discharged by a single norm_num tactic.
why it matters
This definition supplies the concrete constants for the eight-tick case, which is used to compute the coercivity constant cmin = 49/162 in the downstream lemma eight_tick_cmin_value and to verify positivity in eightTickModel_pos. It instantiates the eight-tick octave (T7) from the forcing chain and provides a working instance for testing the Law of Existence and Recognition Composition Law inside the CPM framework. The constants match those derived in the LaTeX support document.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.