Constants Native Dimensional Boundary

The dimensional boundary

In physics, the speed of light c, Planck's constant hbar, and Newton's gravitational constant G carry independent dimensions: length per time, action, and a gravitational coupling. A monomial c^a hbar^b G^d is dimensionless only when all three exponents are zero. This is a classical dimensional-analysis fact, and it sets the boundary for any theory that hopes to derive constants from pure numbers.

Recognition Science (RS) is such a theory. Its framework derives dimensionless relations among constants, for example hbar_RS = phi^(-5), where phi is the golden ratio, and G_RS * hbar_RS = 1/pi. These are native identities, forced by the theory's structure. But the framework cannot output the absolute SI value of hbar or G from dimensionless data alone. The dimensional boundary module records this honestly: a dimensional bridge needs a dimensional anchor, one measured number in seconds, meters, or kilograms.

The module proves the negative half of this claim by formal theorem. It constructs the dimension matrix for (c, hbar, G), shows its determinant is -2, and proves that no nontrivial monomial in the three constants is dimensionless. The positive half, that one anchor suffices and determines the whole bridge uniquely, is formalized elsewhere in the library, including a capstone that derives the electron mass in SI kilograms from a single anchor with zero hypotheses or open goals.

The bridge itself is a calibration map, not a prediction. The module defines a calibrated tick square, the squared time scale the SI bridge assigns for a supplied value of G, and proves it is positive for any positive input and injective: different anchors give different scales. This is the honest boundary: the framework constrains the shape of the bridge completely, but the absolute scale comes from measurement.

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

The module does not prove that one anchor suffices; that positive half lives in other files. It does not derive the SI value of hbar or G from pure numbers. The determinant -2 being nonzero is the only fact the boundary argument needs; the index-2 sublattice structure is not used.

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: