aT_aM_eq_of_c_G
plain-language theorem explainer
Under the speed-of-light and Newton-G matching constraints on an SI bridge, the ratio of tick duration to coherence-mass equals G_SI/(G_RS c_SI³). Anyone deriving the unique SI calibration (especially a_T² = π ħ_SI G_SI/c_SI⁵) cites this ratio identity. The proof substitutes the c-forced length factor into the G-constraint, clears denominators, and rearranges by linear combination.
Claim. Let $b$ be an SI bridge with positive conversion factors $a_T$ (seconds per tick), $a_L$ (metres per voxel), and $a_M$ (kilograms per coherence-mass). If the $c$-constraint $c_{\mathrm{SI}} = c_{\mathrm{RS}}\, a_L/a_T$ and the $G$-constraint $G_{\mathrm{SI}} = G_{\mathrm{RS}}\, a_L^3/(a_M a_T^2)$ both hold, then $a_T/a_M = G_{\mathrm{SI}}/(G_{\mathrm{RS}}\, c_{\mathrm{SI}}^3)$.
background
The SIBridgeClosure module fixes the dimensional conversion from RS-native units to SI. An SI bridge is three strictly positive factors: $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/coherence-mass). Matching the dimensionless RS predictions $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$ against SI anchors yields three constraints; this lemma uses only the $c$- and $G$-constraints.
The $c$-constraint is $c_{\mathrm{SI}}=c_{\mathrm{RS}},a_L/a_T$ with $c_{\mathrm{SI}}$ the exact SI-2019 speed of light. The $G$-constraint is $G_{\mathrm{SI}}=G_{\mathrm{RS}},a_L^3/(a_M a_T^2)$, where $G_{\mathrm{SI}}$ is the CODATA measured Newton constant (the single remaining dimensional anchor after SI 2019) and $G_{\mathrm{RS}}=\varphi^5/\pi$ is the RS-native value from the recognition/Planck bridge $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ at $\lambda_{\mathrm{rec}}=c=1$.
Upstream, $a_L$ is already solved from the $c$-constraint alone (via aL_eq_of_c_constraint), so the length factor can be eliminated and the $G$-equation reduced to a pure $a_T/a_M$ ratio.
proof idea
Apply the upstream identity that the $c$-constraint forces $a_L=c_{\mathrm{SI}} a_T$ (with $c_{\mathrm{RS}}=1$). Record positivity-derived nonzeros for $a_T$, $a_M$, $G_{\mathrm{RS}}$, and $c_{\mathrm{SI}}^3$. Unfold the $G$-constraint and substitute that $a_L$. After field_simp, the equation is equivalent to the polynomial form $G_{\mathrm{SI}},a_M=G_{\mathrm{RS}},c_{\mathrm{SI}}^3,a_T$ (the $a_T^2$ in the denominator cancels one power from $(c_{\mathrm{SI}} a_T)^3$). Rewrite the target ratio equality as a cross-multiplication and finish by linear_combination against that polynomial identity.
why it matters
This is one of the two helper ratio identities feeding the module's main algebraic closure a_T_sq_eq: under all three constraints, $a_T^2=\pi,\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$, i.e. the fundamental tick satisfies $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$. Downstream multiplies $(a_M a_T)\cdot(a_T/a_M)=a_T^2$ using this lemma together with the companion $c$+$\hbar$ ratio, then inserts $\hbar_{\mathrm{RS}} G_{\mathrm{RS}}=1/\pi$.
In the Recognition framework the native constants are fixed ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$); what remained open was uniqueness of the SI conversion map once the dimensional anchor is supplied. This lemma eliminates $a_L$ from $c$ and $G$ alone, so the tick-to-mass ratio is determined without further input. It does not predict $G_{\mathrm{SI}}$; it only closes the calibration algebra that turns the CODATA anchor into a unique $\tau_0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.