ExternalAnchorMarker
plain-language theorem explainer
ExternalAnchorMarker is defined as the unit type to flag declarations that incorporate external empirical calibration data such as CODATA values. Researchers comparing Recognition Science predictions against measured constants reference this marker to preserve separation between pure derivations and calibration inputs. The implementation is a direct type alias to Unit that carries no data or computational semantics.
Claim. Let $M$ be the unit type used to mark declarations that depend on external calibration data rather than pure Recognition Science derivation from the Recognition Composition Law.
background
This module serves as the single quarantined location for all empirical calibration data that enters Recognition Science from external sources. The cost-first core derives every quantity from the Recognition Composition Law without external input, so this module is mechanically isolated to enable comparison with experiment while keeping the core uncontaminated. Definitions here receive the external_anchor attribute for automated audit.
proof idea
The declaration is a one-line abbreviation that sets ExternalAnchorMarker equal to the unit type Unit, providing a type-level documentation signal with no proof obligations.
why it matters
The marker supports the explicit policy that the cost-first core must never import this module, thereby maintaining a clean separation between RCL-based derivations and empirical anchors such as CODATA 2022 values. It enables downstream modules to acknowledge calibration dependence without affecting the pure theoretical structures such as J-cost minimization or spectral emergence. No parent theorems or downstream uses are recorded because the declaration functions solely as a passive documentation device.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.