pith. sign in
module module high

IndisputableMonolith.Constants.ExternalAnchors

show as:
view Lean formalization →

The ExternalAnchors module supplies SI-unit values for fundamental constants together with an ExternalAnchorMarker type that flags calibration dependence. Neutrino mass derivations and thermodynamic calculations in the Recognition framework reference these anchors to link native phi-ladder units to laboratory data. The module contains only definitions and documentation markers with no theorems or proofs.

claimThe module declares the marker type $ExternalAnchorMarker$ and the constants $c_{SI}$, $hbar_{SI}$, $h_{SI}$, $e_{SI}$, $kB_{SI}$, $NA_{SI}$, $G_{SI}$, $G_{SI uncertainty}$, $alpha_{CODATA}$, $alpha_{CODATA uncertainty}$, and $alpha^{-1}_{CODATA}$.

background

Recognition Science works in native units where $c=1$, $hbar=phi^{-5}$, and $G=phi^5/pi$, with the Recognition Composition Law and the eight-tick octave fixing the structure. External anchors supply measured SI values to calibrate results that depend on experiment rather than pure derivation from the J-cost equation. The module documentation states that the marker type signals calibration dependence without altering code semantics.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies calibration points used by the NeutrinoSector module for T14 neutrino mass scales on the deep ladder and by the thermodynamics modules for chemical potential from J-cost gradients, heat capacity from 8-tick mode counting, and phase transitions from J-cost bifurcations. It anchors the framework to CODATA values while preserving internal consistency with the phi-ladder and D=3.

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)