pith. sign in
module module high

IndisputableMonolith.ILG.Reciprocity

show as:
view Lean formalization →

ILG.Reciprocity defines the dimensionless variable X = k τ₀ / a and its reciprocity identities for the Infra-Luminous Gravity kernel. Cosmologists deriving first-order growth corrections cite it when building the prefactor in the GrowthODE module. The module supplies definitions and algebraic identities on top of the imported kernel formalization.

claim\( X = k \tau_0 / a \), with the ILG kernel weight \( w(k,a) = 1 + C (a / (k \tau_0))^\alpha \).

background

The upstream ILG.Kernel module formalizes the weight function as w(k, a) = 1 + C · (a / (k τ₀))^α where k is the wave number. This module introduces the dimensionless variable X = k τ₀ / a, which appears as the reciprocal argument in the kernel term. The theoretical setting is the Infra-Luminous Gravity framework for modified growth in cosmology.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the GrowthODE module, which derives the prefactor for the first-order ILG growth correction in EdS background by plugging D = a(1 + B a^α) into the growth ODE. It supplies the reciprocity structure for the dimensionless variable X required by that derivation.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)