pith. machine review for the scientific record. sign in
structure definition def or abbrev high

KernelParams

show as:
view Lean formalization →

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.

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

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.

scope and limits

formal statement (Lean)

  39structure KernelParams where
  40  /-- Exponent α = (1 - 1/φ) / 2 -/
  41  alpha : ℝ
  42  /-- Amplitude constant C -/
  43  C : ℝ
  44  /-- Reference time scale τ₀ -/
  45  tau0 : ℝ
  46  /-- Positivity of τ₀ -/
  47  tau0_pos : 0 < tau0
  48  /-- Nonnegativity of α -/
  49  alpha_nonneg : 0 ≤ alpha
  50  /-- Nonnegativity of C -/
  51  C_nonneg : 0 ≤ C
  52
  53/-- RS-canonical kernel parameters derived from golden ratio. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (21)

Lean names referenced from this declaration's body.