pith. sign in
module module high

IndisputableMonolith.Measurement.RSNative.Calibration.SI

show as:
view Lean formalization →

This module supplies SI conversion functions for RS-native action quanta (act) to joule-seconds. Researchers anchoring Recognition Science observables to laboratory units would cite it. It implements the conversion as the product of joules per coh and seconds per tick, using definitions imported from RSNativeUnits and Core.

claimThe module defines maps such as $to_joule_seconds(a) = a · (joules_per_coh × seconds_per_tick)$ that convert a number $a$ of action quanta to SI $J·s$, where one act equals one coh times one tick.

background

The module sits inside the RS-native measurement scaffold of Core, which treats ticks, voxels, coh, and act as base standards with $τ_0 = 1$ and $c = 1$. SI/CODATA values appear only as optional external calibration. It imports the ledger-primitive unit system from Constants.RSNativeUnits, whose doc-comment states that all physics can be expressed in these units without reference to SI.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the concrete conversion layer required by the downstream Single-Anchor SI Calibration module, which provides a single-anchor protocol for reporting RS-native measurements in SI without fit parameters. It completes the optional calibration step that keeps core theory (ticks/voxels/coh/act) independent of external units.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)