Ilg Kernel Kernel At Ratio One Alpha Zero

The kernel at its reference scale

The kernel is a mathematical filter that multiplies a signal at each scale, and in the Infra-Luminous Gravity framework it takes the form w(k, a) = 1 + C · (a / (k τ₀))^α. Here k is the wave number, a is the scale factor, τ₀ is a reference time scale, α is an exponent, and C is an amplitude constant. The kernel is defined so that it is always at least 1 and positive for physical parameter ranges, meaning it never suppresses a signal below its background level.

The theorem kernel_at_ratio_one_alpha_zero establishes a specific value. When the exponent α is zero and the ratio a / (k τ₀) equals 1, the kernel equals 1 + C. In plain language, at the reference scale where the scale factor and the product of wave number and reference time are equal, the kernel's value is simply one plus the amplitude constant. This is a recognition event, a discrete record of a scale matching a reference, and the theorem states the kernel's value at that exact point.

The proof is a direct calculation. The kernel's formula contains the term (max 0.01 (a / (k τ₀)))^α. With the ratio set to 1 and α set to 0, this term becomes 1^0, which equals 1, so the kernel reduces to 1 + C. The theorem requires k to be nonzero and the ratio to be exactly 1, and it uses the fact that 0.01 is less than 1 so the maximum function selects 1. This is a clean boundary condition, not a statement about the kernel's behavior away from this point.

In Recognition Science, this theorem is a small but necessary piece of the framework's library of formal theorems. It confirms that the kernel has a well-defined value at its reference scale, which is a prerequisite for the kernel's use in modeling cosmological perturbations. The kernel's monotonicity in the scale factor, proven separately, shows how the filter responds as the universe expands, but this theorem fixes the baseline at the reference point.

What the theorem does not claim is equally important. It does not say that the kernel equals 1 + C at any other scale, nor does it establish the value of C itself. The constant C is set by other definitions: in the Recognition Science parameter set, C equals phi^(-3/2), and in the eight-tick parameter set, C equals 49/162. The theorem only pins down the kernel's value at the single reference point where the ratio is one and the exponent is zero.

/-- Kernel equals 1 + C when the ratio a/(k τ₀) = 1 and α = 0. -/
theorem kernel_at_ratio_one_alpha_zero (P : KernelParams) (hα : P.alpha = 0)
    (k a : ℝ) (hk : k ≠ 0) (hratio : a / (k * P.tau0) = 1) (h1ge : (0.01 : ℝ) ≤ 1) :
    kernel P k a = 1 + P.C := by
  unfold kernel
  have hmax : max 0.01 (a / (k * P.tau0)) = 1 := by
    rw [hratio]
    exact max_eq_right h1ge
  simp [hmax, hα, Real.rpow_zero]

/-- Kernel is at least 1. -/
theorem kernel_ge_one (P : KernelParams) (k a : ℝ) : 1 ≤ kernel P k a := by
  unfold kernel
  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
    apply lt_max_of_lt_left
    norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

/-- Kernel is always positive for valid parameters. -/
theorem kernel_pos (P : KernelParams) (k a : ℝ) : 0 < kernel P k a := by
  unfold kernel
  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
    apply lt_max_of_lt_left
    norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

/-- Kernel equals 1 + C when the ratio a/(k τ₀) = 1 and α = 0. -/
theorem kernel_at_ratio_one_alpha_zero (P : KernelParams) (hα : P.alpha = 0)
    (k a : ℝ) (hk : k ≠ 0) (hratio : a / (k * P.tau0) = 1) (h1ge : (0.01 : ℝ) ≤ 1) :
    kernel P k a = 1 + P.C := by
  unfold kernel
  have hmax : max 0.01 (a / (k * P.tau0)) = 1 := by
    rw [hratio]
    exact max_eq_right h1ge
  simp [hmax, hα, Real.rpow_zero]

/-- The RS-canonical C equals φ^(-3/2). -/
@[simp] theorem rsKernelParams_C (tau0 : ℝ) (h : 0 < tau0) :
    (rsKernelParams tau0 h).C = phi ^ (-(3 : ℝ) / 2) := rfl

What this page does not claim

The theorem does not establish the kernel's value at any scale other than the reference point where the ratio is one. The theorem does not determine the value of the amplitude constant C, which is set by separate definitions. The theorem does not prove that the kernel's reference scale has any physical significance beyond being a mathematical boundary condition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/ILG/Kernel.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: