dynamicalTime
plain-language theorem explainer
The declaration defines the standard Keplerian dynamical time T_dyn for mass M at radius r under Newton's constant G_N. Bandwidth saturation analyses in Recognition Science cite it when computing the recognition event rate demanded by Newtonian orbits. The definition is a direct one-line transcription of the orbital period formula with no additional lemmas.
Claim. The dynamical time is $T_ {dyn}(G_N, M, r) = 2π √(r³ / (G_N M))$.
background
In the Bandwidth Saturation module the dynamical time supplies the period that converts Newtonian orbital motion into a recognition event rate. The module shows that when this rate exceeds the holographic bound the recognition operator batches updates, producing the ILG time kernel w_t > 1. Upstream, G_N is the Newtonian constant imported from EntanglementEntropy while M is the recognition structure from the Recognition and Cycle3 modules.
proof idea
One-line definition that directly transcribes the classical Keplerian period formula. No tactics or lemmas are invoked; the body is the explicit expression 2 * Real.pi * Real.sqrt (r ^ 3 / (G_N * M)).
why it matters
This definition supplies the T_dyn argument required by demandedRate, IsSaturated, IsSubSaturated and saturated_or_sub in the RecognitionBandwidth sibling module. It implements the dynamical time that appears in the critical-acceleration equation M / T_dyn = A / (4ℓ_P² · k_R · 8τ₀) and thereby links Newtonian orbits to the eight-tick cycle and holographic bandwidth limit of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.