pith. machine review for the scientific record. sign in
theorem proved term proof high

eightTickKernelParams_C

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 172@[simp] theorem eightTickKernelParams_C (tau0 : ℝ) (h : 0 < tau0) :
 173    (eightTickKernelParams tau0 h).C = 49 / 162 := rfl

proof body

Term-mode proof.

 174
 175/-! ## Dimensional Analysis -/
 176
 177/-- Kernel ratio is scale-invariant: the ratio a/(k τ₀) is dimensionless. -/

depends on (11)

Lean names referenced from this declaration's body.