pith. sign in
module module high

IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor

show as:
view Lean formalization →

This module supplies a single-anchor SI calibration for RS-native quantities by fixing the speed of light at its exact definitional value. It defines c_SI, h_SI, tau0_seconds_protocol, CalibrationCert, and the calibration function together with hygienic variants. Measurement researchers converting tick-based RS results to laboratory units cite it to keep core theory free of CODATA numerals. The module consists entirely of definitions and positivity assertions with no theorems.

claimThe module fixes $c = 299792458$ m/s exactly and supplies the record CalibrationCert together with the map calibration that converts RS-native observables (ticks, voxels) to SI units via the supplied external anchor.

background

Recognition Science uses a native measurement scaffold with base units ticks, voxels, coherence and action, setting τ₀ = 1 inside the core. The Core module keeps all theory RS-native while routing SI reporting through an explicit ExternalCalibration record supplied from outside. The SI adapter module enforces the seam: core catalogs never embed CODATA numerals; conversion occurs only via the supplied record. Constants.RSNativeUnits defines the ledger primitives as the fundamental standards. SingleAnchor implements one concrete realization of that adapter by anchoring to the exact SI definition of c.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies CalibrationCert and the calibration function that the RS-Native → SI Calibration Adapter requires for explicit external anchoring. It thereby enables tau0_seconds_protocol and externalCalibration_of_tau0_seconds while preserving the separation between native theory and laboratory reporting demanded by the Core and Constants modules.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)