IndisputableMonolith.Constants.NativeDimensionalBoundary

   1import Mathlib
   2import IndisputableMonolith.Foundation.SIBridgeClosure
   3
   4/-!
   5# Native Constants and the Dimensional Boundary
   6
   7This module records the honest boundary between first-principles native
   8constants and SI calibration.
   9
  10The recognition framework can force dimensionless/native identities such as
  11`hbar_RS = phi^(-5)`, `G_RS * hbar_RS = 1/pi`, and `kappa_RS * hbar_RS = 8`.
  12It cannot, from pure dimensionless data alone, output the absolute SI value of
  13`hbar` or `G`.  A dimensional bridge needs a dimensional anchor.
  14
  15This is not a weakness of RS; it is dimensional analysis.  The dimensions of
  16`c`, `hbar`, and `G` are independent, so no nontrivial monomial
  17`c^a hbar^b G^d` is dimensionless.
  18
  19## Where the positive half lives (do not re-prove it here)
  20
  21This module proves the negative half (an anchor is *required*). The positive
  22half (one anchor *suffices* and determines the whole bridge uniquely) is
  23already formalized, more completely, elsewhere:
  24
  25* `Foundation.SIBridgeClosure.tau0_eq_sqrt_pi_planck_time` /
  26  `a_T_sq_eq`: given the `c, ℏ, G` constraints, the tick conversion factor is
  27  uniquely `a_T = √π · τ_Planck`.
  28* `Measurement.RSNative.Calibration.SingleAnchor`: from one scalar (`τ₀` in
  29  seconds) the full `ExternalCalibration` is derived (meters/voxel from SI `c`,
  30  joules/coh from SI `ℏ`).
  31* `Verification.FirstPrinciplesToSI.first_principles_to_SI_capstone`: T0–T8 plus
  32  the single anchor `τ₀` yields the electron mass in SI kilograms with the mass
  33  audit at 0 Hypothesis / 0 Open / 0 External.
  34
  35Together: exactly one dimensional anchor, and it determines everything.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Constants
  40namespace NativeDimensionalBoundary
  41
  42open IndisputableMonolith.Foundation.SIBridgeClosure
  43
  44noncomputable section
  45
  46/-- Dimension exponents `(L,T,M)` of a monomial `c^a hbar^b G^d`.
  47
  48`c` has dimensions `L T^-1`; `hbar` has dimensions `M L^2 T^-1`;
  49`G` has dimensions `L^3 M^-1 T^-2`. -/
  50def cHbarGDimension (a b d : ℤ) : ℤ × ℤ × ℤ :=
  51  (a + 2 * b + 3 * d, -a - b - 2 * d, b - d)
  52
  53/-- The `(c, hbar, G)` dimension matrix: columns are the `(L,T,M)` exponent
  54vectors of `c = (1,-1,0)`, `hbar = (2,-1,1)`, `G = (3,-2,-1)`. -/
  55def dimMatrix : Matrix (Fin 3) (Fin 3) ℤ :=
  56  Matrix.of ![![1, 2, 3], ![-1, -1, -2], ![0, 1, -1]]
  57
  58/-- The determinant of the `(c, hbar, G)` dimension matrix is `-2` (a real
  59`Matrix.det`, not a free-floating numeral). The value `-2` (rather than `±1`)
  60also records that `(c, hbar, G)` span an index-`2` sublattice of the integer
  61dimension lattice, so the Planck system is a basis only up to half-integer
  62powers; but the only fact the boundary argument needs is `det ≠ 0`. -/
  63theorem dimMatrix_det : dimMatrix.det = -2 := by
  64  simp [dimMatrix, Matrix.det_fin_three, Matrix.of_apply,
  65    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
  66    Matrix.cons_val_fin_one]
  67
  68/-- The determinant of the `(c,hbar,G)` dimension matrix is nonzero, i.e. the
  69three dimension vectors are linearly independent. -/
  70theorem dimension_matrix_c_hbar_G_det_nonzero : dimMatrix.det ≠ 0 := by
  71  rw [dimMatrix_det]; norm_num
  72
  73/-- No nontrivial monomial in `c`, `hbar`, and `G` is dimensionless. -/
  74theorem no_nontrivial_dimensionless_monomial {a b d : ℤ}
  75    (h : cHbarGDimension a b d = (0, 0, 0)) :
  76    a = 0 ∧ b = 0 ∧ d = 0 := by
  77  unfold cHbarGDimension at h
  78  simp only [Prod.mk.injEq] at h
  79  rcases h with ⟨hL, hT, hM⟩
  80  omega
  81
  82/-- A pure-number theory can fix only dimensionless/native relations among
  83`c`, `hbar`, and `G`; an absolute SI value needs a dimensional anchor. -/
  84theorem dimensionless_theory_needs_anchor {a b d : ℤ}
  85    (hDimensionless : cHbarGDimension a b d = (0, 0, 0)) :
  86    a = 0 ∧ b = 0 ∧ d = 0 :=
  87  no_nontrivial_dimensionless_monomial hDimensionless
  88
  89/-- The squared tick scale that the SI bridge assigns after a positive supplied
  90value of Newton's constant.  This is the same algebraic shape as
  91`SIBridgeClosure.a_T_sq_eq`, but with `G_input` left variable to expose the
  92anchor dependence. -/
  93def calibratedTickSquare (G_input : ℝ) : ℝ :=
  94  Real.pi * hbar_SI * G_input / c_SI ^ 5
  95
  96/-- Any positive supplied `G_input` gives a positive calibrated tick square. -/
  97theorem calibratedTickSquare_pos {G_input : ℝ} (hG : 0 < G_input) :
  98    0 < calibratedTickSquare G_input := by
  99  unfold calibratedTickSquare
 100  exact div_pos (mul_pos (mul_pos Real.pi_pos hbar_SI_pos) hG) (pow_pos c_SI_pos 5)
 101
 102/-- Changing the supplied `G` changes the calibrated tick square.  Thus the SI
 103bridge depends on the dimensional anchor; it does not predict that anchor. -/
 104theorem calibratedTickSquare_injective :
 105    Function.Injective calibratedTickSquare := by
 106  intro G₁ G₂ h
 107  unfold calibratedTickSquare at h
 108  have hcoeff : Real.pi * hbar_SI / c_SI ^ 5 ≠ 0 := by
 109    exact div_ne_zero (mul_ne_zero Real.pi_ne_zero hbar_SI_pos.ne') (pow_ne_zero 5 c_SI_pos.ne')
 110  have hlin : (Real.pi * hbar_SI / c_SI ^ 5) * G₁ =
 111      (Real.pi * hbar_SI / c_SI ^ 5) * G₂ := by
 112    calc
 113      (Real.pi * hbar_SI / c_SI ^ 5) * G₁
 114          = Real.pi * hbar_SI * G₁ / c_SI ^ 5 := by ring
 115      _ = Real.pi * hbar_SI * G₂ / c_SI ^ 5 := h
 116      _ = (Real.pi * hbar_SI / c_SI ^ 5) * G₂ := by ring
 117  exact (mul_left_cancel₀ hcoeff hlin)
 118
 119/-- The SI bridge is a calibration map: for every positive supplied dimensional
 120anchor `G_input`, the bridge assigns a positive tick-square scale, and different
 121anchors give different scales. -/
 122theorem si_bridge_is_calibration_not_prediction :
 123    (∀ G_input : ℝ, 0 < G_input → 0 < calibratedTickSquare G_input) ∧
 124      Function.Injective calibratedTickSquare :=
 125  ⟨fun _ hG => calibratedTickSquare_pos hG, calibratedTickSquare_injective⟩
 126
 127/-- Certificate packaging the dimensional-boundary audit. -/
 128structure NativeDimensionalBoundaryCert where
 129  determinant_nonzero : dimMatrix.det ≠ 0
 130  no_dimensionless_monomial :
 131    ∀ {a b d : ℤ}, cHbarGDimension a b d = (0, 0, 0) → a = 0 ∧ b = 0 ∧ d = 0
 132  bridge_calibrates :
 133    (∀ G_input : ℝ, 0 < G_input → 0 < calibratedTickSquare G_input) ∧
 134      Function.Injective calibratedTickSquare
 135
 136/-- Native constants are first-principles objects only up to the dimensional
 137boundary; SI conversion is a uniquely constrained calibration once an anchor is
 138supplied. -/
 139theorem native_dimensional_boundary_cert : NativeDimensionalBoundaryCert where
 140  determinant_nonzero := dimension_matrix_c_hbar_G_det_nonzero
 141  no_dimensionless_monomial := fun h => no_nontrivial_dimensionless_monomial h
 142  bridge_calibrates := si_bridge_is_calibration_not_prediction
 143
 144end
 145
 146end NativeDimensionalBoundary
 147end Constants
 148end IndisputableMonolith
 149