calibratedTickSquare
plain-language theorem explainer
Defines the SI-bridge squared tick scale as π ħ_SI G_input / c_SI^5, leaving Newton's constant free. Anyone auditing the dimensional boundary between RS-native units and SI calibration cites this map. It is a one-line algebraic definition matching the closed-form tick factor from SIBridgeClosure, with G kept as an input anchor.
Claim. For a real input $G_{\mathrm{input}}$, the calibrated squared tick is $\pi\,\hbar_{\mathrm{SI}}\,G_{\mathrm{input}}/c_{\mathrm{SI}}^{5}$, where $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are the fixed SI external anchors for the speed of light and reduced Planck constant.
background
Recognition Science forces dimensionless native identities such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but cannot output absolute SI values of $\hbar$ or $G$ from pure dimensionless data. The module records that honest boundary: $c$, $\hbar$, and $G$ have independent dimensions, so no nontrivial monomial $c^a\hbar^b G^d$ is dimensionless, and a dimensional bridge needs one external anchor.
The fundamental RS time quantum is the tick $\tau_0=1$ in native units. On the SI side, $c_{\mathrm{SI}}=299792458,\mathrm{m/s}$ and $\hbar_{\mathrm{SI}}$ are fixed external anchors (SI 2019). The positive half of the story already lives in SIBridgeClosure: given the $c,\hbar,G$ constraints, the tick conversion is uniquely $a_T=\sqrt{\pi},\tau_{\mathrm{Planck}}$. This definition keeps $G$ variable so the anchor dependence is visible.
proof idea
Pure definition: the body is the monomial $\pi\cdot\hbar_{\mathrm{SI}}\cdot G_{\mathrm{input}}/c_{\mathrm{SI}}^5$. No tactics or lemmas; it is the same algebraic shape as the closed-form squared tick factor in SIBridgeClosure, with Newton's constant left as a free real parameter rather than a fixed constant.
why it matters
This map is the witness that the SI bridge is calibration, not prediction. Downstream, positivity for every positive $G_{\mathrm{input}}$ and injectivity (different $G$ give different tick squares) are packaged into si_bridge_is_calibration_not_prediction and into the NativeDimensionalBoundaryCert audit fields. Together with the nonzero dimension-matrix determinant and the no-nontrivial-dimensionless-monomial lemma, it closes the negative half of the dimensional-boundary claim: an anchor is required, and the bridge does not invent one. The positive half (one anchor suffices) is already formalized elsewhere via T0–T8 plus a single $\tau_0$ anchor yielding SI masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.