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

IndisputableMonolith.Constants.ILG

show as:
view Lean formalization →

The ILG module defines the lag parameter C_lag and locked alpha value that anchor modified gravity in Recognition Science. These constants are used when recognition throughput exceeds holographic bounds and forces batching over 8-tick cycles. Researchers deriving ILG gravity from recognition events cite the module for its explicit phi-based expressions and positivity lemmas. The module supplies only definitions and elementary bounds.

claim$C_{lag} = phi^{-5}$, $alpha = (1 - phi^{-1})/2$

background

The module lives inside the Constants section and imports the base RS time quantum tau_0 = 1 tick. It supplies the ILG parameters that appear when holographic information bounds limit recognition events per unit time. Recognition cost per bit is k_R = ln(phi) and the eight-tick cadence governs the batching that produces the ILG time kernel w_t > 1.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed directly into Bandwidth Saturation, where Newtonian dynamics exceeding the holographic bound trigger batching that is identified with the ILG kernel, and into Recognition Bandwidth, which connects the holographic bound, k_R = ln(phi), C_lag, alpha, and the 8-tick cadence. The module therefore closes the parameter list required for those unification arguments.

scope and limits

used by (2)

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 (5)