def definition def or abbrev

`to_joule_seconds`

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

formal statement (Lean)

  39@[simp] noncomputable def to_joule_seconds (cal : ExternalCalibration) (A : Act) : ℝ :=

Definition body.

  40  (A : ℝ) * (cal.joules_per_coh * cal.seconds_per_tick)
  41
  42/-! ## Measurement-level conversion helpers -/
  43

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

measure_to_joule_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
one_act_reports_hbar in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use

Lean names referenced from this declaration's body.

ExternalCalibration in IndisputableMonolith.Constants.RSNativeUnits decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Act in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use