AlignmentMap
plain-language theorem explainer
AlignmentMap is the function type between coordinate systems of distinct agents. Researchers comparing measurements across agents cite it when building explicit alignment data. The declaration is a direct type abbreviation with no computational content or proof obligations.
Claim. An alignment map from coordinate system $α$ to coordinate system $β$ is any function $α → β$.
background
The module sets up a scaffold for cross-agent alignment of measurements. It treats alignment as explicit data consisting of a map plus protocol, without resolving qualia or ethics comparability. AlignmentMap supplies the map component. The upstream Core.map definition applies a function to a measurement value while preserving window, protocol, uncertainty, and notes. The three A declarations supply active edge counts and the actualization operator from their respective modules.
proof idea
One-line type abbreviation that equates AlignmentMap α β directly to the arrow type α → β.
why it matters
It supplies the map field inside the downstream Alignment structure. The structure packages this map with an AlignmentProtocol to realize the module's protocol-level seam for cross-agent measurement comparison. This step supports the measurement domain by recording the explicit map data required for meaningful comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.