Alignment
plain-language theorem explainer
Alignment packages a coordinate map between agent types with a protocol record that lists invariants for cross-agent comparability. Measurement researchers composing consistent data across agents cite this structure when transforming values while preserving windows and notes. It is supplied as a structure definition that directly bundles the map function and protocol record without further computation.
Claim. An alignment between types $α$ and $β$ consists of a function $f:α→β$ together with a protocol record that lists invariants (such as dominant mode or total $Z$) required to remain preserved under the mapping.
background
The module sets up a scaffold for cross-agent alignment in measurements. It defines the protocol-level seam for comparing measurements across agents and makes the alignment explicit data (a map plus a protocol) while recording invariants that must be preserved. AlignmentMap is the function type $α→β$. AlignmentProtocol extends the base Protocol with an optional list of invariants. Upstream Core.map applies a function to a measurement while copying window, protocol, uncertainty, and notes unchanged.
proof idea
This is a structure definition that requires exactly two fields: an AlignmentMap and an AlignmentProtocol. No tactics or reductions are applied; the declaration simply packages the two components for later use in measurement transformations.
why it matters
The structure supplies the packaged alignment consumed by the apply operation that transforms a measurement and appends an audit note, and it appears in the definition of ResonantAxes for the primary axes of the 8-tick cubic voxel. It fills the explicit-data requirement stated in the module documentation for cross-agent comparability. The construction supports invariant preservation needed for spatial alignments in the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.