Gravity Parameterization Bridge Time Power Eq Accel Power At R Eq R0

The exponent bridge

In circular motion, the acceleration of an orbiting body is centripetal acceleration: the inward pull that keeps it on the circle, equal to the square of its speed divided by the radius of the circle. The time for one full revolution is the orbital period. These two quantities are not independent; the faster a body moves at a given radius, the shorter its period and the stronger its acceleration. The framework's machine-checked library of formal theorems records this connection as an exact algebraic identity: acceleration times the square of the period equals four pi squared times the radius.

The declaration time_power_eq_accel_power_at_r_eq_r0 takes this one step further. It compares two ways of writing a scaling law, a rule that says how some quantity grows when another changes. One form uses the ratio of accelerations, raised to a power. The other uses the ratio of periods, raised to a different power. The theorem proves that at the special radius where the orbit's size equals the reference length, these two forms are exactly equivalent: a time exponent of alpha corresponds to an acceleration exponent of alpha over two. The proof is algebraic and complete, with no gaps in the machine-checked derivation.

The identity matters because it lets a researcher translate a model written in one language into the other without losing information. A model that describes gravity through orbital time can be rewritten as a model that describes it through acceleration, and the mapping between their exponents is exact at that one radius. The theorem does not say the two forms are equal at every radius; it pins the equivalence to the single point where the orbit radius equals the reference radius. It also does not claim that any particular physical law, such as Newton's inverse-square law, follows from this identity. The bridge is kinematic, a fact about circular motion and how its quantities relate, not a statement about what forces exist.

/-- **Exponent bridge (time→acceleration form):** at the characteristic radius \(r=r_0\),
\[
\left(\frac{T_{\rm dyn}}{T_0}\right)^{\alpha}
= \left(\frac{a_0}{a}\right)^{\alpha/2}.
\]

This is the exact mapping when the exponent \(\alpha\) is interpreted as the
**time-exponent** (as in a time-kernel), and one rewrites the model in acceleration space.
-/
theorem time_power_eq_accel_power_at_r_eq_r0
    (v r0 a0 α : ℝ) (hv : 0 < v) (hr0 : 0 < r0) (ha0 : 0 < a0) :
    let a := accel v r0
    let T := Tdyn v r0
    let Tref := T0 r0 a0
    (T / Tref) ^ α = (a0 / a) ^ (α / 2) := by
  intro a T Tref
  -- Use the already-proved form with exponent α/2
  have h := accel_power_eq_time_power_at_r_eq_r0 v r0 a0 (α / 2) hv hr0 ha0
  -- h: (a0/a)^(α/2) = (T/Tref)^(2*(α/2)) = (T/Tref)^α
  have : 2 * (α / 2) = α := by ring
  simp only [this] at h
  exact h.symm

/-- Core identity: \(a\,T_{\rm dyn}^2 = 4\pi^2 r\). -/
theorem accel_mul_Tdyn_sq (v r : ℝ) (hv : v ≠ 0) (hr : r ≠ 0) :
    accel v r * (Tdyn v r)^2 = 4 * (Real.pi ^ 2) * r := by
  unfold accel Tdyn
  field_simp [hv, hr]
  ring

What this page does not claim

The identity holds at every radius, not just at the characteristic radius. The theorem derives a specific force law such as Newton's inverse-square law. The framework claims the bridge is a physical discovery rather than a kinematic identity about circular motion.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/ParameterizationBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: