Pith. sign in
module module moderate

IndisputableMonolith.Physics.GeneralRelativityFromRS

show as:
view Lean formalization →

Module that fixes the Einstein coupling κ = 8φ⁵/π in RS-native units and packages a certificate that a finite list of classical GR effects has been checked. Relativity and constants auditors cite the κ definition and its positivity. Mostly definitional: one algebraic constant, a short positivity proof, an effect enum, and a certificate constructor.

claimThe Einstein coupling is $\kappa = 8\varphi^5/\pi > 0$. A certificate records that a fixed finite list of classical general-relativistic effects has been exercised in Recognition Science units ($c=1$, $G$ built from $\varphi$).

background

Recognition Science works in units with $c=1$ and expresses Newton’s $G$ through powers of the golden ratio $\varphi$. The only import beyond Mathlib is the Constants layer, which sets the fundamental tick $\tau_0=1$.

In that system the Einstein equations are written $G_{\mu\nu}=\kappa T_{\mu\nu}$. The module defines the coupling $\kappa$ directly as $8\varphi^5/\pi$ and proves it is positive. It also introduces an inductive type of named classical GR effects, a count of those effects, and a certificate structure that bundles positivity of $\kappa$ with the claim that every listed effect has been tested.

proof idea

Definition module plus one elementary inequality. einsteinKappa is the closed-form $8\varphi^5/\pi$; einsteinKappa_pos follows from $\varphi>0$ and $\pi>0$. GREffect enumerates the classical tests; grEffectCount and all_gr_effects_tested turn the enum into a completeness statement. GeneralRelativityCert / generalRelativityCert package those facts into a single certificate value.

why it matters in Recognition Science

Supplies the RS-native Einstein coupling that any weak-field or continuum limit must match, consistent with the primer constants built from $\varphi$. The certificate is the Physics-domain hook for higher-level claims that “GR is recovered from RS.” No downstream dependents are recorded yet; the module is a leaf audit artifact rather than a step in the T0–T8 forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)