eightTickModel
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value (9/7)^2 from the J-uniqueness functional equation.
- Does not prove uniqueness of this model among all eight-tick compatible choices.
- Does not address empirical calibration of the defect mass function.
- Does not extend the construction to parameter types other than Unit.
formal statement (Lean)
135noncomputable def eightTickModel : Model Unit := {
proof body
Definition body.
136 C := {
137 Knet := (9/7)^2,
138 Cproj := 2,
139 Ceng := 1,
140 Cdisp := 1,
141 Knet_nonneg := by norm_num,
142 Cproj_nonneg := by norm_num,
143 Ceng_nonneg := by norm_num,
144 Cdisp_nonneg := by norm_num
145 },
146 defectMass := fun _ => 1,
147 orthoMass := fun _ => 1,
148 energyGap := fun _ => 4,
149 tests := fun _ => 1,
150 projection_defect := by
151 intro _
152 -- Need: 1 ≤ (9/7)^2 * 2 * 1
153 have h : (1 : ℝ) ≤ (9/7)^2 * 2 := by norm_num
154 linarith,
155 energy_control := by intro _; norm_num,
156 dispersion := by intro _; norm_num
157}
158
159/-- The eight-tick coercivity constant is 49/162. -/