pith. machine review for the scientific record. sign in
def definition def or abbrev high

T0

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  39def T0 (r0 a0 : ℝ) : ℝ := 2 * Real.pi * Real.sqrt (r0 / a0)

proof body

Definition body.

  40
  41/-- Core identity: \(a\,T_{\rm dyn}^2 = 4\pi^2 r\). -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.