module module

`IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.RSNativeUnits module_import
IndisputableMonolith.Measurement.RSNative.Calibration.SI module_import
IndisputableMonolith.Measurement.RSNative.Core module_import

declarations in this module (15)

def c_SI L41
lemma c_SI_pos L43
def h_SI L49
lemma h_SI_pos L52
def hbar_SI L60
lemma hbar_SI_pos L63
def tau0_seconds_protocol L76
theorem tau0_seconds_protocol_hygienic L93
def externalCalibration_of_tau0_seconds L99
structure CalibrationCert L121
def calibration L130
theorem calibration_protocol_hygienic L133
theorem c_reports_exact L140
theorem one_act_reports_hbar L149
def mkCert L164