Constants Native Dimensional Boundary Dim Matrix Det

The dimensional boundary

The speed of light c, Planck's constant hbar, and Newton's gravitational constant G each carry dimensions: length, time, and mass in different combinations. The declaration dimMatrix_det computes the determinant of the matrix whose columns are these three dimension vectors. The result is -2, a nonzero value. That single fact carries a consequence: the three vectors are linearly independent, so no nontrivial product of powers of c, hbar, and G can be dimensionless.

This is a statement about dimensional analysis, not about any particular physical theory. In the International System of Units, c has dimensions L T⁻¹, hbar has M L² T⁻¹, and G has L³ M⁻¹ T⁻². The determinant of the matrix formed from these exponent vectors is -2, not zero. The nonzero determinant means the three dimensions span a three-dimensional space, and no integer combination of their exponent vectors returns to zero unless all exponents are zero. The framework's machine-checked library of formal theorems proves this as a theorem, not as an assumption.

In Recognition Science, this theorem marks the boundary between what a pure number theory can fix and what requires an external measurement. The framework can derive dimensionless relations among c, hbar, and G, such as hbar_RS = phi^(-5) and G_RS * hbar_RS = 1/pi. It cannot derive the absolute SI value of hbar or G from pure dimensionless data alone. A dimensional bridge needs a dimensional anchor: one measured quantity, such as a tick duration in seconds, from which the full conversion to SI units follows uniquely.

The determinant being -2 rather than ±1 adds a finer detail. It records that c, hbar, and G span an index-2 sublattice of the integer dimension lattice, meaning the Planck system is a basis only up to half-integer powers. But the boundary argument needs only the weaker fact that the determinant is nonzero. The framework's library also proves that any positive supplied value of G gives a positive calibrated tick square, and different anchors give different scales. The SI bridge is a calibration map, not a prediction of the anchor itself.

/-- The determinant of the `(c, hbar, G)` dimension matrix is `-2` (a real
`Matrix.det`, not a free-floating numeral). The value `-2` (rather than `±1`)
also records that `(c, hbar, G)` span an index-`2` sublattice of the integer
dimension lattice, so the Planck system is a basis only up to half-integer
powers; but the only fact the boundary argument needs is `det ≠ 0`. -/
theorem dimMatrix_det : dimMatrix.det = -2 := by
  simp [dimMatrix, Matrix.det_fin_three, Matrix.of_apply,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
    Matrix.cons_val_fin_one]

/-- The determinant of the `(c,hbar,G)` dimension matrix is nonzero, i.e. the
three dimension vectors are linearly independent. -/
theorem dimension_matrix_c_hbar_G_det_nonzero : dimMatrix.det ≠ 0 := by
  rw [dimMatrix_det]; norm_num

/-- No nontrivial monomial in `c`, `hbar`, and `G` is dimensionless. -/
theorem no_nontrivial_dimensionless_monomial {a b d : ℤ}
    (h : cHbarGDimension a b d = (0, 0, 0)) :
    a = 0 ∧ b = 0 ∧ d = 0 := by
  unfold cHbarGDimension at h
  simp only [Prod.mk.injEq] at h
  rcases h with ⟨hL, hT, hM⟩
  omega

/-- A pure-number theory can fix only dimensionless/native relations among
`c`, `hbar`, and `G`; an absolute SI value needs a dimensional anchor. -/
theorem dimensionless_theory_needs_anchor {a b d : ℤ}
    (hDimensionless : cHbarGDimension a b d = (0, 0, 0)) :
    a = 0 ∧ b = 0 ∧ d = 0 :=
  no_nontrivial_dimensionless_monomial hDimensionless

What this page does not claim

The theorem does not derive the numerical SI value of hbar or G from pure theory. The nonzero determinant does not by itself determine the physical scale of any constant. The determinant value -2 does not imply the Planck system is a valid basis for all integer powers.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/NativeDimensionalBoundary.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: