pith. sign in
module module high

IndisputableMonolith.Measurement.RSNative.Core

show as:
view Lean formalization →

The RSNative.Core module defines the measurement protocol for extracting RS observables from states or traces in native units. Alignment and calibration modules cite it to enforce consistent extraction before cross-agent comparison or SI reporting. The module consists of definitions for Protocol, Measurement, Status, Uncertainty, and related types with no proofs.

claimA measurement protocol extracts an observable $O$ from a state or trace $s$ via a map in RS-native units with time quantum $τ_0 = 1$ tick.

background

This module resides in the Measurement domain and supplies the foundational protocol for RS observables. It imports Constants, which fixes the RS time quantum $τ_0 = 1$ tick. Sibling definitions include Protocol, Measurement, Status, Window, Uncertainty, sigmaVal, intervalBounds, and hygienic utilities that encode extraction rules and error bounds.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the Alignment module, which records protocol-level invariants for cross-agent comparison without solving qualia issues; the SI Calibration adapter, which enforces separation from CODATA numerals; and the SingleAnchor module, which supplies concrete calibration without fit parameters. It establishes the explicit data seam required by the Recognition Science measurement framework.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (41)