Pith. sign in
module module high

IndisputableMonolith.Constants.ExternalAnchors

show as:
view Lean formalization →

Central registry of SI and CODATA numerical anchors (c, ħ, e, k_B, N_A, G, α) used only for external calibration and comparison. Downstream quarantine and cosmology modules import it so measured values never enter pure RS derivations. The module is pure definitions plus a documentation marker type; no theorems are proved here.

claimFixed external constants in SI units: speed of light $c$, reduced Planck constant $\hbar$, elementary charge $e$, Boltzmann constant $k_B$, Avogadro number $N_A$, Newtonian $G$ (with uncertainty), and CODATA fine-structure value $\alpha$ (with uncertainty and $\alpha^{-1}$). An $\mathrm{ExternalAnchor}$ marker tags any definition that depends on these measured inputs.

background

Recognition Science works in RS-native units where $c = 1$, $\hbar = \varphi^{-5}$, and $G = \varphi^5/\pi$, with $\alpha^{-1}$ predicted inside a narrow band near 137.03. Experimental comparison still requires the conventional SI/CODATA numbers. This module isolates those numbers so that pure derivation modules never see them.

The sibling definitions are plain Float/ℝ literals for $c$, $\hbar$, $h$, $e$, $k_B$, $N_A$, $G$ (plus $G$ uncertainty), and the CODATA $\alpha$ triple. ExternalAnchorMarker is a documentation-only type: it does not change computation, but flags calibration dependence for auditors.

Import graph is deliberately one-way. Alpha Genesis M1–M3 stay blind to CODATA; only quarantined comparison modules and selected cosmology/physics tracks pull these anchors.

proof idea

This is a definition module: no proofs, no sorry, no hypotheses. It declares SI/CODATA numeric constants and the ExternalAnchorMarker type. Downstream modules import the values when they need a measured comparison target.

why it matters in Recognition Science

Keeps measured constants out of the forcing chain and mass-ladder core while still enabling decisive external checks. Feeds the quarantined Alpha Genesis modules MeasurementVerdict and ResidualTarget (the only Alpha Genesis sites allowed to see CODATA). Cosmology modules OmegaLambdaDerivation, PhaseSaturationVacuum, and VacuumFluctuationStructural use $\alpha$ when stating $\Omega_\Lambda = 11/16 - \alpha/\pi$ against the observed dark-energy band. NeutrinoSector, PhaseTransitions, and AlphaCorrectionAnalysis likewise import anchors for scale or residual comparisons. Without this isolation layer, CODATA would leak into the pure RS derivation path.

scope and limits

used by (10)

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

declarations in this module (36)