pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.ILG.Reciprocity

show as:
view Lean formalization →

The ILG.Reciprocity module defines the dimensionless variable X equal to k tau0 over a and records the associated reciprocity identities. Cosmologists working on first-order corrections to structure growth in modified gravity cite this module to nondimensionalize the ILG kernel. The module consists of a short sequence of definitions followed by direct algebraic identities that follow from the definition of X.

claimThe module centers on the dimensionless variable $X = k τ_0 / a$, where $k$ is the wave number and $τ_0$ a reference time scale, together with reciprocity identities relating quantities evaluated at $X$ and at $1/X$.

background

The Infra-Luminous Gravity framework modifies the growth of density perturbations through a kernel that depends on wave number and scale factor. The upstream Kernel module supplies the explicit form $w(k,a) = 1 + C · (a / (k τ_0))^α$. The Reciprocity module introduces the combination $X = k τ_0 / a$ so that the kernel becomes a function of $X$ alone.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the variable $X$ and reciprocity identities required by the GrowthODE module. That module derives the prefactor for the first-order ILG growth correction in an EdS background by substituting the ansatz $D = a(1 + B a^α)$ into the growth ODE.

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)