eightTickKernelParams_C
plain-language theorem explainer
The amplitude constant C in the eight-tick ILG kernel parameters equals 49/162 for any positive reference timescale. Cosmologists and ILG modelers would cite this to fix the kernel amplitude in scale-invariant expressions. The proof is a direct reflexivity on the parameter record definition.
Claim. For the eight-tick kernel parameters with reference timescale $τ_0 > 0$, the amplitude constant satisfies $C = 49/162$.
background
The ILG kernel is defined as $w(k,a) = 1 + C (a/(k τ_0))^α$ with exponent $α = (1 - 1/φ)/2$ derived from self-similarity. Here τ_0 denotes the fundamental tick duration, a positive real that sets the reference time scale in RS-native units. The eight-tick variant specializes this kernel to the period-8 octave structure. Upstream results supply τ_0 as the tick duration from Constants and the scale factor from LargeScaleStructureFromRS.
proof idea
This is a one-line wrapper that applies reflexivity to the definition of the eight-tick kernel parameters record, which directly sets the C field to 49/162.
why it matters
This result pins the amplitude in the ILG kernel, supporting the kernel positivity, monotonicity, and reduction-to-unity properties listed in the module. It connects to the eight-tick octave (T7) in the forcing chain and supplies a concrete constant for coercivity slack in CPM derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.