Pith. sign in
module module high

IndisputableMonolith.Constants.NativeDimensionalBoundary

show as:
view Lean formalization →

Module on the dimensional boundary of the triple $(c,\hbar,G)$: the $3\times 3$ exponent matrix in $(L,T,M)$ is invertible, so no nontrivial dimensionless monomial exists in those constants alone. Any dimensionless claim therefore needs an external anchor (RS tick or SI bridge). Linear-algebra argument on the classical dimension matrix; certifies that the SI map is calibration, not prediction.

claimWrite $\mathrm{dim}(c^a\hbar^b G^d)=(L,T,M)$ via the classical exponents: $c\sim L T^{-1}$, $\hbar\sim M L^2 T^{-1}$, $G\sim L^3 M^{-1} T^{-2}$. The resulting $3\times 3$ matrix has nonzero determinant, so the only dimensionless monomial is the trivial one. A dimensionless theory therefore requires an external dimensional anchor (e.g. a calibrated tick).

background

Classical dimensional analysis assigns length $L$, time $T$, and mass $M$ to every monomial built from $c$, $\hbar$, and $G$. Explicitly: $c$ carries $L T^{-1}$, $\hbar$ carries $M L^2 T^{-1}$, and $G$ carries $L^3 M^{-1} T^{-2}$. Stacking the three exponent vectors yields a $3\times 3$ integer matrix whose kernel consists of the dimensionless combinations.

Recognition Science works in native units where $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$. Converting those native values into SI requires a unique calibration map once a dimensional anchor is fixed. The upstream SI-bridge closure module states that this conversion map is structural once the anchor is supplied; the present module supplies the dimensional linear algebra that makes the anchor necessary.

Sibling objects include the dimension matrix itself, its determinant, the statement that no nontrivial dimensionless monomial exists, the calibrated-tick square (positive and injective), and a certificate that the SI bridge is calibration rather than prediction.

proof idea

Definition-plus-linear-algebra module. The dimension map is introduced as an explicit $3\times 3$ matrix on exponent triples $(a,b,d)$. Determinant is computed by direct expansion and shown nonzero, hence the matrix is invertible over $\mathbb{Q}$. Kernel triviality immediately yields: the only dimensionless monomial $c^a\hbar^b G^d$ is the unit. From that, any dimensionless theoretical claim must import an external scale (the calibrated tick). Positivity and injectivity of the calibrated-tick square are recorded as elementary real lemmas. A thin certificate packages the boundary statement for downstream SI-bridge use.

why it matters in Recognition Science

Closes the dimensional half of the SI-bridge story: without an external anchor there is no dimensionless content extractable from $(c,\hbar,G)$ alone, so the bridge cannot be a prediction and must be a calibration. Upstream SIBridgeClosure already treats the conversion map as structural once the anchor is given; this module supplies the linear-algebra reason the anchor is mandatory. In the broader RS constants layer it underwrites the claim that native values ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) become SI numbers only after a single dimensional fixing, consistent with the forcing chain's unique $\varphi$ and eight-tick structure. No downstream consumers are listed yet; the certificate is the intended hand-off point.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)