Constants Gravitational Constant

The constant's meaning

Newton's gravitational constant G appears in the law of universal gravitation, F = G m₁m₂/r², and sets the strength of gravity in SI units. Its measured value is approximately 6.674 × 10⁻¹¹ m³ kg⁻¹ s⁻², but it is notoriously difficult to measure precisely. The CODATA 2022 recommended value carries a relative uncertainty of about 22 parts per million, which makes G the least precisely known fundamental constant in physics. The standard measurement methods include torsion balances, where the tiny twist of a suspended fiber reveals the gravitational attraction between masses, and more recent techniques that measure the recoil of atoms in an optical lattice.

In Recognition Science, the framework's library of machine-checked formal theorems derives G from two mathematical constants rather than treating it as an empirically fitted parameter. The derivation begins with the framework's core result, a proved cost function J(x) = (x + 1/x)/2 − 1, which forces the golden ratio φ = (1 + √5)/2 as the unique self-similar scaling. From that, the framework derives the Planck constant ℏ = φ⁻⁵ in its native units. With the recognition wavelength λ_rec = 1 and the speed of light c = 1 in those same units, the framework defines the gravitational constant as G = λ_rec² · c³ / (π · ℏ), which simplifies to G = φ⁵ / π.

In Recognition Science, this is a definition, not a measurement. The framework establishes the positive real number G_rs = φ⁵ / π and proves that it is greater than zero. The claim that this number corresponds to the measured gravitational constant is an empirical check, not a theorem within the framework. The numerical agreement is striking: φ⁵ / π ≈ 4.236 / 3.1416 ≈ 1.348, which in the framework's native units is a dimensionless number. To compare with SI, one must convert units; the framework's claim is that the dimensionless value in its unit system matches the measured G when expressed in the same units.

The consequence of this derivation is that the least precisely known constant in SI becomes a derived quantity in the framework, fixed by the golden ratio and π. This does not make G easier to measure in the laboratory; it offers a different theoretical starting point. The framework's library proves the positivity of G_rs and the equality G_rs = φ⁵ / π, but it does not prove that this number equals the measured G. That comparison lives outside the formal theorems, as an empirical matter.

/-- Newton's gravitational constant G in RS-native units.
    G = λ²_rec · c³ / (π · ℏ) with λ_rec = c = 1, ℏ = φ⁻⁵.
    Thus G = φ⁵ / π. -/
noncomputable def G_rs : ℝ := phi ^ 5 / Real.pi

/-- G > 0. -/
theorem G_rs_pos : 0 < G_rs := by
  unfold G_rs
  apply div_pos
  · exact pow_pos phi_pos 5
  · exact Real.pi_pos

/-- **C-002 Resolution**: The gravitational constant is determined by φ and π.

    G = φ⁵/π has no free parameters. It arises from the ledger geometry:
    - λ_rec: the fundamental recognition wavelength (ℓ₀ = 1 in RS units)
    - c: speed of light (1 in RS units)
    - ℏ: Planck constant (E_coh = φ⁻⁵ in RS units)

    The "least precisely known" constant in SI becomes a derived quantity. -/
theorem gravitational_constant_derived :
    0 < G_rs ∧ G_rs = phi ^ 5 / Real.pi :=
  ⟨G_rs_pos, rfl⟩

What this page does not claim

This answer does not claim that the framework proves the numerical value of G matches measurement. This answer does not claim that the framework derives the measured value of G in SI units. This answer does not claim that φ⁵ / π is empirically equal to 6.674 × 10⁻¹¹ m³ kg⁻¹ s⁻².

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/GravitationalConstant.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: