demandedRate
Recognition Science defines the demanded recognition event rate for mass M at dynamical time T_dyn as their direct ratio in native units where the Planck mass equals one. Workers deriving the ILG saturation kernel or the Newtonian-to-modified-gravity transition cite this quantity when comparing ledger demand against holographic capacity. The definition is a one-line division that inherits all algebraic properties from the real division operation.
claimThe demanded recognition event rate is the real number $R(M,T)=M/T$, where $T$ is the Keplerian dynamical time supplied by the upstream definition $T=2π√(r³/(G_N M))$.
background
The RecognitionBandwidth module supplies the demand side of the saturation comparison that links Newtonian dynamics to the ILG modification. Recognition bandwidth itself is the holographic ceiling $R_max=A/(4ℓ_P²·lnφ·8τ₀)$, built from the bound on information, the per-bit recognition cost lnφ, and the eight-tick cadence. The upstream dynamicalTime definition supplies the Newtonian period that sets the required ledger-update interval for a given mass and radius.
proof idea
One-line definition that returns the quotient of the two real arguments; no lemmas or tactics are invoked beyond the built-in division on ℝ.
why it matters in Recognition Science
This definition supplies the numerator for the bandwidth kernel w_t = demandedRate / bandwidth that amplifies gravity once demand exceeds holographic capacity. It is the common input to the predicates IsSaturated, IsSubSaturated and the theorem saturated_or_sub that partition systems into Newtonian and ILG regimes. The construction therefore closes the loop from Newtonian acceleration to the long-time modification required by the eight-tick octave and phi-ladder structure.
scope and limits
- Does not restore the Planck-mass prefactor; the formula assumes RS-native units with m_P = 1.
- Does not expose radius or G_N; these quantities are already folded into the dynamicalTime argument.
- Does not compute available bandwidth or the saturation ratio; it only produces the demand side.
- Does not incorporate quantum or holographic corrections to the update rate itself.
Lean usage
def kernelExample (M T A : ℝ) : ℝ := bandwidthKernel (demandedRate M T) (bandwidth A)formal statement (Lean)
154noncomputable def demandedRate (mass dynamicalTime : ℝ) : ℝ :=
proof body
Definition body.
155 mass / dynamicalTime
156