apply
plain-language theorem explainer
The apply definition constructs a new measurement of type beta by applying the map component of an alignment structure to the input value while copying window, uncertainty, and protocol fields and appending an audit note. Researchers implementing cross-agent measurement translation in the Recognition Science scaffold would cite this when chaining protocol-level comparisons. The definition proceeds by direct record construction from the alignment map and protocol name.
Claim. Let $A$ be an alignment structure between types $α$ and $β$ (a packaged map plus protocol). For a measurement $m$ of type $α$, the result is the measurement whose value is obtained by applying the map of $A$ to the value of $m$, whose window and uncertainty are unchanged, whose protocol is taken from $A$, and whose notes are extended by a string recording the alignment protocol name.
background
The module supplies the protocol-level seam for comparing measurements across agents. It treats alignment as explicit data (map plus protocol) rather than solving qualia or ethics comparability, and records invariants that must hold for meaningful comparison. The sibling Alignment structure packages a map of type AlignmentMap α β together with an AlignmentProtocol. Upstream, the Measurement structure from Data.Import supplies the core fields (name, value, error), while Core.map shows the extended record used here (value, window, protocol, uncertainty, notes). The module doc states that falsifiers are required whenever status is hypothesis or scaffold.
proof idea
The definition is a direct record constructor. It sets value to the result of the alignment map applied to the input measurement value, copies window and uncertainty unchanged, substitutes the protocol from the alignment, and appends a formatted note string containing the protocol name.
why it matters
This definition supplies the concrete application step inside the cross-agent alignment scaffold, enabling explicit translation between measurement types while preserving an audit trail. It fills the protocol seam described in the module doc without resolving deeper comparability questions. No downstream uses are recorded, leaving the scaffold open for later integration with mass or integration-gap results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.