apply
The apply definition constructs a Measurement in β from an Alignment between α and β together with a Measurement in α by mapping the value field, retaining window and uncertainty, adopting the alignment protocol, and appending an audit note. Researchers formalizing cross-agent measurement comparison within Recognition Science would invoke it to enforce explicit protocol seams. The implementation is a direct record construction that delegates value transformation to the embedded map while preserving metadata.
claimGiven an alignment structure $A$ between types $α$ and $β$ (consisting of a value map and a protocol) and a measurement $m$ with value in $α$, the result is a measurement in $β$ whose value equals the map applied to $m$'s value, with unchanged window and uncertainty, protocol taken from $A$, and notes extended by an alignment audit string.
background
The module defines the protocol-level seam for comparing measurements across agents in Recognition Science. An alignment is a packaged structure holding a map from α to β together with a protocol that records hygiene invariants; the module treats alignment as explicit data rather than solving qualia comparability. The Measurement structure carries value, window, protocol, uncertainty, and notes, as introduced in the Core submodule.
proof idea
The definition performs a direct record construction. It applies the map field of the alignment to the input measurement's value, copies the window and uncertainty fields unchanged, substitutes the protocol from the alignment, and appends an audit note that references the protocol name. No external lemmas are applied; the body is a straightforward field-wise assembly.
why it matters in Recognition Science
This definition supplies the operational step for applying alignments inside the cross-agent seam of the Measurement module. It supports the framework requirement that alignment be treated as explicit data with recorded invariants, closing one part of the scaffold described in the module documentation. No downstream uses are recorded, leaving the seam open for further protocol definitions.
scope and limits
- Does not define any concrete alignment map or protocol.
- Does not guarantee preservation of physical invariants beyond the recorded protocol.
- Does not resolve comparability of qualia or ethical quantities.
- Does not supply falsifiers for hypothesis or scaffold statuses.
formal statement (Lean)
42noncomputable def apply {α β : Type} (A : Alignment α β) (m : Measurement α) : Measurement β :=
proof body
Definition body.
43 { value := A.map m.value
44 window := m.window
45 protocol := A.protocol.protocol
46 uncertainty := m.uncertainty
47 notes := m.notes ++ [s!"Aligned via {A.protocol.name}"]
48 }
49
50end Alignment
51
52end RSNative
53end Measurement
54end IndisputableMonolith