pith. sign in
module module high

IndisputableMonolith.Constants.RSNativeUnits

show as:
view Lean formalization →

RSNativeUnits establishes the base RS-native unit system with the tick as fundamental time quantum and c=1. Researchers deriving quantities from the forcing chain or expressing constants like ħ = φ^{-5} would cite these definitions to keep all work in tick/voxel units. The module consists entirely of definitions for Time, Length, Velocity, Energy, Action, Mass, Frequency, Momentum, Charge, tick, voxel, and c.

claimThe RS-native units are defined with fundamental time quantum $\tau_0 = 1$ tick, $c = 1$, length in voxels, and derived quantities for energy, action, mass, and charge, consistent with the Recognition Composition Law and the eight-tick octave.

background

The module imports Constants, where the fundamental RS time quantum satisfies $\tau_0 = 1$ tick. It also imports KDisplayCore, whose clock-side display definition is $\tau_{rec}(display) = (2\pi \cdot \tau_0) / (8 \ln \phi)$, and Alpha for the fine-structure constant band.

This supplies the notational foundation for the Recognition Science framework in which all physics is expressed without external numerals. Sibling definitions cover the full set of base quantities (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

why it matters in Recognition Science

This module supplies the unit definitions that feed the SI calibration adapters (IndisputableMonolith.Measurement.RSNative.Calibration.SI and SingleAnchor) and the neutrino sector derivation. It implements the base layer for expressing constants such as $\hbar = \phi^{-5}$ and $G = \phi^5 / \pi$ in native units, closing the seam between theory and measurement reporting while preserving the T0-T8 forcing chain and RCL.

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)