demandedRate
plain-language theorem explainer
demandedRate supplies the Newtonian recognition demand rate as the ratio of mass to dynamical time in RS-native units where Planck mass equals one. Researchers modeling ILG modifications via bandwidth saturation cite it when comparing demand against holographic capacity. The definition is a direct quotient with no further reduction.
Claim. The demanded recognition rate is given by $R(M,T)=M/T$, where $M$ is the mass and $T$ the dynamical time.
background
The RecognitionBandwidth module defines recognition bandwidth as the maximum ledger throughput limited by the holographic bound, recognition cost per bit equal to ln(phi), and the eight-tick cadence. Upstream dynamicalTime from BandwidthSaturation computes the Keplerian period as $T=2pi sqrt(r^3/(G M))$. The local setting connects five Recognition Science elements: holographic bound on information, per-bit recognition cost, ILG parameters C_lag=phi^{-5} and alpha, eight-tick cadence, and consciousness boundary cost.
proof idea
The definition is a direct one-line quotient of the two input reals.
why it matters
This definition feeds bandwidthKernel, which forms the ratio of demanded rate to available bandwidth and thereby activates ILG modifications at saturation. It also supports the predicates IsSaturated, IsSubSaturated, and the excluded-middle theorem saturated_or_sub. It fills the gap between Newtonian dynamics and the recognition bandwidth ceiling, relating directly to the eight-tick octave and holographic bound in the unification chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.