`MassDisplayCalibration`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.NeutrinoSector
domain: Physics
line: 70 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.NeutrinoSector on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  67def rung_nu2 : ℤ := -58
  68
  69/-- Explicit reporting seam for converting the RS structural mass scale to eV. -/
  70structure MassDisplayCalibration where
  71  eV_per_structural_unit : ℝ
  72  eV_per_structural_unit_pos : 0 < eV_per_structural_unit
  73
  74/-- Legacy display convention: treat `electron_structural_mass` as MeV and convert to eV. -/
  75def legacy_mass_display_calibration : MassDisplayCalibration where
  76  eV_per_structural_unit := 1e6
  77  eV_per_structural_unit_pos := by norm_num
  78
  79/-- SI-backed display seam from an RS external calibration object.
  80    This maps coherence quanta to eV through Joules and the elementary charge. -/
  81noncomputable def mass_display_calibration_of_external
  82    (cal : Constants.RSNativeUnits.ExternalCalibration) : MassDisplayCalibration where
  83  eV_per_structural_unit := cal.joules_per_coh / Constants.ExternalAnchors.e_SI
  84  eV_per_structural_unit_pos := by
  85    have hcal : 0 < cal.joules_per_coh := cal.joules_pos
  86    have he : 0 < Constants.ExternalAnchors.e_SI := by
  87      norm_num [Constants.ExternalAnchors.e_SI]
  88    exact div_pos hcal he
  89
  90/-- Backwards-compatible alias for old code paths. -/
  91def MeV_to_eV : ℝ := legacy_mass_display_calibration.eV_per_structural_unit
  92
  93/-- Predicted Mass (eV). -/
  94noncomputable def predicted_mass_eV_with
  95    (cal : MassDisplayCalibration) (rung : ℤ) : ℝ :=
  96  electron_structural_mass * (phi ^ rung) * cal.eV_per_structural_unit
  97
  98/-- Default predicted mass in eV (legacy convention). -/
  99noncomputable def predicted_mass_eV (rung : ℤ) : ℝ :=
 100  predicted_mass_eV_with legacy_mass_display_calibration rung

papers checked against this theorem

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