Foundation Sibridge Closure A T A M Eq Of C G

The calibration ratio

In physics, a unit system is a set of choices: how long is a second, how heavy is a kilogram. The International System (SI) defines the second, the metre, and the kilogram through exact constants, but Newton's gravitational constant G remains a measured quantity. The Recognition Science framework works in its own native units, where the speed of light is set to 1 and other constants take simple forms. To display any framework result in familiar SI units, one must know how the two systems connect.

The declaration aT_aM_eq_of_c_G establishes one piece of that connection. It proves that the ratio of the framework's time unit (one tick in seconds) to its mass unit (one coherence-mass in kilograms) equals G_SI divided by the product of the framework's G value and the cube of the SI speed of light. In symbols, with a_T as seconds per tick and a_M as kilograms per coherence-mass, the theorem states a_T / a_M = G_SI / (G_RS · c_SI³). The proof uses only the constraints that match the framework's dimensionless speed of light and gravitational constant to their SI counterparts. It does not require the Planck constant or any other input.

The result is a structural theorem in the machine-checked library of formal theorems, meaning it is proved from the stated assumptions with no gaps. It is conditional: it takes the framework's native constants as given and shows what the conversion ratio must be. The theorem does not predict the SI value of G; that value comes from CODATA measurement. It only says that once G is measured, the ratio between the framework's time and mass units is uniquely fixed.

What the theorem does not claim is broader than what it claims. It does not say the framework derives G from first principles. It does not say the framework's mass unit equals the Planck mass. The framework's electron mass in coherence-mass units is φ³, but the conversion to kilograms involves a downstream dressing factor, not a direct proportionality to the Planck mass. The theorem also does not establish the full three-unit bridge; it fixes only the ratio a_T / a_M, leaving the length unit and the absolute scales to be determined by the other constraints.

For a reader, the practical meaning is this: the framework's internal units are not arbitrary. Once one dimensional measurement, G, is supplied, the relative size of the framework's time and mass units is forced by the algebra. This is the kind of closure that lets the framework make numerical claims in SI units without hiding free parameters in the conversion.

/-- From c + G constraints, `a_T / a_M = G_SI / (G_RS · c_SI³)`. -/
theorem aT_aM_eq_of_c_G (b : SIBridge)
    (hC_c : c_constraint b) (hC_G : G_constraint b) :
    b.a_T / b.a_M = G_SI / (G_RS * c_SI ^ 3) := by
  have h_aL := aL_eq_of_c_constraint b hC_c
  have hT_ne : b.a_T ≠ 0 := ne_of_gt b.a_T_pos
  have hM_ne : b.a_M ≠ 0 := ne_of_gt b.a_M_pos
  have G_RS_ne : G_RS ≠ 0 := ne_of_gt G_RS_pos
  have c_SI_ne : c_SI ≠ 0 := ne_of_gt c_SI_pos
  have c_SI3_ne : c_SI ^ 3 ≠ 0 := pow_ne_zero _ c_SI_ne
  have h_coeff_ne : G_RS * c_SI ^ 3 ≠ 0 :=
    mul_ne_zero G_RS_ne c_SI3_ne
  unfold G_constraint at hC_G
  rw [h_aL] at hC_G
  -- G_SI = G_RS · ((c_SI · a_T)³ / (a_M · a_T²))
  -- After clearing divisions, polynomial form: G_SI · a_M = G_RS · c³ · a_T
  -- (where the a_T² cancels with one factor of a_T from (c·a_T)³).
  have h_polyform : G_SI * b.a_M = G_RS * c_SI ^ 3 * b.a_T := by
    have := hC_G
    have hT2_ne : b.a_T ^ 2 ≠ 0 := pow_ne_zero _ hT_ne
    field_simp at this
    linear_combination this
  rw [div_eq_div_iff hM_ne h_coeff_ne]
  linear_combination -h_polyform

/-- From c + G constraints, `a_T / a_M = G_SI / (G_RS · c_SI³)`. -/
theorem aT_aM_eq_of_c_G (b : SIBridge)
    (hC_c : c_constraint b) (hC_G : G_constraint b) :
    b.a_T / b.a_M = G_SI / (G_RS * c_SI ^ 3) := by
  have h_aL := aL_eq_of_c_constraint b hC_c
  have hT_ne : b.a_T ≠ 0 := ne_of_gt b.a_T_pos
  have hM_ne : b.a_M ≠ 0 := ne_of_gt b.a_M_pos
  have G_RS_ne : G_RS ≠ 0 := ne_of_gt G_RS_pos
  have c_SI_ne : c_SI ≠ 0 := ne_of_gt c_SI_pos
  have c_SI3_ne : c_SI ^ 3 ≠ 0 := pow_ne_zero _ c_SI_ne
  have h_coeff_ne : G_RS * c_SI ^ 3 ≠ 0 :=
    mul_ne_zero G_RS_ne c_SI3_ne
  unfold G_constraint at hC_G
  rw [h_aL] at hC_G
  -- G_SI = G_RS · ((c_SI · a_T)³ / (a_M · a_T²))
  -- After clearing divisions, polynomial form: G_SI · a_M = G_RS · c³ · a_T
  -- (where the a_T² cancels with one factor of a_T from (c·a_T)³).
  have h_polyform : G_SI * b.a_M = G_RS * c_SI ^ 3 * b.a_T := by
    have := hC_G
    have hT2_ne : b.a_T ^ 2 ≠ 0 := pow_ne_zero _ hT_ne
    field_simp at this
    linear_combination this
  rw [div_eq_div_iff hM_ne h_coeff_ne]
  linear_combination -h_polyform

/-- Newton's gravitational constant in SI (CODATA 2018 recommended value).
This is the SINGLE remaining dimensional measurement after SI 2019. -/
def G_SI : ℝ := 6.67430e-11

What this page does not claim

The framework derives the SI value of Newton's constant from its own principles. The framework's mass unit equals the Planck mass directly. The theorem fixes the absolute scale of the length unit or the absolute scale of the time and mass units separately.

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/Foundation/SIBridgeClosure.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: