pith. machine review for the scientific record. sign in
def definition def or abbrev high

calibration

show as:
view Lean formalization →

This definition produces the external calibration structure from a certificate supplying the single empirical time anchor tau zero in seconds. Researchers converting RS-native tick, voxel, and coherence quantities into SI units for reporting would cite it when a single-anchor seam is required. The body is a direct one-line application of the external calibration constructor to the certificate value and its positivity witness.

claimLet cert be a calibration certificate containing a positive real measurement tau_0 in seconds that satisfies the single-anchor protocol. Then calibration(cert) is the external calibration structure whose seconds-per-tick field equals tau_0, whose meters-per-voxel field is fixed by the exact SI definition of the speed of light, and whose joules-per-coherence field is fixed by the exact SI definition of Planck's constant together with the RS identity that one action equals one coherence times one tick.

background

The module implements a single-anchor SI calibration protocol for the RS-native framework. In RS-native units the theory runs in ticks, voxels, coherences, and actions with c equal to 1 and no SI numerals. To obtain SI reporting one supplies only the scalar tau_0 in seconds; meters per voxel follows from the SI definition of c and joules per coherence follows from the SI definition of h together with the identity 1 act = 1 coh times 1 tick. A CalibrationCert bundles the measured tau_0 as a Measurement real, a proof that the protocol is the canonical single-anchor protocol, and a positivity witness 0 less than tau_0.value. The target ExternalCalibration is the structure with fields seconds_per_tick, meters_per_voxel, and joules_per_coh.

proof idea

The definition is a one-line wrapper that applies externalCalibration_of_tau0_seconds to the value and positivity proof extracted from the input certificate.

why it matters in Recognition Science

This definition supplies the concrete mapping required for SI reporting of RS-native results and is invoked in downstream derivations of constants such as tau0_pos, E_coh_pos, thermal energy at unit temperature, and the canonical cost algebra that uses the J-cost function. It realizes the single-anchor protocol of the module, ensuring that only one empirical scalar enters the conversion while the remainder follows from SI definitions of c and h. It closes the measurement seam for the phi-ladder mass formulas and alpha bounds without introducing free parameters.

scope and limits

formal statement (Lean)

 130noncomputable def calibration (cert : CalibrationCert) : ExternalCalibration :=

proof body

Definition body.

 131  externalCalibration_of_tau0_seconds cert.tau0_seconds.value cert.tau0_pos
 132

used by (40)

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

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.