eightTickKernelParams
plain-language theorem explainer
Eight-tick kernel parameters supply the concrete ILG bundle with amplitude fixed at 49/162 and exponent locked to the self-similar value (1 - 1/phi)/2. Researchers modeling scale-dependent gravity kernels cite this when instantiating the w(k,a) function for coercivity or monotonicity arguments. The definition assembles the KernelParams record by direct field assignment from alphaLock together with a single norm_num check.
Claim. The eight-tick ILG kernel parameters are the record with exponent $alpha = (1 - phi^{-1})/2$, amplitude $C = 49/162$, reference timescale $tau_0 > 0$, and the corresponding nonnegativity proofs for $alpha$ and $C$.
background
KernelParams bundles the ILG kernel parameters: exponent alpha, amplitude C, reference time tau0 with its positivity hypothesis, and nonnegativity statements for alpha and C. The module defines the kernel as w(k,a) = 1 + C (a/(k tau0))^alpha, where alpha = (1 - 1/phi)/2 arises from self-similarity and C encodes coercivity slack. Upstream, alphaLock from Constants supplies the locked value (1 - 1/phi)/2 together with its positivity lemma, while tau0 is the fundamental tick duration imported from both Compat.Constants and Constants.
proof idea
The definition constructs the KernelParams record by setting alpha to alphaLock, C to the literal 49/162, tau0 to the input parameter, and tau0_pos to the input hypothesis. Nonnegativity of alpha is obtained from alphaLock_pos via le_of_lt; nonnegativity of C is discharged by the norm_num tactic.
why it matters
This definition provides the eight-tick instantiation of the ILG kernel parameters, which is used directly by the downstream theorem eightTickKernelParams_C that extracts the value of C. It aligns with the eight-tick octave (T7) in the Recognition Science forcing chain and supplies the amplitude needed for kernel-based coercivity calculations in the CPM framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.