Constants Native Dimensional Boundary Native Dimensional Boundary Cert

The dimensional boundary

The speed of light c, Planck's constant ℏ, and Newton's gravitational constant G carry independent physical dimensions: length per time, action, and the coupling of mass to spacetime curvature. Dimensional analysis says no product of powers of these three, except the trivial one, can be dimensionless. The Recognition Science framework's machine-checked library of formal theorems proves this fact in the declaration native_dimensional_boundary_cert, which packages three results: the dimension matrix has nonzero determinant, no nontrivial monomial in c, ℏ, and G is dimensionless, and the bridge from native units to SI units is a calibration map, not a prediction.

The practical consequence is sharp. The framework can derive dimensionless relations among native constants, such as ℏ = φ⁻⁵ and G·ℏ = 1/π, where φ is the golden ratio. But it cannot, from pure dimensionless data alone, output the absolute SI value of ℏ or G. The certificate proves this impossibility: because the three dimension vectors are linearly independent, any attempt to form a dimensionless combination from c, ℏ, and G collapses to the trivial all-zero case. A dimensional anchor, one measured quantity with SI units, is therefore required before any native constant can be expressed in kilograms, meters, or seconds.

The certificate also proves that one anchor suffices. The bridge function from a supplied positive value of G to the squared tick scale, the native unit of time, is injective: different anchors give different scales, and every positive anchor gives a positive scale. This is the honest boundary. The framework's library elsewhere shows that a single scalar anchor, the tick time τ₀ in seconds, determines the entire conversion, yielding the electron mass in kilograms with zero hypotheses or external inputs beyond that one measurement.

In Recognition Science, this boundary is not a weakness but a feature of dimensional analysis itself. The certificate's value is precision about what the framework claims: it forces dimensionless structure from first principles, and it forces the shape of the calibration once an anchor is supplied, but it does not predict the anchor. A reader should take away a clear picture: the framework's native constants are first-principles objects only up to this dimensional boundary, and SI conversion is a uniquely constrained calibration, not a free parameter and not a derivation from nothing.

/-- Native constants are first-principles objects only up to the dimensional
boundary; SI conversion is a uniquely constrained calibration once an anchor is
supplied. -/
theorem native_dimensional_boundary_cert : NativeDimensionalBoundaryCert where
  determinant_nonzero := dimension_matrix_c_hbar_G_det_nonzero
  no_dimensionless_monomial := fun h => no_nontrivial_dimensionless_monomial h
  bridge_calibrates := si_bridge_is_calibration_not_prediction

/-- 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 certificate does not prove that the framework derives the absolute SI value of ℏ or G from pure theory. The certificate does not claim that the dimensional anchor is predicted by the framework; it is supplied as input. The certificate does not address the physical interpretation of the tick scale or its relation to conventional time units beyond the algebraic bridge.

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: