structure definition def or abbrev

`Alignment`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

ResonantAxes in IndisputableMonolith.Applied.PosturalAlignment decl_use
apply in IndisputableMonolith.Measurement.RSNative.Alignment decl_use
ew_vector_gauge in IndisputableMonolith.Physics.SectorYardsticks decl_use

depends on (5)

Lean names referenced from this declaration's body.

AlignmentMap in IndisputableMonolith.Measurement.RSNative.Alignment decl_use
AlignmentProtocol in IndisputableMonolith.Measurement.RSNative.Alignment decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use