dim_G
plain-language theorem explainer
The declaration assigns the dimensional signature [L³ T⁻² M⁻¹] to Newton's gravitational constant. Researchers checking consistency of Planck units or RS-derived constants would reference it when verifying formulas such as ℓ_P = √(ℏ G / c³). It is a direct constructor application of the Dimension structure with fixed integer exponents.
Claim. The gravitational constant carries the dimensional signature $[L^3 T^{-2} M^{-1}]$.
background
The module supplies a dimensional analysis framework built on the three fundamental units τ₀ (fundamental tick), ℓ₀ = c · τ₀ (recognition length), and φ (golden ratio). Each physical quantity is tagged with a Dimension record whose fields L, T, M are integer exponents for length, time, and mass.
The upstream definition of G in Constants states G = λ_rec² c³ / (π ℏ) in RS-native units; the present declaration records the expected exponents that follow from that expression. The sibling Dimension structure is the sole carrier of these exponents and is used throughout the module for consistency checks on Planck length, time, and mass.
proof idea
One-line definition that applies the Dimension constructor to the triple (3, -2, -1).
why it matters
This definition supplies the dimensional anchor required by the module's documentation of Planck-unit formulas and by the first-principles derivation of G in Constants. It directly supports the Recognition Science claim that all constants descend from τ₀, ℓ₀, and φ while preserving the expected [L³ T⁻² M⁻¹] signature. No downstream theorems are recorded yet, but the entry closes the documentation loop for dimensional consistency of the gravitational constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.