pith. sign in
module module moderate

IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor

show as:
view Lean formalization →

The SingleAnchor module supplies the exact SI-definitional speed of light in meters per second as an anchor for RS-native to SI reporting. Researchers performing explicit calibrations between ledger-based units and laboratory standards would cite it to keep core theory free of CODATA numerals. It consists of definitions plus positivity statements with no deeper proof structure.

claim$c_{\rm SI} = 299792458$ (exact, in m/s) together with the associated positivity and calibration records that convert RS-native quantities via an external record.

background

The module imports three upstream packages. RSNativeUnits defines a Recognition-Science-native unit system that treats the ledger primitives as the base standards; all physics can be expressed in these units without reference to SI. The SI module is the explicit seam where RS-native quantities can be reported in SI, with the rule that RS-native theory must not depend on CODATA numerals and that conversion occurs only through an explicit ExternalCalibration record. Core supplies the Lean-first measurement scaffold with ticks/voxels/coh/act, $\tau_0=1$, and the requirement that SI remains optional calibration outside the core.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the constants referenced by CalibrationCert and calibration in the same file, which in turn feed the external calibration mechanism used by downstream RS measurement protocols. It closes the single-anchor seam required by the SI adapter without violating the separation of core theory from calibration data.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)