pith. machine review for the scientific record. sign in
def definition def or abbrev high

e_SI

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

Lean usage

cal.joules_per_coh / Constants.ExternalAnchors.e_SI

formal statement (Lean)

  82@[simp]
  83noncomputable def e_SI : ℝ := 1.602176634e-19

proof body

Definition body.

  84
  85/-- **EXTERNAL ANCHOR**: Boltzmann constant (exact, SI 2019 definition).
  86    k_B = 1.380649 × 10⁻²³ J/K -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.