`mkCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor
domain: Measurement
line: 164 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor on GitHub at line 164.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 161
 162This is a helper for downstream modules; real usage should supply a `Protocol`d
 163measurement record coming from a declared empirical procedure. -/
 164def mkCert (tau0_s : ℝ) (htau : 0 < tau0_s) : CalibrationCert :=
 165  { tau0_seconds :=
 166      { value := tau0_s
 167        protocol := tau0_seconds_protocol
 168        notes := ["Units: SI seconds per RS tick (single-anchor calibration seam)."] }
 169    protocol_ok := rfl
 170    tau0_pos := htau
 171  }
 172
 173end
 174
 175end SingleAnchor
 176end Calibration
 177end RSNative
 178end Measurement
 179end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.