Pith. sign in
module module moderate

IndisputableMonolith.Physics.SchwarzchildRadiusFromRS

show as:
view Lean formalization →

Defines the Schwarzschild radius in Recognition Science units as $r_s = 2\varphi^5 M/\pi$, recovering the classical $2GM/c^2$ with $c=1$ and the RS value $G=\varphi^5/\pi$. Introduces the RS Planck length, a positive schwarzschild factor, black-hole class bookkeeping, and a certificate bundle. Physicists matching GR horizons to the phi-ladder cite this module. Content is definitional with positivity lemmas.

claimIn RS-native units ($c=1$, $G=\varphi^5/\pi$), the Schwarzschild radius of mass $M$ is $r_s(M)=2\varphi^5 M/\pi$. The module also records the RS Planck length, a positive dimensionless schwarzschild factor, a finite black-hole class enumeration, and a certificate packaging these identities.

background

Recognition Science fixes the dimensionful constants in native units by the forcing chain: $c=1$ and $G=\varphi^5/\pi$ (with $\hbar=\varphi^{-5}$). The classical Schwarzschild radius $r_s=2GM/c^2$ therefore collapses to the pure phi expression $2\varphi^5 M/\pi$.

The module sits in the Physics domain and imports only Mathlib plus IndisputableMonolith.Constants (whose native time quantum is the tick $\tau_0=1$). Sibling definitions introduce a schwarzschild factor, its positivity, an RS Planck length, a black-hole class type with a finite count, and a certificate record that bundles the radius identity for downstream use.

proof idea

Definition module: the radius formula is the direct substitution of the RS values $c=1$ and $G=\varphi^5/\pi$ into $2GM/c^2$. Positivity of the schwarzschild factor is a one-line arithmetic consequence of $\varphi>1$. Remaining declarations are inductive or structure definitions (black-hole classes, certificate) with no deep proof obligations.

why it matters in Recognition Science

Supplies the GR horizon scale in the same units used for the mass ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and the fine-structure band. Links the geometric constant $G=\varphi^5/\pi$ forced by the Recognition framework to the classical black-hole radius, so horizon and Planck-scale comparisons stay inside the phi calculus. No downstream consumers are recorded yet; the certificate is the natural hook for later horizon or information-bound theorems.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)