e_SI
plain-language theorem explainer
The e_SI definition supplies the exact 2019 SI value of the elementary charge for external calibration. Researchers mapping Recognition Science structural masses to electron-volts cite it when converting coherence quanta in the neutrino sector. It is implemented as a direct numerical assignment with the simp attribute for rewriting.
Claim. The elementary charge is defined by the exact SI 2019 value $e = 1.602176634 × 10^{-19}$ coulombs.
background
This module serves as the single quarantined location for all empirical calibration data entering Recognition Science from external sources, per the module documentation. The cost-first core derives everything from the Recognition Composition Law and must not import this module; any importing module explicitly acknowledges use of external data. Similar anchors appear upstream, such as the Boltzmann constant $k_B = 1.380649 × 10^{-23}$ J/K in information and quantum modules, and the dimensionless bridge ratio $K = ϕ^{1/2}$.
proof idea
Direct definition assigning the CODATA 2019 exact numerical value, marked with the simp attribute for automatic rewriting in downstream expressions.
why it matters
It supplies the calibration seam that converts RS-native structural units to SI observables, feeding directly into the mass_display_calibration_of_external definition in the neutrino sector. This enables comparison of the phi-ladder mass formula against experiment while preserving isolation of the pure cost derivation from the forcing chain (T0-T8) and RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.