IndisputableMonolith.Verification.DimensionalRigidity

   1import Mathlib
   2
   3/-!
   4# Dimensional Rigidity: No Dimensionless Combination of c, ℏ, G
   5
   6**NO-GO CERTIFICATE** (2026-07-06, resolving the ℏ/G audit's category-error
   7finding as a kernel-checked boundary stone).
   8
   9## The claim
  10
  11In the (M, L, T) dimension basis the three constants carry exponent vectors
  12
  13  c : (0, 1, −1)     [L T⁻¹]
  14  ℏ : (1, 2, −1)     [M L² T⁻¹]
  15  G : (−1, 3, −2)    [M⁻¹ L³ T⁻²]
  16
  17The matrix of these vectors has determinant −2 ≠ 0, so the vectors are
  18linearly independent over ℚ: **the only dimensionless monomial
  19c^a · ℏ^b · G^g is the trivial one (a = b = g = 0).**
  20
  21## Why this matters for RS_v1
  22
  23A dimensionless framework (any framework whose outputs are pure numbers)
  24can therefore never DERIVE the SI values of c, ℏ, or G. It can only fix
  25their values in its own native units and calibrate to SI through an
  26externally supplied scale (one anchor). Claims of the form "the framework
  27derives ℏ" are category errors, and this file makes the obstruction a
  28theorem rather than a footnote. The native identities ℏ_R = φ⁻⁵ and
  29G_R = φ⁵/π are DEFINITIONS of native units, not predictions of SI values.
  30
  31This is a LOCAL no-go about dimensionFUL constants. It says nothing
  32against deriving dimensionLESS quantities (mass ratios, α, g⋆-type
  33counts), which remain the legitimate targets.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Verification
  38namespace DimensionalRigidity
  39
  40/-- Dimension exponent vector of c in the (M, L, T) basis. -/
  41def dimC : Fin 3 → ℚ := ![0, 1, -1]
  42
  43/-- Dimension exponent vector of ℏ in the (M, L, T) basis. -/
  44def dimHbar : Fin 3 → ℚ := ![1, 2, -1]
  45
  46/-- Dimension exponent vector of G in the (M, L, T) basis. -/
  47def dimG : Fin 3 → ℚ := ![-1, 3, -2]
  48
  49/-- The dimension matrix with rows (c, ℏ, G). -/
  50def dimMatrix : Matrix (Fin 3) (Fin 3) ℚ :=
  51  Matrix.of ![dimC, dimHbar, dimG]
  52
  53/-- The dimension matrix has determinant −2. -/
  54theorem dimMatrix_det : dimMatrix.det = -2 := by
  55  simp [dimMatrix, dimC, dimHbar, dimG, Matrix.det_fin_three]
  56  norm_num
  57
  58/-- **THE NO-GO**: no nontrivial dimensionless monomial in (c, ℏ, G).
  59If a·dim(c) + b·dim(ℏ) + g·dim(G) = 0 componentwise (i.e. c^a ℏ^b G^g is
  60dimensionless), then a = b = g = 0. -/
  61theorem no_dimensionless_combination (a b g : ℚ)
  62    (h : ∀ i : Fin 3, a * dimC i + b * dimHbar i + g * dimG i = 0) :
  63    a = 0 ∧ b = 0 ∧ g = 0 := by
  64  have h0 := h 0
  65  have h1 := h 1
  66  have h2 := h 2
  67  simp [dimC, dimHbar, dimG, Fin.isValue] at h0 h1 h2
  68  refine ⟨?_, ?_, ?_⟩ <;> linarith
  69
  70/-- Corollary, stated in the direction referees will quote: a framework whose
  71outputs are pure numbers cannot output the SI value of any one of c, ℏ, G
  72individually; only a dimensionless combination could be framework-derivable,
  73and by `no_dimensionless_combination` no nontrivial one exists. -/
  74theorem si_values_not_derivable_from_pure_numbers :
  75    ¬ ∃ (a b g : ℚ), (a, b, g) ≠ (0, 0, 0) ∧
  76      (∀ i : Fin 3, a * dimC i + b * dimHbar i + g * dimG i = 0) := by
  77  rintro ⟨a, b, g, hne, h⟩
  78  obtain ⟨ha, hb, hg⟩ := no_dimensionless_combination a b g h
  79  exact hne (by simp [ha, hb, hg])
  80
  81end DimensionalRigidity
  82end Verification
  83end IndisputableMonolith
  84