dimensionless_theory_needs_anchor
plain-language theorem explainer
Any monomial in c, ħ, and G whose (L,T,M) dimension vector vanishes must be the trivial constant monomial. A pure-number theory can therefore fix only dimensionless native relations among these three constants; an absolute SI value needs a dimensional anchor. Anyone arguing the SI-bridge boundary in Recognition Science would cite this. The proof is a one-line application of the nontrivial-monomial vanishing lemma.
Claim. If the length-time-mass dimension vector of the monomial $c^a \hbar^b G^d$ is $(0,0,0)$, then the integer exponents satisfy $a=0$, $b=0$, and $d=0$.
background
This module records the honest boundary between first-principles native constants and SI calibration. Recognition Science can force dimensionless native identities such as $\hbar_{\mathrm{RS}}=\varphi^{-5}$ and $G_{\mathrm{RS}}\hbar_{\mathrm{RS}}=1/\pi$, but cannot, from pure dimensionless data alone, output absolute SI values of $\hbar$ or $G$. A dimensional bridge needs a dimensional anchor.
The dimension map sends integer exponents $(a,b,d)$ to the $(L,T,M)$ triple of $c^a\hbar^b G^d$, using $c\sim L T^{-1}$, $\hbar\sim M L^2 T^{-1}$, $G\sim L^3 M^{-1} T^{-2}$. The three columns are linearly independent, so no nontrivial monomial is dimensionless. That independence is the content of the upstream vanishing lemma this result wraps.
The positive half (one anchor suffices and determines the bridge uniquely) already lives in SIBridgeClosure and SingleAnchor. This module proves only the negative half: an anchor is required.
proof idea
One-line term proof: apply the upstream lemma that no nontrivial monomial in $c$, $\hbar$, and $G$ is dimensionless, feeding it the hypothesis that the dimension triple is $(0,0,0)$. That lemma unfolds the dimension map, splits the product equality into three integer equations for $(L,T,M)$, and solves the linear system to force $a=b=d=0$.
why it matters
Names the necessity half of the native dimensional boundary: pure dimensionless data cannot fix absolute SI scales for $c$, $\hbar$, and $G$. Paired with the positive half already formalized elsewhere (tick conversion uniquely $\sqrt{\pi}$ times Planck time under the $c,\hbar,G$ constraints; one scalar $\tau_0$ determining the full external calibration; the first-principles-to-SI capstone with T0–T8 plus a single anchor), it underwrites the module claim that exactly one dimensional anchor determines everything.
This is dimensional analysis, not a defect of RS. It protects the honest split between forced native relations (including the RS-native units $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and SI calibration. No downstream users are recorded yet; the declaration is the named interface for the necessity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.