pith. machine review for the scientific record. sign in
def definition def or abbrev high

map

show as:
view Lean formalization →

The map definition applies a function to the value field of an RS-native Measurement record while copying its window, protocol, uncertainty, and notes unchanged. Researchers deriving new observables from raw RS data would cite it when lifting measurements across types. The implementation is a direct record construction that performs no additional computation on metadata.

claimGiven a function $f : α → β$ and a measurement $m$ whose record contains value $v$, optional window $w$, protocol $p$, optional uncertainty $u$, and notes list $n$, the result is the measurement record with value $f(v)$, window $w$, protocol $p$, uncertainty $u$, and notes $n$.

background

The Measurement structure is a record with a polymorphic value, optional Window, explicit Protocol, optional Uncertainty, and notes list. This supplies the core scaffold for RS-native measurements in which every observable carries its protocol so that windowing and coarse-graining choices remain visible rather than hidden. The module establishes a Lean-first framework whose core theory rests on ticks, voxels, and ledger observables with $τ₀ = 1$, treating SI/CODATA calibration as external. Upstream results include the generic Measurement record from Data.Import and the minimal Map scaffold from the parent Measurement module, both of which supply the type-safe transformation pattern used here.

proof idea

The definition is a one-line record constructor that sets the value field to the application of the supplied function and copies the remaining four fields verbatim from the input record.

why it matters in Recognition Science

This definition supplies the basic lifting operation required by the cost-algebra layer, appearing in downstream constructions such as CostMorphism, cost_algebra_unique_aczel, and reciprocal_involution. It thereby supports the uniqueness result for the canonical cost algebra (T5) by permitting value transformations that preserve the multiplicative structure needed for Aczél’s theorem. The same map is used in ablation studies and narrative-geodesic encodings, closing the loop from raw RS observables to derived algebraic and aesthetic quantities.

scope and limits

Lean usage

def scaled (m : Measurement ℝ) : Measurement ℝ := map (fun x => 2 * x) m

formal statement (Lean)

 127def map {α β : Type} (f : α → β) (m : Measurement α) : Measurement β :=

proof body

Definition body.

 128  { value := f m.value
 129    window := m.window
 130    protocol := m.protocol
 131    uncertainty := m.uncertainty
 132    notes := m.notes
 133  }
 134
 135/-- Map the value and replace protocol (e.g., when you derive a new observable). -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.