IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor
The SingleAnchor module supplies SI calibration definitions for RS-native constants using a single anchor, specifically the exact speed of light. Measurement researchers in Recognition Science cite it to bridge native tick/voxel units to SI reporting. It is a definitions-only module with no theorems or proofs.
claim$c_{\rm SI} = 299792458$ m s$^{-1}$ (exact).
background
This module operates within the RS-native measurement system. The Core module establishes a Lean-first scaffold with RS-native primitives (ticks, voxels, coh, act) and $\tau_0 = 1$, keeping SI as optional external calibration. The SI module provides the adapter seam where RS quantities are reported in SI via explicit ExternalCalibration records, without embedding CODATA numerals in the core theory.
The RSNativeUnits module defines the fundamental base units from ledger primitives, enabling all physics in native units. SingleAnchor extends this by providing concrete single-anchor calibrations anchored on the SI-definitional speed of light.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the calibration layer that enables the external calibration protocol in the broader RS framework. It directly supports the design goal in the Core module of keeping SI optional and explicit. It implements the seam described in the SI calibration module, allowing RS quantities to be reported in SI without depending on CODATA in the core theory.
scope and limits
- Does not embed CODATA numerals in core RS theory.
- Does not alter the native tick/voxel measurement scaffold.
- Does not provide multi-anchor calibrations.
depends on (3)
declarations in this module (15)
-
def
c_SI -
lemma
c_SI_pos -
def
h_SI -
lemma
h_SI_pos -
def
hbar_SI -
lemma
hbar_SI_pos -
def
tau0_seconds_protocol -
theorem
tau0_seconds_protocol_hygienic -
def
externalCalibration_of_tau0_seconds -
structure
CalibrationCert -
def
calibration -
theorem
calibration_protocol_hygienic -
theorem
c_reports_exact -
theorem
one_act_reports_hbar -
def
mkCert