AlignmentMap
plain-language theorem explainer
AlignmentMap supplies the function type for mapping measurement values from one agent's coordinate system to another's in the cross-agent alignment scaffold. Researchers constructing packaged alignments for RS-native measurement consistency would reference it when combining the map with protocol invariants. The declaration is a direct type abbreviation with no computational content or proof steps.
Claim. An alignment map from coordinate system $α$ to coordinate system $β$ is any function $α → β$.
background
The module sets up a scaffold for comparing measurements across agents by requiring explicit data: a map together with a protocol, plus invariants that keep comparisons meaningful. It explicitly avoids qualia or ethics issues. Upstream, Core.map applies a function to a Measurement while carrying over window, protocol, uncertainty, and notes unchanged.
proof idea
This is a direct type abbreviation with no lemmas applied and no tactics.
why it matters
It supplies the map field for the downstream Alignment structure, which packages the map with AlignmentProtocol to realize the protocol-level seam for cross-agent comparisons. The definition supports the explicit-data approach described in the module for the Measurement domain within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.