pith. machine review for the scientific record. sign in
def definition def or abbrev high

bandwidthKernel

show as:
view Lean formalization →

The bandwidth kernel is the ILG time kernel defined as the ratio of demanded recognition rate to available bandwidth. Researchers modeling saturation-driven gravity modifications cite it to locate the Newtonian-to-ILG transition. The definition is a direct division of the two input rates with no further computation.

claimThe ILG time kernel satisfies $w_t(R_d,R_b)=R_d/R_b$, where $R_d$ is the recognition event rate demanded by Newtonian dynamics of mass $M$ at dynamical time $T_{dyn}$ and $R_b$ is the holographic bandwidth limit $A/(4ell_P^2 k_R 8tau_0)$ for boundary area $A$.

background

Recognition bandwidth is the maximum recognition events per unit time allowed by the holographic bound: $R_{max}(A)=A/(4ell_P^2 k_R 8tau_0)$, with each event costing $k_R=ln(phi)$ bits and processing limited to one cycle per $8tau_0$. Demanded rate is the Newtonian requirement $R_{demand}=M/T_{dyn}$ (in units where Planck mass is 1). The module BandwidthSaturation treats ILG gravity as the batching compensation that occurs when demand exceeds this limit, forcing multiple dynamical times into each 8-tick cycle.

proof idea

One-line definition that returns the quotient of demandedRate by availableBandwidth.

why it matters in Recognition Science

This definition supplies the ratio used by the three saturation theorems in the same module (kernel_unity_at_saturation, kernel_gt_one_when_saturated, kernel_lt_one_when_sub). It realizes the ILG time kernel $w_t$ that amplifies gravity below the critical acceleration, directly implementing the eight-tick octave (T7) and the holographic bound that forces modified dynamics. It closes the path from recognition throughput limits to observable ILG parameters C_lag and alpha.

scope and limits

formal statement (Lean)

 151noncomputable def bandwidthKernel (demandedRate availableBandwidth : ℝ) : ℝ :=

proof body

Definition body.

 152  demandedRate / availableBandwidth
 153
 154/-- The bandwidth kernel equals 1 at saturation (transition point). -/

used by (3)

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

depends on (5)

Lean names referenced from this declaration's body.