T0
plain-language theorem explainer
T0 defines the characteristic dynamical time from reference length r0 and acceleration a0 as the expression 2π√(r0/a0). Orbital mechanics and RS gravity researchers cite it when converting between acceleration-parameterized and time-parameterized weight forms. The implementation is a direct one-line algebraic definition with no lemmas or tactics required.
Claim. $T_0(r_0, a_0) := 2π √(r_0 / a_0)$ for reference length $r_0$ and reference acceleration $a_0$.
background
The module formalizes exact algebraic identities relating circular-orbit acceleration $a = v^2/r$ and orbital time $T_{dyn} = 2π r/v$ to the common scale $T_0$. Upstream results supply the identity event (J-cost minimum at state 1) and the r0 anchor (φ-exponent offsets per sector from wallpaper and cube geometry). The local setting is the precise bridge between acceleration-parameterized and time-parameterized weight forms, with every identity fully proven.
proof idea
One-line definition that directly encodes the standard orbital period relation $T_0 = 2π √(r_0/a_0)$ using Real.pi and sqrt; no lemmas applied.
why it matters
T0 supplies the base dynamical time scale feeding tau0_pos in Constants and spectral_emergence in SpectralEmergence. It completes the parameterization bridge step that supports the eight-tick octave (T7) and links to the phi-ladder mass formula. The declaration touches the RS-native derivation of ħ and the D = 3 emergence certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.