rsKernelParams
plain-language theorem explainer
rsKernelParams supplies the canonical ILG kernel parameters with exponent alphaLock = (1 - 1/φ)/2 and amplitude C = φ^{-3/2} for a given reference time τ₀ > 0. Physicists instantiating the kernel w(k,a) = 1 + C (a/(k τ₀))^α for coercivity or scale-factor calculations would cite it directly. The definition is a direct record literal that assigns alpha from alphaLock, C from the golden-ratio power, and passes through the supplied τ₀ and its positivity witness.
Claim. Let τ₀ > 0. The RS-canonical kernel parameters are the record with exponent α = (1 - φ^{-1})/2, amplitude C = φ^{-3/2}, reference timescale τ₀, and the given positivity witness for τ₀ together with the derived nonnegativity statements for α and C.
background
KernelParams is the structure that bundles the ILG kernel parameters: exponent alpha, amplitude C, reference time tau0 with its positivity proof tau0_pos, and nonnegativity witnesses for alpha and C. The module sets the kernel form w(k,a) = 1 + C · (a / (k τ₀))^α where α = (1 - 1/φ)/2 is the self-similarity exponent and C is the amplitude tied to coercivity slack. Upstream, alphaLock is defined as (1 - 1/φ)/2 with positivity proved by linarith after unfolding, while tau0 is the fundamental tick duration with positivity reduced to 0 < 1.
proof idea
The definition constructs the KernelParams record directly. It assigns alpha to alphaLock, C to phi ^ (-3/2), tau0 to the input parameter, tau0_pos to the input h, alpha_nonneg to le_of_lt alphaLock_pos, and C_nonneg to le_of_lt (Real.rpow_pos_of_pos phi_pos _).
why it matters
This definition supplies the concrete RS-derived values that feed the theorems rsKernelParams_alpha, rsKernelParams_C, and ilg_alpha_eq_rs confirming the match to alphaLock and φ^{-3/2}. It anchors the ILG kernel inside the Recognition Science framework by importing the golden-ratio exponent and amplitude that arise from the self-similar fixed point and eight-tick octave. The construction closes the parameter interface for downstream coercivity calculations without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.