Constants External Anchors G Si Pos

The gravitational constant's sign

The gravitational constant G is the number that sets the strength of gravity in Newton's law of universal gravitation. In SI units, its accepted value is approximately 6.67430 × 10⁻¹¹, with an uncertainty of about 0.00015 × 10⁻¹¹. A basic fact about this number is that it is positive: gravity attracts, it does not repel. The declaration G_SI_pos is a formal statement of that positivity, checked by a machine.

The declaration belongs to a collection of external calibration data that the Recognition Science framework keeps separate from its own derivations. This collection holds values taken from CODATA 2022, the standard international dataset for physical constants. The declaration G_SI_pos is a lemma, not a new measurement or a definition. It takes the already-defined value of G in SI units and proves, by direct numerical calculation, that this value is greater than zero. The proof is a simple computation, but it is recorded in a machine-checked library of formal theorems, so the fact is not an assumption but a verified result.

What the declaration does not claim is just as important. It does not derive the value of G from any deeper principle. The value 6.67430 × 10⁻¹¹ is entered into the framework as an external anchor, a piece of experimental data imported for comparison. The lemma only certifies that this imported number has the correct sign. It says nothing about why gravity has the strength it does, and it does not connect G to the framework's own derived constants, such as the Planck constant or the speed of light. Those connections, if they exist, are separate claims.

The practical use of G_SI_pos is to keep the framework's mathematics consistent. When other theorems assume that G is positive, they can cite this lemma instead of taking positivity as an unstated premise. It is a small but necessary bookkeeping step, the kind of fact that a large formal library needs to have on file before it can build anything on top of it.

lemma G_SI_pos : 0 < G_SI := by norm_num [G_SI]

/-- **EXTERNAL ANCHOR**: Gravitational constant (CODATA 2022, measured).
    G = 6.67430(15) × 10⁻¹¹ m³/(kg·s²)
    Relative uncertainty: 2.2 × 10⁻⁵ -/
@[simp]
noncomputable def G_SI : ℝ := 6.67430e-11

/-- **EXTERNAL ANCHOR**: Gravitational constant (CODATA 2022, measured).
    G = 6.67430(15) × 10⁻¹¹ m³/(kg·s²)
    Relative uncertainty: 2.2 × 10⁻⁵ -/
@[simp]
noncomputable def G_SI : ℝ := 6.67430e-11

What this page does not claim

The declaration does not prove the value of G from first principles. The declaration does not connect G to the framework's derived constants like hbar or the speed of light. The declaration does not address the sign of gravity in any unit system other than SI.

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