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

tau0_seconds_protocol

show as:
view Lean formalization →

Defines the single-anchor SI calibration protocol by supplying only τ₀ in seconds per RS tick as the empirical input. Researchers reporting RS-native predictions in SI units cite this definition to fix the reporting scale without introducing fit parameters or tuning dimensionless quantities. The definition directly constructs a Protocol record with name, summary, hypothesis status, two assumptions on measurement stability, and two falsifiers for consistency checks.

claimThe single-anchor SI calibration protocol is the Protocol record that accepts one empirical scalar τ₀ (seconds per RS tick) and derives meters_per_voxel from the SI definition of c = 299792458 m/s together with joules_per_coh from the SI definition of h (hence ħ = h/(2π)) and the RS identity 1 act = 1 coh × 1 tick.

background

RS-native theory runs in tick/voxel/coh/act units with c = 1 and no SI numerals. The module supplies a concrete single-anchor calibration seam: the sole empirical scalar is τ₀ (seconds per tick). Meters per voxel follows from the exact SI definition of c; joules per coh follows from the exact SI h together with the RS identity act = coh · tick. Upstream, the fundamental tick is defined as 1 in RS-native units (Constants.tick) and ħ is set to φ^{-5} in those units (Constants.hbar). The protocol is marked hypothesis because τ₀ is treated as measured input rather than derived.

proof idea

The definition constructs the Protocol record inline. It sets the name field to the calibration identifier, the summary to the single-anchor derivation description, status to hypothesis, assumptions to the two listed conditions on τ₀ stability and SI definitional constants, and falsifiers to the two consistency checks on independent anchors and speed consistency.

why it matters in Recognition Science

This definition supplies the protocol used by CalibrationCert and mkCert to bundle a measured τ₀ with the derived ExternalCalibration. It implements the explicit seam described in the module documentation, ensuring no dimensionless RS predictions receive fit freedom. It connects to the RS-native constants where tick and ħ are defined and supports the overall measurement framework for SI reporting. The parent structure CalibrationCert depends on it directly.

scope and limits

formal statement (Lean)

  76def tau0_seconds_protocol : Protocol :=

proof body

Definition body.

  77  { name := "calibration.single_anchor.tau0_seconds"
  78    summary :=
  79      "Single-anchor SI calibration. Supply τ0 (seconds per tick) as the only empirical scalar. " ++
  80      "Derive meters_per_voxel via SI-defined c=299792458 and derive joules_per_coh via SI-defined h (hbar=h/(2π)) " ++
  81      "together with RS identity 1 act = 1 coh * 1 tick. No mass-data fitting; this is a reporting seam only."
  82    status := .hypothesis
  83    assumptions :=
  84      [ "A1: τ0 (one RS tick) corresponds to a stable physical duration that can be measured in SI seconds using a declared lab protocol."
  85      , "A2: SI definitional constants (c and h) are treated as exact conventions; they introduce no fit freedom."
  86      ]
  87    falsifiers :=
  88      [ "F1: Two independent anchors for τ0 (e.g. time-first vs length-first) disagree beyond stated uncertainties."
  89      , "F2: Under the derived calibration, the SI speed consistency check fails beyond uncertainty."
  90      ]
  91  }
  92

used by (3)

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

depends on (30)

Lean names referenced from this declaration's body.