IndisputableMonolith.Foundation.SIBridgeClosure
Records the SI laboratory values of c, ħ, and G alongside the RS-native values c = 1, ħ = φ^{-5}, G = φ^5/π, with elementary positivity. Gravity SI-lift modules and the native dimensional-boundary layer import it for honest unit conversion. Structure is definitions plus short positivity lemmas, not a deep theorem.
claimBridge module fixing SI constants $c_{\mathrm{SI}}$, $\hbar_{\mathrm{SI}}$, $G_{\mathrm{SI}}$ (positive; $c$ exact since SI 2019) and RS-native constants $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^{5}/\pi$ (positive), so SI-lift theorems can convert dimensionless RS identities into laboratory units.
background
Recognition Science forces dimensionless native identities from the T0–T8 chain and the Recognition Composition Law. In RS-native units one has $c=1$, $\hbar=\varphi^{-5}$, and $G=\varphi^{5}/\pi$. Absolute SI magnitudes are calibration data: they cannot be read off from pure dimensionless structure alone.
The imported Constants layer supplies the RS time quantum $\tau_0=1$ tick and $\varphi$. This module is the thin naming layer that places the three SI constants next to their RS-native counterparts so downstream SI-lift proofs can cite both sides without smuggling absolute scales into the foundation.
Sibling declarations cover $c_{\mathrm{SI}}$, $\hbar_{\mathrm{SI}}$, $G_{\mathrm{SI}}$ and $c_{\mathrm{RS}}$, $\hbar_{\mathrm{RS}}$, $G_{\mathrm{RS}}$, each with a positivity lemma (including $\varphi^5>0$).
proof idea
Definition-and-positivity module, not a deep argument. It binds the three SI constants (with $c$ marked exact since the 2019 SI redefinition), binds the three RS-native constants to the primer identities $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^{5}/\pi$, and discharges elementary positivity goals from $\varphi>1$ and field arithmetic. No forcing-chain or RCL reasoning lives here.
why it matters in Recognition Science
Parent consumers are the SI gravity lifts and the dimensional-boundary record. NativeDimensionalBoundary uses it to state the honest split: RS can force native identities such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but cannot output absolute SI values from dimensionless data alone.
HawkingTemperatureSI (Track 3.A), BlackHoleEntropySI (Track 3.B), and BlackHoleEchoesSI (Track 3.D) import the bridge to convert quarantined $\varphi$-rung and black-hole algebra into SI units as structural theorems, without reopening native forcing or claiming SI derivation of $c$, $\hbar$, $G$.
scope and limits
- Does not derive SI values of c, ħ, or G from RS axioms.
- Does not prove the native identities ħ = φ^{-5} or G = φ^5/π (those are upstream).
- Does not convert concrete observables; only names the constant bridge.
- Does not calibrate α, masses, or the φ-ladder yardstick.
- Does not claim SI magnitudes are forced by the T0–T8 chain.
used by (4)
depends on (1)
declarations in this module (33)
-
def
c_SI -
def
hbar_SI -
def
G_SI -
theorem
c_SI_pos -
theorem
hbar_SI_pos -
theorem
G_SI_pos -
def
c_RS -
def
hbar_RS -
def
G_RS -
theorem
c_RS_pos -
theorem
phi_pow_5_pos -
theorem
hbar_RS_pos -
theorem
G_RS_pos -
theorem
hbar_RS_mul_G_RS -
structure
SIBridge -
def
c_constraint -
def
hbar_constraint -
def
G_constraint -
def
IsClosedBridge -
theorem
aL_eq_of_c_constraint -
theorem
aM_aT_eq_of_c_hbar -
theorem
aT_aM_eq_of_c_G -
theorem
a_T_sq_eq -
def
tau_Planck -
theorem
tau_Planck_pos -
theorem
a_T_eq -
theorem
tau0_eq_sqrt_pi_planck_time -
def
tau0_predicted_seconds -
theorem
tau0_predicted_seconds_pos -
theorem
si_bridge_closed_under_three_constraints -
structure
SIBridgeClosureCert -
def
siBridgeClosureCert -
theorem
siBridgeClosureCert_inhabited