Ilg Kernel Kernel Dynamical Time Ge One

The time kernel's floor

In the Recognition Science framework, the Infra-Luminous Gravity (ILG) kernel is a mathematical factor that adjusts a background density to account for perturbations. It is written as w(k, a) = 1 + C · (a / (k τ₀))^α, where k is a wave number, a is the scale factor of the universe, τ₀ is a reference time scale, α is an exponent derived from self-similarity, and C is an amplitude constant. The kernel is a positive number that is always at least 1, meaning it never reduces the background value below its base level.

The declaration kernel_dynamical_time_ge_one is a theorem in the framework's machine-checked library of formal theorems. It establishes that a related quantity, called the dynamical time kernel, is also always at least 1. This dynamical time kernel is defined as 1 + C · (max 0.01 (T_dyn / τ₀))^α, where T_dyn represents a dynamical time scale. The theorem proves that for any valid kernel parameters and any real value of T_dyn, the inequality 1 ≤ kernel_dynamical_time P T_dyn holds. This is a formal guarantee that the time-dependent correction never dips below unity, regardless of the time scale input.

The proof of the theorem is direct and relies on the structure of the definition. The term (max 0.01 (T_dyn / τ₀)) is always positive, and raising a positive number to any real power α yields a non-negative result. Since the amplitude constant C is constrained to be non-negative in the KernelParams structure, the product C · (positive)^α is non-negative. Adding this non-negative term to 1 gives a result that is at least 1. The theorem is a direct consequence of these non-negativity properties, which are also used to prove the positivity of the kernel itself.

The theorem is part of a larger formalization that connects the ILG kernel to the framework's core principles. The exponent α is locked to the value (1 - 1/φ) / 2, where φ is the golden ratio, through a self-similarity condition. The amplitude constant C can take different values depending on the parameter set, such as φ^(-3/2) for the Recognition Science parameters or 49/162 for the eight-tick parameters. The theorem kernel_dynamical_time_ge_one holds for any of these parameter choices, making it a general property of the dynamical time kernel within the framework.

What the theorem does not claim is equally important. It does not assert that the dynamical time kernel is bounded above, only that it has a lower bound of 1. It does not claim that the kernel is constant or stationary in time; the theorem kernel_dynamical_time_stationary, which states the kernel equals itself, is a trivial reflexivity statement, not a claim of physical time-independence. The theorem also does not establish any physical law about the actual passage of time or the evolution of the universe; it is a mathematical statement about a defined function, not an empirical observation.

/-- The dynamical-time kernel is at least 1. -/
theorem kernel_dynamical_time_ge_one (P : KernelParams) (T_dyn : ℝ) :
    1 ≤ kernel_dynamical_time P T_dyn := by
  unfold kernel_dynamical_time
  have hmax_pos : 0 < max 0.01 (T_dyn / P.tau0) := by
    apply lt_max_of_lt_left; norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

/-- The dynamical-time ILG kernel: depends only on the local orbital
period `T_dyn`, the recognition tick `τ₀`, the lag amplitude `C`, and the
self-similarity exponent `α`. For a stationary orbit `T_dyn` is constant,
so the enhancement is constant, and the acceleration on an isolated mass
does not grow in time. -/
noncomputable def kernel_dynamical_time (P : KernelParams) (T_dyn : ℝ) : ℝ :=
  1 + P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha

/-- The dynamical-time kernel is positive. -/
theorem kernel_dynamical_time_pos (P : KernelParams) (T_dyn : ℝ) :
    0 < kernel_dynamical_time P T_dyn := by
  unfold kernel_dynamical_time
  have hmax_pos : 0 < max 0.01 (T_dyn / P.tau0) := by
    apply lt_max_of_lt_left; norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

What this page does not claim

The theorem does not state that the dynamical time kernel is bounded above or that it remains constant over time. The theorem does not assert any empirical fact about the actual passage of time or the evolution of the universe. The theorem does not claim that the kernel is physically meaningful for all real values of T_dyn, only that the inequality holds mathematically.

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: