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

ExternalAnchorMarker

show as:
view Lean formalization →

The ExternalAnchorMarker introduces a unit type to tag definitions that incorporate external empirical constants such as CODATA values. Researchers comparing RS-native derivations against measured data would cite it to identify calibration seams. The implementation is a one-line abbreviation to the unit type that carries no computational content.

claimLet $M$ denote the unit type used to mark declarations that depend on external empirical calibration data such as the CODATA 2022 values for fundamental constants.

background

This module serves as the single quarantined location for all empirical calibration data that enters Recognition Science from external sources. Its policy enforces that the cost-first core, built solely on the Recognition Composition Law, never imports this module, while any importing module explicitly acknowledges its use of external anchors. Upstream structures supply the relevant primitives: nuclear density tiers on the phi-ladder, the abstract CPM constants bundle, the J-cost factorization from the Ledger, and the spectral emergence of gauge content and fermion generations.

proof idea

The declaration is a one-line abbreviation directly to the unit type.

why it matters in Recognition Science

The marker implements the mechanical separation between pure RCL derivations and experimental comparison, supporting the listing of SI 2019 exact values for c, hbar, G and the alpha band. It aligns with the forcing chain landmarks that fix D = 3 and the eight-tick octave while leaving open the precise numerical matching between RS-native units and measured constants.

scope and limits

formal statement (Lean)

  53abbrev ExternalAnchorMarker := Unit

proof body

Definition body.

  54
  55/-! ## CODATA 2022 Fundamental Constants
  56
  57**EXTERNAL ANCHOR SECTION**
  58
  59These are the official CODATA 2022 values. The SI 2019 redefinition makes
  60several of these exact by definition.
  61-/
  62
  63section CODATAFundamental
  64
  65/-- **EXTERNAL ANCHOR**: Speed of light in vacuum (exact, SI 2019 definition).
  66    c = 299792458 m/s -/

depends on (7)

Lean names referenced from this declaration's body.