Pith. sign in
module module moderate

IndisputableMonolith.Verification.DimensionalRigidity

show as:
view Lean formalization →

Module on dimensional rigidity of the SI triad c, ħ, G in the (M,L,T) basis. It records their exponent vectors, the 3×3 dimension matrix and its determinant, then proves there is no nontrivial dimensionless monomial and that SI numerical values cannot be fixed by pure numbers alone. Verification and units arguments in RS cite it. The arc is definition of vectors, a determinant check, then two corollaries.

claimIn the $(M,L,T)$ basis the dimension vectors of $c$, $\hbar$, and $G$ assemble into a $3\times 3$ matrix of nonzero determinant. Hence no nontrivial dimensionless combination $c^{a}\hbar^{b}G^{d}$ exists, and the SI numerical values of these constants are not derivable from pure numbers alone.

background

Dimensional analysis assigns each physical quantity an exponent triple in mass, length, and time. The speed of light, reduced Planck constant, and Newton constant are the usual generators of the SI mechanical sector; their exponent vectors are the rows (or columns) of a $3\times 3$ dimension matrix.

Recognition Science works in native units with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$. Separating those pure-number assignments from SI bookkeeping requires knowing that the triad is dimensionally rigid: the only way to cancel all three dimensions is the zero exponent vector.

The module sits in the Verification domain. Sibling definitions name the individual vectors (dimC, dimHbar, dimG), the assembled matrix and its determinant, and the two rigidity statements that follow from $\det\neq 0$.

proof idea

Definition layer first: exponent vectors of $c$, $\hbar$, $G$ in $(M,L,T)$, then the $3\times 3$ dimension matrix and an explicit determinant evaluation. From $\det\neq 0$ one obtains linear independence of the three rows, hence the only integer (or real) solution of $a,\mathrm{dim}(c)+b,\mathrm{dim}(\hbar)+d,\mathrm{dim}(G)=0$ is $a=b=d=0$. The final statement lifts that algebraic fact to the claim that SI numerical values are not fixed by pure-number identities alone. No deep analysis; the work is bookkeeping plus a $3\times 3$ determinant.

why it matters in Recognition Science

RS quotes concrete native values $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$ and an $\alpha^{-1}$ band near $137$. Those claims are meaningful only after one separates dimensionless RS content from SI unit conventions. This module supplies that separation: because the dimension matrix is invertible, no hidden dimensionless combination can smuggle SI magnitudes out of pure arithmetic.

Downstream verification developments that compare RS predictions to CODATA-style SI numbers rely on exactly this rigidity. It does not itself derive the native values; it certifies that the dimensional obstruction is absent of loopholes. Landmarks touched: the RS-native constant package and the verification layer that audits it against ordinary dimensional analysis.

scope and limits

declarations in this module (8)