def
definition
name
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RSNative.Alignment on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
23
24namespace AlignmentProtocol
25
26@[simp] def name (A : AlignmentProtocol) : String := A.protocol.name
27@[simp] def status (A : AlignmentProtocol) : Status := A.protocol.status
28
29end AlignmentProtocol
30
31/-- An alignment map from one agent’s coordinate system to another’s. -/
32abbrev AlignmentMap (α β : Type) : Type := α → β
33
34/-- A packaged alignment: map + protocol hygiene. -/
35structure Alignment (α β : Type) where
36 map : AlignmentMap α β
37 protocol : AlignmentProtocol
38
39namespace Alignment
40
41/-- Apply an alignment map to a measurement value, keeping window/uncertainty, and appending an audit note. -/
42noncomputable def apply {α β : Type} (A : Alignment α β) (m : Measurement α) : Measurement β :=
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