dim_G
Newton's gravitational constant G receives the dimensional signature [L³ T^{-2} M^{-1}]. Researchers deriving Planck units or checking consistency in Recognition Science would reference this assignment. The definition directly instantiates the Dimension record with length exponent 3, time exponent -2, and mass exponent -1.
claimThe gravitational constant $G$ carries the dimensional signature $[L^3 T^{-2} M^{-1}]$.
background
The module establishes a dimensional analysis framework for Recognition Science in which every quantity carries a signature [L^a, T^b, M^c]. The Dimension structure records these three integer exponents for length, time, and mass. Fundamental units are the tick τ₀, recognition length ℓ₀ = c τ₀, and golden ratio φ, from which constants including G are derived self-consistently.
proof idea
This definition is a one-line wrapper that applies the Dimension constructor to the exponents 3, -2, -1.
why it matters in Recognition Science
It supplies the dimensional signature required to verify the Planck length √(ℏG/c³), Planck time √(ℏG/c⁵), and Planck mass √(ℏc/G) formulas inside the Recognition Science derivation of G = λ_rec² c³ / (π ℏ). The assignment aligns with the module's goal of obtaining all constants from τ₀, ℓ₀, and φ while respecting D = 3 spatial dimensions.
scope and limits
- Does not derive the numerical value of G.
- Does not verify dimensional consistency of any formula.
- Does not address variable or higher-dimensional signatures.
formal statement (Lean)
62def dim_G : Dimension := ⟨3, -2, -1⟩
proof body
Definition body.
63
64/-! ## Dimensional Consistency (Documentation)
65
66The Planck length formula has correct dimensions:
67 ℓ_P = √(ℏG/c³)
68 [ℏG/c³] = [L²T⁻¹M¹][L³T⁻²M⁻¹]/[L³T⁻³M⁰]
69 = [L⁵T⁻³M⁰]/[L³T⁻³M⁰]
70 = [L²T⁰M⁰]
71 [√(ℏG/c³)] = [L¹] ✓
72
73The Planck time formula has correct dimensions:
74 t_P = √(ℏG/c⁵)
75 [ℏG/c⁵] = [L²T⁻¹M¹][L³T⁻²M⁻¹]/[L⁵T⁻⁵M⁰]
76 = [L⁵T⁻³M⁰]/[L⁵T⁻⁵M⁰]
77 = [L⁰T²M⁰]
78 [√(ℏG/c⁵)] = [T¹] ✓
79
80The Planck mass formula has correct dimensions:
81 m_P = √(ℏc/G)
82 [ℏc/G] = [L²T⁻¹M¹][L¹T⁻¹M⁰]/[L³T⁻²M⁻¹]
83 = [L³T⁻²M¹]/[L³T⁻²M⁻¹]
84 = [L⁰T⁰M²]
85 [√(ℏc/G)] = [M¹] ✓
86
87τ₀ = √(ℏG/(πc³))/c has dimension [T]:
88 [√(ℏG/c³)/c] = [L¹]/[L¹T⁻¹] = [T¹] ✓
89-/
90
91/-! ## Dimensioned Quantities -/
92
93/-- A dimensioned physical quantity with its value and dimensional signature. -/