eightTickModel
plain-language theorem explainer
A concrete instantiation of the abstract CPM model structure uses the eight-tick aligned constants with net stiffness equal to the square of nine sevenths and projection cost 2. Researchers verifying coercivity bounds in the Recognition framework cite this example when confirming that the eight-tick octave yields positive minimum coercivity. The definition is assembled by direct record construction, with all nonnegativity and inequality conditions discharged by numerical normalization.
Claim. The eight-tick model is the structure $M : Model(Unit)$ whose constants record satisfies $K_{net} = (9/7)^2$, $C_{proj} = 2$, $C_{eng} = 1$, $C_{disp} = 1$, with defect mass, orthogonal mass, energy gap, and test functions all constantly equal to 1, and with the projection defect inequality, energy control, and dispersion conditions holding by direct numerical verification.
background
In the CPM setting the Model structure consists of a Constants record (Knet, Cproj, Ceng, Cdisp) together with four functions from the parameter type to the reals that supply defect mass, orthogonal mass, energy gap, and test count. The eight-tick model sets the parameter type to Unit and populates the constants from the RS-native tick, the fundamental time quantum equal to 1. Upstream results supply the tick definition as the base time quantum and the three-dimensional dispersion function that appears in the dispersion field of the record.
proof idea
The definition builds the Model record by direct field assignment, inserting Knet equal to (9/7) squared and the remaining constants to the eight-tick values. Nonnegativity of each constant is discharged by norm_num. The projection defect obligation reduces to the numerical claim 1 ≤ (9/7)^2 * 2, proved by norm_num followed by linarith; energy control and dispersion are immediate norm_num applications.
why it matters
This definition supplies the concrete data consumed by the eight-tick cmin value lemma, which evaluates the coercivity minimum to 49/162, and by the positivity lemma that confirms the three strict inequalities required by cmin positivity. It realizes the eight-tick octave step of the forcing chain, furnishing a working instance against which the Recognition Composition Law and the emergence of three spatial dimensions can be checked. The chosen constants match those derived in the supporting LaTeX document for the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.