calibratedTickSquare_injective
plain-language theorem explainer
The map sending a supplied Newton constant G to the SI-bridge tick-square scale π ℏ_SI G / c_SI^5 is injective on the reals. Anyone arguing that the RS–SI bridge is a calibration (not a prediction of G) cites this. The proof is a short cancellation: the prefactor π ℏ_SI / c_SI^5 is nonzero, so equal images force equal G.
Claim. The real map $G \mapsto \pi \, \hbar_{\mathrm{SI}} \, G / c_{\mathrm{SI}}^{5}$ is injective: if two supplied values of Newton's constant produce the same calibrated tick-square scale, then the two values are equal.
background
This module draws the honest line between RS-native dimensionless identities and SI units. Recognition Science forces relations such as $\hbar_{\mathrm{RS}} = \varphi^{-5}$ and $G_{\mathrm{RS}} \hbar_{\mathrm{RS}} = 1/\pi$, but pure dimensionless data cannot fix the absolute SI values of $\hbar$ or $G$. A dimensional bridge needs a dimensional anchor.
The calibrated tick square is the squared conversion factor the SI bridge assigns once a positive $G$ is supplied: $\mathrm{calibratedTickSquare}(G) = \pi , \hbar_{\mathrm{SI}} , G / c_{\mathrm{SI}}^{5}$. It has the same algebraic shape as the closed-form $a_T^{2}$ identity in SIBridgeClosure, with $G$ left free so anchor dependence is visible. Here $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are the fixed 2019 SI external anchors (exact $c$, CODATA $\hbar$), both strictly positive.
The native tick is the RS time quantum $\tau_0 = 1$. The positive half of the story (one anchor suffices and determines the full bridge) lives in SIBridgeClosure and SingleAnchor; this module proves the negative half: an anchor is required.
proof idea
Tactic proof by direct cancellation. Fix $G_1, G_2$ with equal calibrated tick squares. Unfold the definition so the hypothesis is $\pi , \hbar_{\mathrm{SI}} , G_1 / c_{\mathrm{SI}}^{5} = \pi , \hbar_{\mathrm{SI}} , G_2 / c_{\mathrm{SI}}^{5}$. The prefactor $\pi , \hbar_{\mathrm{SI}} / c_{\mathrm{SI}}^{5}$ is nonzero because $\pi \neq 0$, $\hbar_{\mathrm{SI}} > 0$, and $c_{\mathrm{SI}} > 0$ (so its fifth power is nonzero). Rewrite both sides as that prefactor times $G_i$ by ring, then apply left-cancellation for multiplication by a nonzero real. No RS-specific lemmas beyond positivity of the SI anchors.
why it matters
Feeds directly into si_bridge_is_calibration_not_prediction, which packages positivity and injectivity: every positive $G$ yields a positive tick-square scale, and distinct anchors yield distinct scales. That theorem is the prose claim that the SI bridge is a calibration map, not a prediction of Newton's constant.
In the broader framework this is the dimensional-boundary audit. RS forces the dimensionless skeleton (T0–T8, J-uniqueness, $\varphi$, eight-tick octave, $D=3$) and the native relations among $c$, $\hbar$, $G$ in RS units, but the absolute SI placement of the ladder needs exactly one external anchor. Injectivity says the bridge cannot hide a free $G$: changing the anchor moves the tick scale. Together with the positive half (one anchor determines the whole ExternalCalibration and the first-principles-to-SI capstone), the ledger is: exactly one dimensional anchor, and it determines everything.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.