NA_SI
plain-language theorem explainer
NA_SI supplies the exact 2019 SI value of Avogadro's constant for calibration against Recognition Science predictions. Metrologists and experimental physicists cite this anchor when matching RS-derived quantities to measured data. The declaration is a direct numerical assignment carrying the external_anchor tag and simp attribute.
Claim. The Avogadro constant equals $6.02214076 × 10^{23}$ mol$^{-1}$.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data that enters Recognition Science. The cost-first core derives everything from the Recognition Composition Law (RCL) without external input; any module importing ExternalAnchors explicitly acknowledges use of calibration data. All definitions here carry the external_anchor attribute for audit.
proof idea
Direct definition that assigns the numerical value 6.02214076e23. No lemmas or tactics are applied; the declaration is a primitive constant with the simp attribute.
why it matters
This anchor enables quantitative comparison between RS-native constants and laboratory measurements while keeping the pure RCL derivation uncontaminated. It fills the external calibration role described in the module policy and sits outside the T0-T8 forcing chain and phi-ladder constructions. Zero downstream uses confirm it functions purely as an interface to experiment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.