module module high

`IndisputableMonolith.Foundation.SIBridgeClosure`

Defines the SI bridge constants c, ħ, G together with their RS-native counterparts and positivity lemmas. Anyone converting a dimensionless RS identity into laboratory units cites this module. The content is mostly named constants and elementary positivity proofs, not a deep derivation.

claimThe module records the SI values $c_{\mathrm{SI}}$, $\hbar_{\mathrm{SI}}$, $G_{\mathrm{SI}}$ (with $c_{\mathrm{SI}}$ exact by the 2019 SI definition) and the RS-native values $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^{5}/\pi$, each with a positivity certificate.

background

Recognition Science works in dimensionless native units fixed by the forcing chain: $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$. Laboratory predictions require an explicit map from those native values to SI. This module is that map.

It sits on IndisputableMonolith.Constants, which supplies the fundamental RS time quantum $\tau_0=1$ tick and the golden ratio $\varphi$. The SI side uses the post-2019 definitions (exact $c$, fixed $h$ and $e$); the RS side restates the native identities already forced upstream.

Downstream modules treat the pair (native identity, SI lift) as the honest dimensional boundary: pure RS data cannot invent absolute SI scales, so calibration constants must be injected here.

proof idea

This is primarily a definition-and-positivity module. SI constants are introduced as concrete positive reals (with $c$ exact by SI 2019). RS constants are abbreviations of the native formulae $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}$ from the $\varphi$-ladder. Positivity lemmas are short algebraic arguments from $\varphi>1$ and the positivity of the defining expressions; there is no deep forcing proof inside the module itself.

why it matters in Recognition Science

Closes the unit-conversion layer required by every SI-facing gravity track. NativeDimensionalBoundary imports it to state the boundary between forced native identities and SI calibration. HawkingTemperatureSI (Track 3.A), BlackHoleEntropySI (Track 3.B), and BlackHoleEchoesSI (Track 3.D) all import it to lift quarantined $\varphi$-rung algebra into SI units without smuggling absolute scales back into the native theory.

In the primer language this is the place where $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$ meet their laboratory counterparts, keeping the forcing chain (T5–T8) cleanly separated from metrology.

scope and limits

Does not derive SI values of c, ħ, G from first principles; they are calibration inputs.
Does not prove the native identities ħ_RS = φ^{-5} or G_RS = φ^5/π; those live upstream.
Does not perform any black-hole or echo calculation; only supplies constants.
Does not claim the SI bridge is unique beyond the 2019 SI conventions.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Constants.NativeDimensionalBoundary module_import
IndisputableMonolith.Gravity.BlackHoleEchoesSI module_import
IndisputableMonolith.Gravity.BlackHoleEntropySI module_import
IndisputableMonolith.Gravity.HawkingTemperatureSI module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (33)

def c_SI L90
def hbar_SI L94
def G_SI L98
theorem c_SI_pos L100
theorem hbar_SI_pos L101
theorem G_SI_pos L102
def c_RS L107
def hbar_RS L111
def G_RS L115
theorem c_RS_pos L117
theorem phi_pow_5_pos L119
theorem hbar_RS_pos L121
theorem G_RS_pos L125
theorem hbar_RS_mul_G_RS L130
structure SIBridge L142
def c_constraint L155
def hbar_constraint L159
def G_constraint L164
def IsClosedBridge L168
theorem aL_eq_of_c_constraint L174
theorem aM_aT_eq_of_c_hbar L186
theorem aT_aM_eq_of_c_G L209
theorem a_T_sq_eq L238
def tau_Planck L277
theorem tau_Planck_pos L279
theorem a_T_eq L287
theorem tau0_eq_sqrt_pi_planck_time L295
def tau0_predicted_seconds L308
theorem tau0_predicted_seconds_pos L310
theorem si_bridge_closed_under_three_constraints L317
structure SIBridgeClosureCert L335
def siBridgeClosureCert L350
theorem siBridgeClosureCert_inhabited L357