pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.RSNativeUnits

show as:
view Lean formalization →

RSNativeUnits establishes the native unit system for Recognition Science, defining time in ticks with τ₀ equal to one tick and c set to 1, along with derived dimensions. Calibration adapters and neutrino mass derivations cite it to keep all calculations in RS-native form before any external conversion. The module consists of a collection of sibling definitions for Time, Length, Velocity, Energy, Action, Mass, Frequency, Momentum, Charge, tick, voxel, and c, importing core constants and display kernels with no theorems.

claimIn RS-native units the fundamental time quantum satisfies $τ_0 = 1$ tick with $c = 1$, length measured in voxels, and all other quantities (energy, mass, momentum, charge, frequency, action) derived directly from these without external numerals.

background

Recognition Science runs all theory in a native unit system anchored on the tick as the indivisible time quantum. The upstream Constants module states that τ₀ = 1 tick is the fundamental RS time quantum. KDisplayCore supplies the clock-side display relation τ_rec(display) = (2π · τ₀) / (8 ln φ). This module collects the basic dimensional definitions (Time, Length, Velocity, Energy, Action, Mass, Frequency, Momentum, Charge) together with the primitives tick, voxel, and c.

proof idea

This is a definition module, no proofs. It organizes content as a flat collection of sibling definitions, each importing the necessary constants from Constants and KDisplayCore without any theorem statements or tactics.

why it matters in Recognition Science

The module supplies the unit foundation required by downstream calibration adapters in Measurement.RSNative.Calibration.SI and SingleAnchor, which convert RS-native results to SI only through explicit external records. It also supports Physics.NeutrinoSector for neutrino mass derivations on the deep ladder. It implements the native units consistent with the T0-T8 forcing chain and the Recognition Composition Law.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (64)