apply
plain-language theorem explainer
This definition supplies the function that takes a packaged alignment between types alpha and beta together with a measurement in alpha and returns the corresponding measurement in beta. Cross-agent comparison work in the Recognition Science measurement scaffold would invoke it to transfer values while preserving window and uncertainty. The body is a direct record construction that applies the alignment map to the value and appends an audit note drawn from the protocol name.
Claim. Let $A$ be a packaged alignment (map plus protocol) from type $α$ to type $β$ and let $m$ be a measurement of type $α$. The aligned result is the measurement of type $β$ whose value equals the image of $m$'s value under $A$'s map, whose window and uncertainty are copied from $m$, whose protocol is taken from $A$, and whose notes are extended by an entry recording the alignment protocol name.
background
The module defines the protocol-level seam for comparing measurements across agents. It makes alignment explicit data (a map plus a protocol) and records invariants that must be preserved for a comparison to be meaningful; it does not solve qualia or ethics comparability. The Alignment structure packages a map of type AlignmentMap α β together with an AlignmentProtocol. The Measurement structure (from the Core import) carries value, window, protocol, uncertainty and notes fields. Upstream, the Core map function applies a function to the value while preserving the remaining fields.
proof idea
The definition constructs a new Measurement record by direct field assignment. It substitutes the value via the map component of the supplied Alignment, copies window and uncertainty unchanged, replaces the protocol with the one inside the alignment's protocol record, and extends the notes list with a formatted string containing the protocol name.
why it matters
The definition supplies the operational mechanism required by the module's explicit-data requirement for cross-agent measurement transfer. It sits inside the Measurement domain scaffold and enables consistent value movement under alignment protocols. No downstream uses are recorded yet; the construction therefore remains a foundational building block for later protocol hygiene checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.