pith. sign in
module module high

IndisputableMonolith.Measurement.RSNative.Core

show as:
view Lean formalization →

This module establishes the core definitions for RS-native measurement protocols, specifying how observables are extracted from states or traces in tick-based units. Physicists building calibration layers or alignment protocols would cite it as the entry point for the measurement domain. It consists entirely of type declarations and helper functions with no theorem proofs.

claimThe module introduces types for Protocol (extraction rule from state/trace to observable), Measurement (recorded value with uncertainty), Status, Window, and Uncertainty, together with functions map and intervalBounds, all expressed in RS-native units with time quantum τ₀ = 1 tick.

background

Recognition Science runs in native units where the fundamental time quantum τ₀ equals one tick, supplied by the imported Constants module. This core module defines the Protocol type for extraction rules, the Measurement type for results, and supporting structures such as Status, hygienic checks, sigmaVal, and intervalBounds to record observables with controlled uncertainty. The local setting is the Measurement domain, which isolates observable extraction from both the underlying forcing chain and any external SI numerals.

proof idea

This is a definition module with no proofs; it declares types and functions for protocols, measurements, and uncertainty handling.

why it matters in Recognition Science

The module supplies the foundational measurement abstractions that downstream modules rely on. Alignment uses it to define explicit protocol seams for cross-agent comparison while recording invariants. Calibration.SI and Calibration.SingleAnchor import it to enforce that RS-native theory remains independent of CODATA values and that SI reporting occurs only through externally supplied calibration records. It thereby supports the framework separation between native theory (T0–T8, RCL) and measurement reporting.

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)