Constants Native Dimensional Boundary No Nontrivial Dimensionless Monomial

The dimensional boundary

Dimensional analysis is the discipline of checking that physical equations respect units. Length, time, and mass are independent dimensions, and the constants speed of light c, Planck constant ℏ, and gravitational constant G carry them in different combinations. The theorem no_nontrivial_dimensionless_monomial states that no product c^aℏ^bG^d with integer exponents is dimensionless unless all three exponents are zero. In plain language: from these three constants alone, pure arithmetic cannot produce a unit-free number that would pin down their absolute sizes.

This is a classical fact, not a framework invention. The dimension vectors of c, ℏ, and G are linearly independent, so their only dimensionless combination is the trivial one. The framework's machine-checked library of formal theorems proves it by computing the determinant of the 3×3 dimension matrix, which is −2, and therefore nonzero. The proof is a short algebraic check, and the result is exactly what dimensional analysis has always said: the dimensions of c, ℏ, and G are independent, so no monomial in them is dimensionless.

The consequence for the Recognition Science framework is a boundary on what it can claim. The framework derives native identities such as ℏ = φ⁻⁵ and Gℏ = 1/π, which are dimensionless relations among its own units. But it cannot, from pure dimensionless data alone, output the absolute SI value of ℏ or G. The theorem dimensionless_theory_needs_anchor makes this explicit: a pure-number theory can fix only dimensionless relations; an absolute SI value requires a dimensional anchor, one measured input such as a tick duration in seconds.

In Recognition Science, this boundary is not a weakness but a calibration condition. The framework's library shows that one scalar anchor, τ₀ in seconds, suffices to determine the whole bridge from native units to SI: meters per voxel follow from SI c, joules per coh from SI ℏ, and the electron mass in kilograms follows from the full T0–T8 chain plus that single anchor. The theorem si_bridge_is_calibration_not_prediction states the map from a supplied G value to the calibrated tick scale is positive and injective: different anchors give different scales, so the bridge calibrates rather than predicts. The boundary theorem is what makes this honesty precise: exactly one dimensional anchor is required, and it determines everything else.

/-- 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

/-- 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

/-- 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

/-- The SI bridge is a calibration map: for every positive supplied dimensional
anchor `G_input`, the bridge assigns a positive tick-square scale, and different
anchors give different scales. -/
theorem si_bridge_is_calibration_not_prediction :
    (∀ G_input : ℝ, 0 < G_input → 0 < calibratedTickSquare G_input) ∧
      Function.Injective calibratedTickSquare :=
  ⟨fun _ hG => calibratedTickSquare_pos hG, calibratedTickSquare_injective⟩

What this page does not claim

This theorem does not prove that the framework's native identities like ℏ = φ⁻⁵ are correct in SI units. This theorem does not claim that a dimensional anchor can be derived from pure theory rather than supplied by measurement. This theorem does not establish the value of any individual constant; it only establishes the boundary on what pure dimensionless reasoning can fix.

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: