pith. sign in
module module high

IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor

show as:
view Lean formalization →

This module supplies exact SI values for RS-native constants (c, h, hbar, tau0) and the single-anchor calibration record that maps RS units to SI without embedding CODATA numerals in core theory. Measurement and calibration authors cite it when reporting RS predictions in laboratory units. It consists entirely of definitions and positivity lemmas.

claimThe module defines $c_{ m SI}=299792458$ (exact, m/s), $h_{ m SI}$, $ar h_{ m SI}$, the protocol $ au_0$ seconds, and the record $\text{ExternalCalibration}$ that anchors RS-native quantities to SI via a single constant.

background

The parent modules establish an RS-native unit system whose base standards are ticks, voxels, coherence, and action with $\tau_0=1$ (RSNativeUnits), an explicit seam that keeps all SI conversion outside core theory via an ExternalCalibration record (SI), and a Lean-first scaffold that treats SI/CODATA as optional calibration only (Core). SingleAnchor supplies the concrete SI numerals and the hygienic protocol that realizes the single-anchor case of that seam.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the CalibrationCert and calibration_protocol_hygienic objects that appear among its siblings. It supplies the concrete SI anchor required by the RSNativeUnits and SI modules so that downstream measurement statements can be reported in laboratory units while preserving the separation between RS-native theory and external calibration.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)