mass_display_calibration_of_external
plain-language theorem explainer
This definition builds an SI-backed display seam that converts RS coherence quanta to eV by dividing the joules-per-coherence value from an ExternalCalibration object by the elementary charge. Neutrino mass modelers in the Recognition framework cite it when reporting structural masses on the deep ladder in observable units. The construction is a direct field assignment whose only non-trivial content is a one-line positivity argument via division of positives.
Claim. Given an external calibration object $cal$ supplying joules per coherence quantum, the display calibration is the structure whose eV-per-structural-unit field equals (joules per coherence quantum) divided by the elementary charge $e$, with the positivity condition $0 < $ that ratio.
background
MassDisplayCalibration is the explicit reporting seam that converts the dimensionless RS structural mass scale into electron-volts. Its two fields are the conversion factor eV_per_structural_unit together with the proof obligation that the factor is positive. ExternalCalibration supplies the three RS-to-SI anchors (seconds per tick, meters per voxel, joules per coherence quantum) that appear in the definition. The module T14 places neutrinos on the deep ladder with rungs near -54 and -58; the present definition supplies the SI/eV reporting path that replaces the legacy MeV-based convention noted in the module doc-comment.
proof idea
The definition is a direct field assignment for eV_per_structural_unit. The accompanying positivity proof applies div_pos to the two hypotheses cal.joules_pos and the norm_num fact that e_SI is positive.
why it matters
The definition closes the SI reporting seam required by the neutrino mass formulas in the same module. It sits downstream of ExternalCalibration and e_SI, and upstream of any concrete mass_display use that must output eV values. Within the Recognition framework it implements the calibration note in the T14 module doc-comment, ensuring that deep-ladder predictions remain comparable to oscillation data without introducing new parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.