Foundation Sibridge Closure

The SI bridge

The SI bridge is the conversion table between the internal units of Recognition Science and the everyday units of the International System. The framework's own numbers are pure ratios: the speed of light is set to 1, the reduced Planck constant to the inverse fifth power of the golden ratio, and Newton's gravitational constant to the fifth power of the golden ratio divided by pi. These are not SI values. To display a prediction in seconds or metres, the framework needs three positive conversion factors: one tick in seconds, one voxel in metres, and one coherence-mass in kilograms.

The proof shows that these three factors are uniquely determined once the SI values of c, hbar, and G are supplied. The speed of light and the reduced Planck constant are exact by definition in the modern SI system; the gravitational constant remains a measured quantity. The proof takes these three inputs and shows that the conversion factors must satisfy a specific algebraic relation. The central result is a closed-form expression for the tick duration: the square of the seconds-per-tick factor equals pi times hbar_SI times G_SI divided by c_SI to the fifth power. This is a structural theorem, checked by the machine, with no free parameters left over.

In plain terms, the framework's native time unit is not arbitrary. It is forced to be the square root of pi times the Planck time, where the Planck time is built from the measured SI constants. The same logic fixes the voxel size and the coherence-mass in kilograms. The framework does not predict the SI value of G; it takes that measurement as an anchor and derives everything else from it.

This closure reduces the number of free dimensional parameters in physics. The Standard Model carries more than a dozen free masses and mixing angles expressed in GeV. In this account, those reduce to a single dimensional anchor, the measured G, plus the dimensionless structure that the framework derives. The electron mass, for example, is not predicted to sit at the Planck scale; the framework claims only that its dimensionless ratio in coherence-mass units is the cube of the golden ratio, with a separate aging factor connecting substrate and electroweak scales.

What a reader can now see is the precise boundary of the framework's claim. The conversion algebra is closed and unique. The remaining open item is the cosmic-Z hierarchy factor that relates substrate-frame masses to observed ones, a structural fact shared by all Standard Model masses, not a fitted parameter.

/-- **MASTER STATEMENT**: under the c, ℏ, G calibration constraints, the SI
bridge is uniquely determined and `a_T = √π · τ_Planck`. This closes the
conversion-map problem conditional on the dimensional anchor. -/
theorem si_bridge_closed_under_three_constraints :
    ∀ b : SIBridge, IsClosedBridge b →
      b.a_T = Real.sqrt Real.pi * tau_Planck := tau0_eq_sqrt_pi_planck_time

/-- **MAIN ALGEBRAIC IDENTITY**: under c + ℏ + G constraints,
`a_T² = π · ℏ_SI · G_SI / c_SI⁵`.

Proof: multiply `(a_M · a_T) · (a_T / a_M) = a_T²` using the helper
identities, and use `ℏ_RS · G_RS = 1/π`. -/
theorem a_T_sq_eq (b : SIBridge) (hC : IsClosedBridge b) :
    b.a_T ^ 2 = Real.pi * hbar_SI * G_SI / c_SI ^ 5 := by
  obtain ⟨hC_c, hC_h, hC_G⟩ := hC
  have h_aMaT := aM_aT_eq_of_c_hbar b hC_c hC_h
  have h_aTaM := aT_aM_eq_of_c_G b hC_c hC_G
  have hM_ne : b.a_M ≠ 0 := ne_of_gt b.a_M_pos
  -- (a_M · a_T) · (a_T / a_M) = a_T²
  have h_prod : (b.a_M * b.a_T) * (b.a_T / b.a_M) = b.a_T ^ 2 := by
    rw [show (b.a_M * b.a_T) * (b.a_T / b.a_M)
          = (b.a_M / b.a_M) * (b.a_T * b.a_T) from by ring]
    rw [div_self hM_ne, one_mul, sq]
  -- Substitute the helper identities and simplify using ℏ_RS · G_RS = 1/π
  have h_hG : hbar_RS * G_RS = 1 / Real.pi := hbar_RS_mul_G_RS
  have hbar_RS_ne : hbar_RS ≠ 0 := hbar_RS_pos.ne'
  have G_RS_ne : G_RS ≠ 0 := G_RS_pos.ne'
  have c_SI_ne : c_SI ≠ 0 := c_SI_pos.ne'
  have hpi_ne : Real.pi ≠ 0 := Real.pi_pos.ne'
  have c_SI2_ne : c_SI ^ 2 ≠ 0 := pow_ne_zero _ c_SI_ne
  have c_SI3_ne : c_SI ^ 3 ≠ 0 := pow_ne_zero _ c_SI_ne
  have c_SI5_ne : c_SI ^ 5 ≠ 0 := pow_ne_zero _ c_SI_ne
  -- Compute (ℏ_SI / (ℏ_RS · c²)) · (G_SI / (G_RS · c³)) = π · ℏ_SI · G_SI / c⁵
  have h_target : (hbar_SI / (hbar_RS * c_SI ^ 2)) * (G_SI / (G_RS * c_SI ^ 3))
      = Real.pi * hbar_SI * G_SI / c_SI ^ 5 := by
    -- Combine fractions: numerator product over denominator product.
    have h_combine : (hbar_SI / (hbar_RS * c_SI ^ 2)) * (G_SI / (G_RS * c_SI ^ 3))
        = hbar_SI * G_SI / (hbar_RS * G_RS * c_SI ^ 5) := by
      rw [div_mul_div_comm]
      congr 1
      ring
    rw [h_combine, h_hG]
    -- Goal: ℏ_SI · G_SI / ((1/π) · c⁵) = π · ℏ_SI · G_SI / c⁵
    rw [show (1 / Real.pi) * c_SI ^ 5 = c_SI ^ 5 / Real.pi from by ring]
    rw [div_div_eq_mul_div]
    rw [show hbar_SI * G_SI * Real.pi = Real.pi * hbar_SI * G_SI from by ring]
  rw [← h_prod, h_aMaT, h_aTaM, h_target]

/-- **HEADLINE THEOREM**: τ₀ = √π · τ_Planck under the calibrated bridge. -/
theorem tau0_eq_sqrt_pi_planck_time (b : SIBridge) (hC : IsClosedBridge b) :
    b.a_T = Real.sqrt Real.pi * tau_Planck := by
  rw [a_T_eq b hC]
  unfold tau_Planck
  rw [show Real.pi * hbar_SI * G_SI / c_SI ^ 5 =
      Real.pi * (hbar_SI * G_SI / c_SI ^ 5) from by ring]
  exact Real.sqrt_mul (le_of_lt Real.pi_pos) _

/-- 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

This module does not predict the SI value of the gravitational constant; it uses the CODATA measurement as an input. The framework does not claim the electron mass sits at phi cubed times the Planck mass; the hierarchy factor remains a separate structural fact. The SI bridge closure does not derive the pi that appears in the gravitational constant; it inherits it from the framework's constants package.

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: