pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.ExternalAnchors

show as:
view Lean formalization →

The ExternalAnchors module declares a marker type and SI-unit values for fundamental constants to flag calibration dependence in Recognition Science. It is imported by the neutrino mass scale derivation and by thermodynamic modules on chemical potential, heat capacity, and phase transitions. As a definition module it contains no proofs, only declarations that tie RS-native units to external data.

claimMarker type $E$ for external anchors together with SI constants $c_{SI}$, $h_{SI}$, $G_{SI}$, $k_B$, $N_A$, and CODATA values for $1/alpha$ with uncertainties.

background

This module belongs to the Constants domain and supplies the ExternalAnchorMarker type whose sole purpose is to signal that a declaration depends on external calibration data. It lists concrete SI values for the speed of light, Planck constants, gravitational constant, Boltzmann constant, Avogadro number, and the CODATA fine-structure constant together with their reported uncertainties. These anchors allow later modules to match the RS-native relations (c = 1, hbar = phi^{-5}, G = phi^5 / pi) against laboratory measurements.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the calibration points required by the neutrino sector (T14) and by the thermodynamic results on chemical potential from J-cost gradients (THERMO-007), heat capacity from 8-tick mode counting (THERMO-004), and phase transitions from J-cost bifurcations (THERMO-006). It therefore closes the interface between the phi-ladder constants and measured SI quantities.

scope and limits

used by (4)

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

declarations in this module (36)