pith. machine review for the scientific record. sign in
theorem proved term proof high

alpha_is_bandwidth_exponent

show as:
view Lean formalization →

The ILG exponent α equals (1 - φ^{-1})/2 and fixes the power-law index of the bandwidth kernel's scaling with dynamical time under holographic throughput limits. Workers deriving the MOND-like a_sat scale from recognition batching over the eight-tick cycle would cite this equality to lock the kernel form. The proof is a one-line reflexivity that matches the locked constant definition imported from the ILG module.

claimThe locked ILG exponent satisfies $α = (1 - φ^{-1})/2$.

background

The BandwidthSaturation module treats ILG gravity as the consequence of recognition throughput limits: when Newtonian dynamics demand more events per unit time than the holographic bound A/(4ℓ_P² · k_R · 8τ₀) permits, the operator batches gravitational updates, producing the time kernel w_t > 1. The critical acceleration a_sat marks the transition where demanded rate equals available bandwidth, with T_dyn = 2πr/v and gravitational area A = 4π(2GM/a)². Upstream, alpha_locked is defined in IndisputableMonolith.Constants.ILG as (1 - 1/φ)/2 and re-exported in CouplingLockIn and SPARCFalsifier as the fixed value αLock ≈ 0.191 that emerges from the recognition composition law and φ-ladder.

proof idea

The proof is a one-line wrapper that applies reflexivity to the definition of alpha_locked.

why it matters in Recognition Science

This equality anchors the bandwidth exponent inside the Recognition framework's forcing chain (T5 J-uniqueness through T7 eight-tick octave) and supplies the φ-determined index required for the ILG kernel to restore consistency above saturation. It directly supports the module's derivation of a_sat and the claim that ILG parameters C_lag and α are bandwidth-determined. No downstream uses are recorded yet, but the result closes the link between the locked coupling and the holographic saturation condition.

scope and limits

formal statement (Lean)

 190theorem alpha_is_bandwidth_exponent :
 191    alpha_locked = (1 - 1 / phi) / 2 := rfl

proof body

Term-mode proof.

 192
 193end BandwidthSaturation
 194end Unification
 195end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.