Constants Dimensions Dim G

The gravitational constant's dimensions

In classical physics, the gravitational constant G appears in Newton's law of universal gravitation, which states that the force between two masses is proportional to the product of the masses divided by the square of the distance between them. The constant of proportionality, G, is not dimensionless; it carries units that make the equation balance. Measuring force in newtons, distance in meters, and mass in kilograms, G has the units of cubic meters per kilogram per second squared. This is the standard dimensional signature of G, written as [L³T⁻²M⁻¹], and it is a fact any physics textbook states.

The Recognition Science framework, a system that derives physical structure from a discrete record of recognition events, models this classical fact in its machine-checked library of formal theorems. The declaration dim_G defines the dimensional signature of the gravitational constant as [L³T⁻²M⁻¹], matching the classical units exactly. Within the framework, this is a definitional choice, not a derived theorem. It establishes the dimensional identity of G so that further calculations, such as the Planck length and time, can be checked for consistency. The framework's documentation demonstrates that the Planck length formula, ℓ_P = √(ℏG/c³), has the correct dimensions of length, and similarly for Planck time and mass.

What dim_G does not do is give a numerical value for G. It says nothing about the strength of gravity, only its units. The declaration also does not derive G from more basic principles; it simply assigns the correct dimensions. This is a foundational bookkeeping step, ensuring that every subsequent formula in the framework respects dimensional consistency. It is the difference between saying gravity has a certain strength and saying gravity is measured in certain units.

In Recognition Science, the fundamental units are the tick τ₀, the recognition length ℓ₀, and the golden ratio φ. The framework's constants module derives values for ℏ, G, and c from these primitives, but the dimensional analysis module, where dim_G lives, is the part that tracks the units. The declaration is a small but necessary piece of the framework's machinery: it labels the gravitational constant so that the framework's equations remain physically meaningful. Without it, the framework could not claim its derived constants correspond to the physical world.

/-- Gravitational constant dimension: [L³T⁻²M⁻¹] -/
def dim_G : Dimension := ⟨3, -2, -1⟩

What this page does not claim

dim_G does not assign a numerical value to the gravitational constant. dim_G does not derive G from more basic principles; it only assigns its dimensions. The dimensional analysis module does not prove the existence of three spatial dimensions.

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/Constants/Dimensions.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: