KernelParams
plain-language theorem explainer
KernelParams bundles the ILG exponent alpha, amplitude C and reference timescale tau0 together with their nonnegativity and positivity constraints. Researchers modeling infra-luminous gravity or applying coercivity bounds cite this record when constructing the kernel w(k,a) inside CPMInstance. The declaration is a plain structure definition that directly encodes the parameter fields and axioms with no computational steps.
Claim. A record consisting of a real number $alpha$ (the exponent), a real number $C$ (the amplitude), a positive real number $tau_0$ (the reference timescale), together with proofs that $alpha geq 0$ and $C geq 0$.
background
The ILG kernel takes the explicit form $w(k,a)=1+Ccdot(a/(ktau_0))^alpha$, where $alpha=(1-1/phi)/2$ is fixed by self-similarity and $tau_0$ is the fundamental tick duration. The module imports $tau_0$ and its positivity lemma from Constants (and its Compat wrapper) together with the fine-structure constant definition from Constants.Alpha. Upstream results establish $tau_0$ as the RS-native time unit and supply the positivity fact $0<tau_0$ by direct simplification from the tick definition.
proof idea
The declaration is a structure definition that simply lists the three fields and their three inequality axioms. No lemmas are applied and no tactics are invoked; the construction serves only as a typed container for the kernel parameters.
why it matters
KernelParams supplies the concrete parameters required by defectMass, EnergyControlHypothesis and the coercivity theorems ilg_coercivity and ilg_falsifiable_bound in CPMInstance. It realizes the kernel form stated in the module documentation and thereby connects the ILG model to the Recognition Science constants $tau_0$ and $alpha$. The structure closes the parameter interface needed for falsifiable upper bounds on dark-matter-like effects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.