Constants Derivation G Relation Satisfied

The gravitational constant check

Newton's gravitational constant G is the number that sets the strength of gravity: the force between two masses is G times the product of the masses divided by the square of the distance between them. In the SI system, the accepted value from CODATA 2018 is G = 6.67430 × 10⁻¹¹ m³/(kg·s²). This is a measured quantity, not a derived one in conventional physics; it has to be put in by hand.

Recognition Science (RS) is a framework that starts from a different premise: that reality keeps a discrete record of recognition events, and that the cost of each recognition is forced by a small set of plain conditions. From that starting point, the framework's library of machine-checked formal theorems derives a chain of results that includes the golden ratio, an eight-tick cycle, and three spatial dimensions. It also derives expressions for physical constants rather than treating them as free parameters.

In that derivation, the framework defines a formula for G, called G_derived, which takes three inputs: a fundamental time unit tau0, the reduced Planck constant hbar, and the speed of light c. The formula is G_derived = π · c⁵ · τ² / hbar. The declaration G_relation_satisfied is a theorem in the framework's library that proves, with no gaps, that when you plug in the framework's own tau0 together with the CODATA values of hbar and c, this formula gives back exactly the CODATA value of G. The proof is a direct algebraic verification; it does not fit any parameter to make the numbers match.

What this establishes is a consistency result. The framework's derivation of tau0, its fundamental time unit, was built so that the relation tau0 = sqrt(hbar·G / (π·c³)) / c holds. The G_relation_satisfied theorem confirms that this construction is self-consistent: the derived G equals the measured G, to the precision of the CODATA inputs. It is a check that the framework's internal definitions agree with an externally measured number, not a new measurement of G itself.

What it does not claim is more important. This theorem does not derive G from first principles in the sense of predicting a value that was not already put in. The CODATA value of G is an input to the framework's definition of tau0; the theorem verifies that the round trip works. It also does not claim that G_derived is the unique formula for G, nor that the framework has explained why gravity has this particular strength. The theorem is a proof of internal consistency, not a derivation of the constant's value from nothing.

/-- **Theorem**: G_derived tau0 hbar_codata c_codata = G_codata -/
theorem G_relation_satisfied :
    G_derived tau0 hbar_codata c_codata = G_codata := by
  unfold G_derived
  rw [tau0_sq_eq]
  have hℏ : hbar_codata ≠ 0 := hbar_codata_ne_zero
  have hc : c_codata ≠ 0 := c_codata_ne_zero
  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
  have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
  field_simp

def G_derived (τ hbar_val c_val : ℝ) : ℝ := Real.pi * c_val ^ 5 * τ ^ 2 / hbar_val

def tau0 : ℝ := sqrt (hbar_codata * G_codata / (Real.pi * c_codata ^ 3)) / c_codata

def G_codata : ℝ := 6.67430e-11

What this page does not claim

This theorem does not derive the numerical value of G from first principles; the CODATA value is an input. This theorem does not prove that G_derived is the only possible formula for the gravitational constant. This theorem does not explain why gravity has the strength it does.

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